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

op/3: No permission to create operator `'|'' #31

Closed jonaprieto closed 8 years ago

jonaprieto commented 8 years ago 
λ apia Test.agda --atp=metis --atp=z3 --output-dir=.
Proving the conjecture in ./Test/13-8744-comm.fof
ERROR: op/3: No permission to create operator `'|''
(error "failed to open file './Test/13-8744-comm.smt2'")
metis 2.3 (release 20160102) proved the conjecture
apia: getProcessGroupIDOf: does not exist (No such process)
asr commented 8 years ago

I couldn't reproduce the issue. The issue is related to the tptp2X program which is required when using Z3.

asr commented 8 years ago

Which is the output of running 

$ tptp2X foo

?

jonaprieto commented 8 years ago 
λ ~/ tptp2X foo
---------------------------------------------------------------------
TPTP2X directory      = /Users/jonaprieto/Desktop/EAFIT/Research/TPTP-v6.3.0/TPTP2X
TPTP directory        = /Users/jonaprieto/Desktop/EAFIT/Research/TPTP-v6.3.0
Prolog interpreter    = /usr/local/bin/swipl
Files to convert      = foo
Size                  =
Transformation        = none
Format to convert to  = tptp:short
Output directory      = /Users/jonaprieto/tptp
---------------------------------------------------------------------
ERROR : /Users/jonaprieto/foo cannot be found, and has been ignored.
asr commented 8 years ago

Prolog interpreter = /usr/local/bin/swipl

Could you reproduce the problem building tptp2X using a different Prolog interpreter?

jonaprieto commented 8 years ago

With gnu-prolog.

λ ~/ tptp2X foo
---------------------------------------------------------------------
TPTP2X directory      = /Users/jonaprieto/Desktop/EAFIT/Research/TPTP-v6.3.0/TPTP2X
TPTP directory        = /Users/jonaprieto/Desktop/EAFIT/Research/TPTP-v6.3.0
Prolog interpreter    = /usr/local/bin/gprolog
Files to convert      = foo
Size                  =
Transformation        = none
Format to convert to  = tptp:short
Output directory      = /Users/jonaprieto/tptp
---------------------------------------------------------------------
ERROR : /Users/jonaprieto/foo cannot be found, and has been ignored.
λ ~/ cd ~/apia/notes/README
λ ~/apia/notes/README/ master* apia Test.agda --atp=metis --atp=z3 --output-dir=.
Proving the conjecture in ./Test/13-8744-comm.fof
uncaught exception: error(existence_error(procedure,tptp2X/5),top_level/0)
| ?-
(error "failed to open file './Test/13-8744-comm.smt2'")
metis 2.3 (release 20160102) proved the conjecture
apia: getProcessGroupIDOf: does not exist (No such process)
λ ~/apia/notes/README/ master*
asr commented 8 years ago

Could you reproduce the problem using your version of Linux?

jonaprieto commented 8 years ago

In linux with yap:

λ apia Test.agda --atp=metis --atp=z3 --output-dir=.
Proving the conjecture in ./Test/13-8744-comm.fof
     ERROR!!
     PERMISSION ERROR- op(502,xfy,|): cannot create operator |
% YAP execution halted
metis 2.3 (release 20160102) proved the conjecture

And then, I installed gprolog

λ  apia Test.agda --atp=metis --atp=z3 --output-dir=.
Proving the conjecture in ./Test/13-8744-comm.fof
uncaught exception: error(existence_error(procedure,tptp2X/5),top_level/0)
metis 2.3 (release 20160102) proved the conjecture

The problem is with z3 I guess. Z3 version 4.4.1.

asr commented 8 years ago

The problem is with z3 I guess.

Yes, see my previous comment.

asr commented 8 years ago

The installation of tptp2X asks:

The Prolog dialect must be one of :
    eclipse, yap, swi, sicstus, quintus, generic

I could reproduce the issue using swi, but I couldn't using eclipse:

$ cat refl.fof
fof(refl, conjecture, ! [X] : X = X).
$ tptp2X -q2 -fsmt2 -d. refl.fof
/tmp/refl.fof -> /tmp//refl.smt2

Could you reproduce the issue using eclipse?

jonaprieto commented 8 years ago

This issue about operator (|) is not present with eclipse because is more liberal than the others Prolog implementations (e.g. see the documentation about op/3 in swi-prolog, the bar can only be greater or equal than 1100 priority).

λ  eclipse                               
ECLiPSe Constraint Logic Programming System [kernel]
Version 6.1 #220 (x86_64_linux), Thu Apr 21 22:40 2016
[eclipse 1]: op(502, xfy, '|').
Yes (0.00s cpu)

But, using another prolog like swilp

λ  swipl
Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.2.3)
?- op(502, xfy, '|').
ERROR: op/3: No permission to create operator `'|''

I figured it out how to avoid this error message.

λ  swipl
Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.2.3)
?- op(502, xfy, '|').
ERROR: op/3: No permission to create operator `'|''
?- use_module(library(system)).
true
?- system_mode(true).
true.
?- op(502, xfy, '|').
true.
?- system_mode(false).
true.

Then, modifying in the file tptp2X.main the lines related with bar operator from the installation folder TPTP/TPTP2X, the error message op/3: No permission to create operator '|'' disappears but a new messages appear.

:-use_module(library(system)).
:-system_mode(true).
:-op(502, xfy, '|').
:-system_mode(false).

But it's kind of hack.

Anyway, using eclipse without modify anything, tptp2X doesn't work, let's try a call of tptp2X given as example in the documentation of tptp2X.

λ ~/TPTP-v6.3.0/TPTP2X/ tptp2X -tfr,random -f prover9 PUZ001+1
---------------------------------------------------------------------
TPTP2X directory      = /home/jonaprieto/TPTP-v6.3.0/TPTP2X
TPTP directory        = /home/jonaprieto/TPTP-v6.3.0
Prolog interpreter    = /home/jonaprieto/prologs/bin/x86_64_linux//eclipse
Files to convert      = PUZ001+1
Size                  = 
Transformation        = fr,random
Format to convert to  = prover9
Output directory      = /home/jonaprieto/TPTP-v6.3.0/TPTP2X/prover9
---------------------------------------------------------------------
Abort
asr commented 8 years ago

Anyway, using eclipse without modify anything, tptp2X doesn't work

Did you test the MVE in my previous comment?

asr commented 8 years ago

λ ~/TPTP-v6.3.0/TPTP2X/ tptp2X -tfr,random -f prover9 PUZ001+1

What are you testing in this example?

asr commented 8 years ago

This issue about operator (|) is not present with eclipse because is more liberal than the others Prolog implementations (e.g. see the documentation about op/3 in swi-prolog, the bar can only be greater or equal than 1100 priority).

Please report this problem (CC'ing me) using a MVE to tptp2X's authors.

jonaprieto commented 8 years ago

Did you test the MVE in my previous comment?

Yes, I did. 

λ  tptp2X -q2 -fsmt2 -d. refl.fof        
Abort
[eclipse 5]: Error(s) occurred while compiling tptp2X.main
calling an undefined procedure prolog_dialect(_441) in module eclipse

I ran another ./tptpt2_install and,

λ  tptp2X -q2 -fsmt2 -d. refl.fof
Abort

What are you testing in this example? The output must be something like:

~/TPTP/TPTP2X> tptp2X -tfr,random -f prover9 PUZ001+1
---------------------------------------------------------------------
TPTP2X directory      = /home/graph/tptp/TPTP/TPTP2X
TPTP directory        = /home/graph/tptp/TPTP
Prolog interpreter    = /usr/local/eclipse5.10_140/bin/i386_linux/eclipse
Files to convert      = PUZ001+1
Size                  = 
Transformation        = fr,random
Format to convert to  = prover9
Output directory      = /home/graph/tptp/TPTP/TPTP2X/prover9
---------------------------------------------------------------------
Made the directory /home/graph/tptp/TPTP/TPTP2X/prover9/PUZ
/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p -> /home/graph/tptp/TPTP/TPTP2X/prover9/PUZ/PUZ001+1+fr.in
/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p -> /home/graph/tptp/TPTP/TPTP2X/prover9/PUZ/PUZ001+1+ran.in
asr commented 8 years ago

λ ~/apia/notes/README/ master*

Please use a simpler prompt for reporting the issues.

asr commented 8 years ago

Using your (binary) version of eclipse, I could reproduce the issue:

$ eclipse
ECLiPSe Constraint Logic Programming System [kernel]
Kernel and basic libraries copyright Cisco Systems, Inc.
and subject to the Cisco-style Mozilla Public Licence 1.1
(see legal/cmpl.txt or http://eclipseclp.org/licence)
Source available at www.sourceforge.org/projects/eclipse-clp
GMP library copyright Free Software Foundation, see legal/lgpl.txt
For other libraries see their individual copyright notices
Version 6.1 #220 (x86_64_linux), Thu Apr 21 22:40 2016
$ tptp2X -q2 -fsmt2 -d. refl1.fof
Abort
asr commented 8 years ago

The above example works for me using

$ eclipse
ECLiPSe Constraint Logic Programming System [kernel]
Kernel and basic libraries copyright Cisco Systems, Inc.
and subject to the Cisco-style Mozilla Public Licence 1.1
(see legal/cmpl.txt or www.eclipse-clp.org/licence)
Source available at www.sourceforge.org/projects/eclipse-clp
GMP library copyright Free Software Foundation, see legal/lgpl.txt
For other libraries see their individual copyright notices
Version 5.10 #42, Sun Dec 24 15:09 2006
jonaprieto commented 8 years ago

It works with that version of eclipse.

asr commented 8 years ago

I replaced the use of tptp2X by using tptp4X in cbf5cad, so I'm closing the issue.