[Ecls-list] Internal error when compiling the Snark theorem prover with ECL 12.7.1

[Matthias Hölzl]

Hello,

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:

silverbird:Snark tc$ ecl
;;; Loading "/Users/tc/Prog/Lisp/Quicklisp/setup.lisp"
;;; Loading #P"/usr/local/Cellar/ecl/12.7.1/lib/ecl-12.7.1/cmp.fas"
;;; Loading #P"/usr/local/Cellar/ecl/12.7.1/lib/ecl-12.7.1/asdf.fas"
ECL (Embeddable Common-Lisp) 12.7.1 (git:UNKNOWN)
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:compile-system :snark)

;;; Loading "/Users/tc/Prog/Lisp/Hacking/Snark/snark.asd"
;;; Loading "/Users/tc/Prog/Lisp/Hacking/Snark/src/snark-implementation.asd"
[...]
;;; Emitting code for UNIFY-IDENTITY.
;;; Emitting code for #:G1290.
/Users/tc/.cache/common-lisp/ecl-12.7.1-unknown-macosx-x86/Users/tc/Prog/Lisp/Hacking/Snark/src/ASDF-TMP-unify-bag.c:7252:10: error: 
      use of undeclared identifier 'aux_closure'
        value0=(aux_c...
                ^
/Users/tc/.cache/common-lisp/ecl-12.7.1-unknown-macosx-x86/Users/tc/Prog/Lisp/Hacking/Snark/src/ASDF-TMP-unify-bag.c:7252:26: error: 
      use of undeclared identifier 'env0'
        value0=(aux_closure.env=e...
                                ^
[...]
/Users/tc/.cache/common-lisp/ecl-12.7.1-unknown-macosx-x86/Users/tc/Prog/Lisp/Hacking/Snark/src/ASDF-TMP-unify-bag.c:7276:65: error: 
      use of undeclared identifier 'aux_closure'
        value0=(aux_closure.env=env0,cl_env_copy->function=(cl_object)&aux_c...
                                                                       ^
9 errors generated.
;;; Internal error:
;;;   ** Error code 1 when executing
;;; (RUN-PROGRAM "cc" ("-I." "-I/usr/local/Cellar/ecl/12.7.1/include/" "-g" "-O2" "-fPIC" "-fno-common" "-D_THREAD_SAFE" "-Ddarwin" "-O2" "-w" "-c" "/Users/tc/.cache/common-lisp/ecl-12.7.1-unknown-macosx-x86/Users/tc/Prog/Lisp/Hacking/Snark/src/ASDF-TMP-unify-bag.c" "-o" "/Users/tc/.cache/common-lisp/ecl-12.7.1-unknown-macosx-x86/Users/tc/Prog/Lisp/Hacking/Snark/src/ASDF-TMP-unify-bag.o"))
Condition of type: COMPILE-ERROR
Error while invoking #<compile-op NIL 000000010de0f690> on #<cl-source-file "snark-implementation" "unify-bag">

The first offending function in unify-bag.c is the following

/*	local function G1253                                          */
/*	optimize speed 3, debug 0, space 0, safety 2                  */
static cl_object LC39__g1253(cl_object V1)
{ VT46 VLEX46 CLSR46 STCK46
	const cl_env_ptr cl_env_copy = ecl_process_env();
	cl_object value0;
	ecl_cs_check(cl_env_copy,value0);
	{
TTL:
	value0=(aux_closure.env=env0,cl_env_copy->function=(cl_object)&aux_closure,LC49bind_yterm(2,ecl_make_fixnum(0),V1)) /*  BIND-YTERM */;
	return value0;
}}

where the problem seems to be that the definition of STCK46 in unify-bag.eclh is

#define STCK46
static cl_object LC40__g1254(cl_object );

which does not include the definition of aux_closure.  As far as I can tell by looking at the C output, LC39__g1253 is part of the definition of the BIND-XTERM function, which is pretty hairy and defined inside a LABELS form.  Unfortunately I have no simple test case that triggers the error, so this is probably not be a particularly useful bug report.  Sorry about that.

Best regards,

  Matthias