Sys_error с помощью ocamlmklib на объектный файл

Question

Я компиляции доказательства теорем о Cygwin, и я получаю эту ошибку:

$ make 
ocamlmklib -o bin/minisatinterface minisat/core/Solver.o minisat/simp/SimpSolver 
.o bin/Ointerface.o -lstdc++ 
** Fatal error: Error while reading minisat/core/Solver.o: Sys_error("Invalid ar 
gument") 
Makefile:49: recipe for target `bin/libminisatinterface.a' failed 
make: *** [bin/libminisatinterface.a] Error 2 

Это не ясно, какой недопустимый аргумент здесь?

only documentation Я нашел для ocamlmklib не помогло разобраться в сообщении об ошибке. Не мог ли он прочитать сам файл или возникла проблема с содержимым? ls делает список файла:

$ ls -l minisat/core/Solver.o 
-rw-r--r-- 1 gbuday mkpasswd 2096 jan. 22 10.42 minisat/core/Solver.o 

обновления: если удалить Solver.o я получаю другое сообщение об ошибке:

** Fatal error: Cannot find file "minisat/core/Solver.o" 

Так выше сообщение об ошибке о содержимом файла объект.

Answer 1

Я знаю, что это связано с сборкой ATP Satallax, которую можно использовать с Isabelle Sledgehammer, и меня попросили посмотреть на это.

У меня нет опыта работы с файлами make и ocaml. Мой успех при создании Satallax v2.7 произошел исключительно из инструкции INSTALL, с некоторой минимальной способностью догадываться о том, что означало коды ошибок, что я в основном нуждался при создании Satallax v2.6 более года назад.

Первым важным моментом является то, что tar-файл распаковывается во время работы на терминале Cygwin, а не под Windows с чем-то вроде WinZip.

Предполагая, что вы работаете на терминале Cygwin, это те заметки, которые я сделал. После этого я включу текст из Satallax INSTALL и несколько комментариев.

Sources: http://www.ps.uni-saarland.de/~cebrown/satallax/ 

0) tar xvzf satallax-2.7.tar.gz 

1) Cygwin Package (these are also for other's like Leo-II): 
    zlib-devel, make, OCaml devel, gcc devel, g++ devel, libstdc++6-devel 
    Ubuntu 12 Packages: 
    sudo apt-get install build-essential 
    zlibg-dev using the Ubuntu Software Center 
    ocaml and g++ if they don't come with "build-essential" 

2) Put eprover.exe in the path so that ./configure can find it. 
    a) There are the following lines in the configure files, which shows 
     that it's configured to find picomus, eprover has to be in the path 
     or `which eprover` has to be edited. 
     # Optionally set picomus to your picomus executable 
     picomus=${PWD}/picosat-936/picomus 
     # Optionally set eprover to your E theorem prover executable 
     eprover=`which eprover` 

3) Follow the instructions in INSTALL. 
    a) export MROOT=`pwd` takes care of this next note, which I had to do 
     for v2.6, info I keep in here in case I need it in the future. 
    b) export MROOT=<minisat-dir>, where you replace "minisat-dir" with the 
     /cygdrive/e\E_2\binp\isaprove\satallax-2.6\cygwin\minisat 

3) OLD v2.6 NOTE: If you get an error, delete the old source and try 
    untaring the sources again. 

. Моя сборка v2.7 прошла без проблем, кроме ошибок при тестировании.

С Satallax v2.7 в настоящее время требуется, чтобы сборка находила eprover. Примечание STEP 3 от INSTALL сообщает, что вы должны изменить configure или поставить eprover.exe в путь до сборки. Я положил его на пути, который для меня является

E:\E_2\dev\Isabelle2013-2\contrib\e-1.8\x86-cygwin 

МОНТАЖНАЯ файл затем дает краткие инструкции:

* Short Instructions 

cd minisat 
export MROOT=`pwd` 
cd core 
make Solver.o 
cd ../simp 
make SimpSolver.o 
cd ../../picosat-936 
./configure 
make 
cd .. 
./configure 
make 
./test | grep ERROR 

После загрузки всех необходимых пакетов и сдачи eprover.exe в пути, он построен без ошибок для меня, кроме теста, но исполняемый файл работает при использовании Изабель Кувалдоймер.

STEP 3 из INSTALL переговоров о предоставлении местоположения picomus исполняемого файла, но я уверен, что не нужно делать, потому что picosat-936\picomus.exe будет построен в этой сборке.

Если вы смотрите сообщения о строительстве, он расскажет вам, что он ищет и что он находит.

Для полноты, включаю текст от INSTALL, за исключением инструкций, относящихся к тому, что уместно для Coq.

There are a number of requirements in order to compile Satallax. 
In short, you need make, ocaml, g++ and the zlib header files. 
In Debian and derived Linux systems, you can get these from 
the build-essential and zlib1g-dev packages. You need 
ocamlopt to obtain a standalone executable. 

If you're not the administrator of the computer on which you're installing, 
you can quote the previous paragraph to the administrator. 

* Short Instructions 

cd minisat 
export MROOT=`pwd` 
cd core 
make Solver.o 
cd ../simp 
make SimpSolver.o 
cd ../../picosat-936 
./configure 
make 
cd .. 
./configure 
make 
./test | grep ERROR 

./bin/satallax.opt is the native code executable to use. 
See test for examples of how to use it. 

* Long Instructions 

STEP 1: 

Compile minisat (see minisat/README) 

cd minisat 
export MROOT=<minisat-dir>    (or setenv in cshell) 
cd core 
make Solver.o 
cd ../simp 
make SimpSolver.o 
cd ../.. 

STEP 2 (Optional. Only needed to extract proof information for proof terms.) : 

Build picosat (including picomus): 

cd picosat-936 
./configure 
make 
cd .. 

STEP 3: 

If desired, edit the configure script to give the location of your picomus 
and eprover executables. (If the executables are not found by the configure script, 
you will need to give the location of the executables to satallax via the command line 
options -P <picomus> -E <eprover> if they are needed.) 
Run the configure script for Satallax. 

./configure 

STEP 4: 

make 

uses ocamlopt to make a standalone executable 

./bin/satallax.opt 

and uses ocamlc to make a bytecode executable 

./bin/satallax 

that depends on ocamlrun 

STEP 5: 

Test satallax using the examples in the script file: 

./test 

As long as you don't see a line with the word ERROR, it should be working.