[Ecls-list] Internal error when compiling the Snark theorem prover with ECL 12.7.1
Matthias Hölzl
tc at xantira.com
Fri Nov 16 19:22:29 UTC 2012
On Nov 11, 2012, at 18:46 , Juan Jose Garcia-Ripoll <juanjose.garciaripoll at gmail.com> wrote:
> On Wed, Oct 31, 2012 at 1:17 AM, Matthias Hölzl <tc at xantira.com> wrote:
> when compiling the Snark theorem prover (<http://www.ai.sri.com/~stickel/snark.html>, or with ASDF system definition at <https://github.com/hoelzl/Snark>), ECL (version 12.7.1 on OSX 10.8.2, installed using homebrew) fails with an internal error:
>
> I have worked out the origin of the error. It is in a nested set of LABELS and closure forms that is complicated enough to make ECL's closure detection algorithm fail.
>
> [...]
>
> The result seems to be that ECL now can *build* Snark. It would be nice to have some idea about the actual performance, for it might uncover further bugs to be tracked down.
Many thanks for solving the problem with building Snark on ECL. I can now build and run our Iliad system (which uses Snark as a central component) and successfully run all tests that don't use Snark. It is also possible to initialize Snark and define logical theories, however as soon as I try to start a proof I get an error message (both in Iliad and in stand-alone Snark):
================================================================================
bash-3.2$ ecl
;;; Loading "/Users/tc/Prog/Lisp/Quicklisp/setup.lisp"
;;; Loading #P"/usr/local/lib/ecl-12.7.1/cmp.fas"
;;; Loading #P"/usr/local/lib/ecl-12.7.1/asdf.fas"
ECL (Embeddable Common-Lisp) 12.7.1 (git:b970c5b206f2590531bab24acadfff165ccb2f92)
Copyright (C) 1984 Taiichi Yuasa and Masami Hagiya
Copyright (C) 1993 Giuseppe Attardi
Copyright (C) 2000 Juan J. Garcia-Ripoll
ECL is free software, and you are welcome to redistribute it
under certain conditions; see file 'Copyright' for details.
Type :h for Help.
Top level in: #<process TOP-LEVEL>.
> (asdf:load-system :snark)
;;; Loading "/Users/tc/Prog/Lisp/Hacking/Snark/snark.asd"
[...]
;;; Loading "/Users/tc/.cache/common-lisp/ecl-12.7.1-b970c5b2-macosx-x86/Users/tc/Prog/Lisp/Hacking/Snark/src/coder.fas"
T
> (in-package :snark-user)
#<"SNARK-USER" package>
SNARK-USER> (initialize)
; Running SNARK from /Users/tc/Prog/Lisp/Hacking/Snark/ in ECL 12.7.1 on silverbird.fritz.box at 2012-11-16T19:50:40
NIL
SNARK-USER> (use-resolution)
T
SNARK-USER> (assert '(foo x))
NIL
SNARK-USER> (prove '(foo ?x) :answer '(ans ?x))
; The current SNARK option values are
; (USE-RESOLUTION T)
; (USE-HYPERRESOLUTION NIL)
[... More output of Snark]
; (USE-RELEVANCE-TEST NIL)
Condition of type: TYPE-ERROR
SI:MISSING-KEYWORD is not of type SNARK-SPARSE-ARRAY::SPARSE-VECTOR-INDEX.
Available restarts:
1. (RESTART-TOPLEVEL) Go back to Top-Level REPL.
Broken at SI:BYTECODES. [Evaluation of: (SNARK:PROVE '(SNARK-USER::FOO SNARK:?X) :ANSWER '(SNARK-USER::ANS SNARK:?X))] In: #<process TOP-LEVEL>.
>> :b
Backtrace:
> SI:BYTECODES [Evaluation of: (SNARK:PROVE '(SNARK-USER::FOO SNARK:?X) :ANSWER '(SNARK-USER::ANS SNARK:?X))]
> si:bytecodes [Evaluation of: (si:top-level t)]
>> :f
Broken at SI:BYTECODES. [Evaluation of: (SNARK:PROVE '(SNARK-USER::FOO SNARK:?X) :ANSWER '(SNARK-USER::ANS SNARK:?X))] In: #<process TOP-LEVEL>.
>> :disassemble
#((SNARK-USER::FOO SNARK:?X) :ANSWER (SNARK-USER::ANS SNARK:?X) SNARK:PROVE)
Name: BYTECODES
Evaluated form:
0 PUSH '(SNARK-USER::FOO SNARK:?X)
2 PUSHVS :ANSWER
4 PUSH '(SNARK-USER::ANS SNARK:?X)
6 CALLG 3,PROVE
9 EXIT
>> :le
(SNARK:PROVE '(SNARK-USER::FOO SNARK:?X) :ANSWER '(SNARK-USER::ANS SNARK:?X))
>> (quit)
; Summary of computation:
[... Some more output of Snark]
; The agenda of input rows to process has 2 entries:
Condition of type: TYPE-ERROR
SI:MISSING-KEYWORD is not of type SNARK-SPARSE-ARRAY::SPARSE-VECTOR-INDEX.
Available restarts:
1. (RESTART-TOPLEVEL) Go back to Top-Level REPL.
Broken at SI:BYTECODES. [Evaluation of: (SNARK:PROVE '(SNARK-USER::FOO SNARK:?X) :ANSWER '(SNARK-USER::ANS SNARK:?X))] In: #<process TOP-LEVEL>.
>> :q
Top level in: #<process TOP-LEVEL>.
SNARK-USER> (quit)
NIL
SNARK-USER>
================================================================================
I'm not sure what the reason for this error might be. However it might be a more general problem with my ECL installation since I cannot load Slime either. When trying to load Slime I get the following result:
================================================================================
(progn (load "/Users/tc/Prog/Lisp/Slime/swank-loader.lisp" :verbose t) (funcall (read-from-string "swank-loader:init")) (funcall (read-from-string "swank:start-server") "/var/folders/7k/fxjq0hl95rv8xs93mgj04vp00000gn/T/slime.18263"))
;;; Loading "/Users/tc/Prog/Lisp/Quicklisp/setup.lisp"
;;; Loading #P"/usr/local/lib/ecl-12.7.1/cmp.fas"
;;; Loading #P"/usr/local/lib/ecl-12.7.1/asdf.fas"
;;; Warning:
;;; in file impl-util.lisp, position 48
;;; at (DEFINTERFACE CALL-WITH-QUIET-COMPILATION ...)
;;; ! The variable #:%IMPLEMENTATION is not used.
[...]
;;; Warning:
;;; in file impl-util.lisp, position 9155
;;; at (DEFINTERFACE DELETE-DIRECTORY-TREE ...)
;;; ! The variable #:%IMPLEMENTATION is not used.;;; Warning: COMPILE-FILE warned while performing
#<compile-op (:VERBOSE NIL) 000000011079c0f0> on
#<cl-source-file "quicklisp" "impl-util">.
;;; Warning:
;;; in file network.lisp, position 75
;;; at (DEFINTERFACE HOST-ADDRESS ...)
;;; ! The variable #:%IMPLEMENTATION is not used.
[...]
;;; Warning:
;;; in file network.lisp, position 4313
;;; at (DEFINTERFACE CALL-WITH-CONNECTION ...)
;;; ! The variable #:%IMPLEMENTATION is not used.;;; Warning: COMPILE-FILE warned while performing
#<compile-op (:VERBOSE NIL) 000000011079c0f0> on
#<cl-source-file "quicklisp" "network">.
;;; Warning:
;;; in file deflate.lisp, position 4847
;;; at (DEFUN GENERATE-CRC32-TABLE ...)
;;; ! Too few arguments for proclaimed function LOGAND
;;; Warning:
;;; in file deflate.lisp, position 5742
;;; at (DEFUN UPDATE-CRC32-CHECKSUM ...)
;;; ! Too few arguments for proclaimed function LOGAND
;;; Warning:
;;; ! Too few arguments for proclaimed function LOGAND
;;; Warning:
;;; ! Too few arguments for proclaimed function LOGAND;;; Warning: COMPILE-FILE warned while performing
#<compile-op (:VERBOSE NIL) 000000011079c0f0> on
#<cl-source-file "quicklisp" "deflate">.
;;; Warning:
;;; in file cdb.lisp, position 77
;;; at (DEFUN CDB-HASH ...)
;;; ! Too few arguments for proclaimed function LOGAND
;;; Warning:
;;; in file cdb.lisp, position 1046
;;; at (DEFUN READ-CDB-U32 ...)
;;; ! Too few arguments for proclaimed function LOGAND
;;; Warning:
;;; in file cdb.lisp, position 2580
;;; at (DEFUN STREAM-LOOKUP ...)
;;; ! Too few arguments for proclaimed function LOGAND
;;; Warning:
;;; in file cdb.lisp, position 9100
;;; at (DEFUN ADD-RECORD ...)
;;; ! Too few arguments for proclaimed function LOGAND
;;; Warning:
;;; ! Too few arguments for proclaimed function LOGAND
;;; Warning:
;;; ! Too few arguments for proclaimed function LOGAND
;;; Warning:
;;; ! Too few arguments for proclaimed function LOGAND
;;; Warning:
;;; ! Too few arguments for proclaimed function LOGAND;;; Warning: COMPILE-FILE warned while performing
#<compile-op (:VERBOSE NIL) 000000011079c0f0> on
#<cl-source-file "quicklisp" "cdb">.
;;; Warning:
;;; in file dist.lisp, position 4920
;;; at (DEFGENERIC PREFERENCE ...)
;;; ! The variable OBJECT is not used.
[...]
;;; Warning:
;;; in file dist.lisp, position 33391
;;; at (DEFMETHOD PROVIDED-SYSTEMS ...)
;;; ! The variable OBJECT is not used.
;;; Warning:
;;; in file dist.lisp, position 33594
;;; at (DEFMETHOD PROVIDED-RELEASES ...)
;;; ! The variable OBJECT is not used.;;; Warning: COMPILE-FILE warned while performing
#<compile-op (:VERBOSE NIL) 000000011079c0f0> on
#<cl-source-file "quicklisp" "dist">.
;;; Warning:
;;; in file client.lisp, position 1117
;;; at (DEFMETHOD QUICKLOAD ...)
;;; ! The variable EXPLAIN is not used.
;;; Warning:
;;; in file client.lisp, position 1117
;;; at (DEFMETHOD QUICKLOAD ...)
;;; ! The variable PROMPT is not used.
;;; Warning:
;;; in file client.lisp, position 1117
;;; at (DEFMETHOD QUICKLOAD ...)
;;; ! The variable VERBOSE is not used.
;;; Warning:
;;; in file client.lisp, position 1117
;;; at (DEFMETHOD QUICKLOAD ...)
;;; ! The variable SYSTEMS is not used.;;; Warning: COMPILE-FILE warned while performing
#<compile-op (:VERBOSE NIL) 000000011079c0f0> on
#<cl-source-file "quicklisp" "client">.
;;; Warning:
;;; in file dist-update.lisp, position 3816
;;; at (DEFMETHOD UPDATE-IN-PLACE ...)
;;; ! The variable NEW-DIST is not used.
;;; Warning:
;;; in file dist-update.lisp, position 3986
;;; at (DEFMETHOD UPDATE-IN-PLACE ...)
;;; ! The variable OLD-DIST is not used.;;; Warning: COMPILE-FILE warned while performing
#<compile-op (:VERBOSE NIL) 000000011079c0f0> on
#<cl-source-file "quicklisp" "dist-update">.
ECL (Embeddable Common-Lisp) 12.7.1 (git:b970c5b206f2590531bab24acadfff165ccb2f92)
Copyright (C) 1984 Taiichi Yuasa and Masami Hagiya
Copyright (C) 1993 Giuseppe Attardi
Copyright (C) 2000 Juan J. Garcia-Ripoll
ECL is free software, and you are welcome to redistribute it
under certain conditions; see file 'Copyright' for details.
Type :h for Help.
Top level in: #<process TOP-LEVEL>.
>
;;; Loading "/Users/tc/Prog/Lisp/Slime/swank-loader.lisp"
;;;
;;; Compiling /Users/tc/Prog/Lisp/Slime/swank-backend.lisp.
;;; OPTIMIZE levels: Safety=2, Space=0, Speed=3, Debug=0
;;;
;;; Warning:
;;; in file swank-backend.lisp, position 21332
;;; at (FSET 'WITH-COMPILATION-HOOKS ...)
;;; ! The variable #:G460 is not used.
;;; Warning:
;;; in file swank-backend.lisp, position 47770
;;; at (DEFINTERFACE SEND ...)
;;; ! The variable THREAD is not used.
;;; Warning:
;;; in file swank-backend.lisp, position 48337
;;; at (DEFINTERFACE FIND-REGISTERED ...)
;;; ! The variable NAME is not used.
;;; End of Pass 1.
;;; Finished compiling /Users/tc/Prog/Lisp/Slime/swank-backend.lisp.
;;;
;;; Loading "/Users/tc/.slime/fasl/2012-11-13/ecl-12.7.1-b970c5b2-darwin-i686/swank-backend.fas"
;;;
;;; Compiling /Users/tc/Prog/Lisp/Slime/swank-source-path-parser.lisp.
;;; OPTIMIZE levels: Safety=2, Space=0, Speed=3, Debug=0
;;;
;;; End of Pass 1.
[...]
;;; Finished compiling /Users/tc/Prog/Lisp/Slime/swank-source-file-cache.lisp.
;;;
;;; Loading "/Users/tc/.slime/fasl/2012-11-13/ecl-12.7.1-b970c5b2-darwin-i686/swank-source-file-cache.fas"
;;;
;;; Compiling /Users/tc/Prog/Lisp/Slime/swank-ecl.lisp.
;;; OPTIMIZE levels: Safety=2, Space=0, Speed=3, Debug=0
;;;
;;; Loading "/usr/local/lib/ecl-12.7.1/profile.asd"
;;; Loading "/usr/local/lib/ecl-12.7.1/profile.fas"
;;; Loading "/usr/local/lib/ecl-12.7.1/serve-event.asd"
;;; Loading "/usr/local/lib/ecl-12.7.1/serve-event.fas"
;;; Style warning:
;;; in file swank-ecl.lisp, position 2486
;;; at (DEFIMPLEMENTATION ACCEPT-CONNECTION ...)
;;; ! Variable LINE was undefined. Compiler assumes it is a global.
;;; End of Pass 1.
;;; Finished compiling /Users/tc/Prog/Lisp/Slime/swank-ecl.lisp.
;;;
;;; Loading "/Users/tc/.slime/fasl/2012-11-13/ecl-12.7.1-b970c5b2-darwin-i686/swank-ecl.fas"
;;;
;;; Compiling /Users/tc/Prog/Lisp/Slime/swank-gray.lisp.
;;; OPTIMIZE levels: Safety=2, Space=0, Speed=3, Debug=3
;;;
;;; Warning:
;;; in file swank-gray.lisp, position 2055
;;; at (DEFMETHOD STREAM-LINE-LENGTH ...)
;;; ! The variable STREAM is not used.
;;; Warning:
;;; in file swank-gray.lisp, position 4140
;;; at (DEFMETHOD STREAM-LINE-COLUMN ...)
;;; ! The variable S is not used.
;;; Warning:
;;; in file swank-gray.lisp, position 4203
;;; at (DEFMETHOD STREAM-LINE-LENGTH ...)
;;; ! The variable S is not used.
;;; End of Pass 1.
;;; Finished compiling /Users/tc/Prog/Lisp/Slime/swank-gray.lisp.
;;;
[...]
;;;
;;; Loading "/Users/tc/.slime/fasl/2012-11-13/ecl-12.7.1-b970c5b2-darwin-i686/swank-rpc.fas"
;;;
;;; Compiling /Users/tc/Prog/Lisp/Slime/swank.lisp.
;;; OPTIMIZE levels: Safety=2, Space=0, Speed=3, Debug=3
;;;
;;; Warning:
;;; in file swank.lisp, position 105352
;;; at (FSET 'WITH-DESCRIBE-SETTINGS ...)
;;; ! The variable #:G1041 is not used.
;;; End of Pass 1.
;;; Finished compiling /Users/tc/Prog/Lisp/Slime/swank.lisp.
;;;
;;; Loading "/Users/tc/.slime/fasl/2012-11-13/ecl-12.7.1-b970c5b2-darwin-i686/swank.fas"
;;; Warning: These Swank interfaces are unimplemented:
(ACTIVATE-STEPPING ADD-FD-HANDLER ADD-SIGIO-HANDLER BACKGROUND-SAVE-IMAGE DUP
EXEC-IMAGE FRAME-CALL LIST-CALLEES LIST-CALLERS MACROEXPAND-ALL
MAKE-FD-STREAM REMOVE-FD-HANDLERS REMOVE-SIGIO-HANDLERS RESTART-FRAME
RETURN-FROM-FRAME SAVE-IMAGE SLDB-BREAK-AT-START SLDB-BREAK-ON-RETURN
SLDB-STEP-INTO SLDB-STEP-NEXT SLDB-STEP-OUT TOGGLE-TRACE)
;;; Loading "/Users/tc/.swank.lisp"
;;;
;;; Compiling /Users/tc/Prog/Lisp/Slime/contrib/swank-util.lisp.
;;; OPTIMIZE levels: Safety=2, Space=0, Speed=3, Debug=3
;;;
;;; End of Pass 1.
;;; Finished compiling /Users/tc/Prog/Lisp/Slime/contrib/swank-util.lisp.
[...]
;;; Compiling /Users/tc/Prog/Lisp/Slime/contrib/swank-arglists.lisp.
;;; OPTIMIZE levels: Safety=2, Space=0, Speed=3, Debug=3
;;;
;;; Loading "/Users/tc/.slime/fasl/2012-11-13/ecl-12.7.1-b970c5b2-darwin-i686/contrib/swank-c-p-c.fas"
;;; Warning:
;;; in file swank-arglists.lisp, position 36057
;;; at (DEFMETHOD COMPUTE-ENRICHED-DECODED-ARGLIST ...)
;;; ! The variable OPERATOR-FORM is not used.
[...]
;;; Warning:
;;; in file swank-arglists.lisp, position 54430
;;; at (DEFGENERIC EXTRACT-LOCAL-OP-ARGLISTS ...)
;;; ! The variable OPERATOR is not used.
;;; End of Pass 1.
;;; Finished compiling /Users/tc/Prog/Lisp/Slime/contrib/swank-arglists.lisp.
;;;
;;;
;;; Compiling /Users/tc/Prog/Lisp/Slime/contrib/swank-fuzzy.lisp.
;;; OPTIMIZE levels: Safety=2, Space=0, Speed=3, Debug=3
;;;
;;; End of Pass 1.
;;; Finished compiling /Users/tc/Prog/Lisp/Slime/contrib/swank-fuzzy.lisp.
;;;
;;;
;;; Compiling /Users/tc/Prog/Lisp/Slime/contrib/swank-fancy-inspector.lisp.
;;; OPTIMIZE levels: Safety=2, Space=0, Speed=3, Debug=3
;;;
;;; Warning:
;;; in file swank-fancy-inspector.lisp, position 24913
;;; at (DEFMETHOD MAKE-SYMBOLS-LISTING ...)
;;; ! The variable GROUPING-KIND is not used.
;;; Warning:
;;; in file swank-fancy-inspector.lisp, position 26666
;;; at (DEFMETHOD MAKE-SYMBOLS-LISTING ...)
;;; ! The variable GROUPING-KIND is not used.
;;; End of Pass 1..slime/fasl/2012-11-13/ecl-12.7.1-b970c5b2-darwin-i686/contrib/swank-fancy-inspector.c: In function ‘LC62normalize_classifications’:
.slime/fasl/2012-11-13/ecl-12.7.1-b970c5b2-darwin-i686/contrib/swank-fancy-inspector.c:4167: error: ‘CLV0’ undeclared (first use in this function)
.slime/fasl/2012-11-13/ecl-12.7.1-b970c5b2-darwin-i686/contrib/swank-fancy-inspector.c:4167: error: (Each undeclared identifier is reported only once
.slime/fasl/2012-11-13/ecl-12.7.1-b970c5b2-darwin-i686/contrib/swank-fancy-inspector.c:4167: error: for each function it appears in.)
;;; Internal error:
;;; ** Error code 1 when executing
;;; (RUN-PROGRAM "gcc" ("-I." "-I/usr/local/include/" "-g" "-O2" "-fPIC" "-fno-common" "-D_THREAD_SAFE" "-Ddarwin" "-O2" "-w" "-c" ".slime/fasl/2012-11-13/ecl-12.7.1-b970c5b2-darwin-i686/contrib/swank-fancy-inspector.c" "-o" ".slime/fasl/2012-11-13/ecl-12.7.1-b970c5b2-darwin-i686/contrib/swank-fancy-inspector.o"));;
;; Error while compiling /Users/tc/Prog/Lisp/Slime/contrib/swank-fancy-inspector.lisp:
;; COMPILE-FILE returned NIL.
;; Aborting.
;;
Condition of type: SIMPLE-CONTROL-ERROR
Restart ABORT is not active.
Available restarts:
1. (RESTART-TOPLEVEL) Go back to Top-Level REPL.
Broken at SWANK-LOADER::HANDLE-SWANK-LOAD-ERROR. In: #<process TOP-LEVEL>.
File: #P"/Users/tc/Prog/Lisp/Slime/swank-loader.lisp" (Position #5714)
>> (quit)
Process inferior-lisp finished
================================================================================
Do you have any suggestions what the reasons for these errors might be, or how to proceed with debugging them? It would be really great if we could get Iliad running on ECL.
Best regards,
Matthias
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman.common-lisp.net/pipermail/ecl-devel/attachments/20121116/4680c95e/attachment.html>
More information about the ecl-devel
mailing list