search

asr / apia

Haskell program for proving first-order theorems written in Agda using automatic theorem provers for first-order logic
MIT License
6 stars 0 forks source link

An internal error using iLeanCop 1.2 #97

Closed jonaprieto closed 7 years ago

jonaprieto commented 7 years ago

I am getting this error:

$ cat $ILEANCOP/ileancop.sh | head -n 4
#!/bin/sh
#-------------
# File:    ileancop.sh
# Version: 1.2
$ file $ILEANCOP/ileancop.sh
/home/hotel/ileancop/ileancop.sh: POSIX shell script, ASCII text executable
$ ls -l $ILEANCOP/ileancop.sh
-rwxr-xr-x. 1 hotel hotel 1678 Mar 16  2008 /home/hotel/ileancop/ileancop.sh
$ apia --version
Apia version 1.0.1-a5404d0
$ make ATPs=\"ileancop\" prove_notes
echo  notes/README/Test.prove_notes
notes/README/Test.prove_notes
agda -v 0 -inotes -inotes/README notes/README/Test.agda
Proving the conjecture in /tmp/apia/notes/README/Test/13-8744-comm.fof
An internal error has occurred. Please report this as a bug.
Location of the error: src/Apia/ATPs.hs:207

Makefile:424: recipe for target 'notes/README/Test.prove_notes' failed
make: *** [notes/README/Test.prove_notes] Error 1
$ agda --version
Agda version 2.6.0.1-509f498
asr commented 7 years ago

That version of ileanCoP isn't supported (see the README). I attach the supported version: ileancop13beta1.tar.gz.

jonaprieto commented 7 years ago

Yeap, I forgot it. Sorry.