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

[Juan Jose Garcia-Ripoll]

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.

Just to give some background, the problem with ECL is that it has two types
of closures and it not only has to detect that a function closes over some
variables (which is hard enough given recursiveness) but also determine
whether the closure has dynamical extent or not. The previous algorithm
naïvely assumed this could be determined in one pass + some correction
phase, but I have had to add some additional steps in the compilation of
the LABELS form.

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.

Also, given that the change is critical enough, it would be nice if Anton
could report the results from cl-test-grid (which should run any time this
afternoon or tomorrow morning).

Best,

Juanjo

-- 
Instituto de Física Fundamental, CSIC
c/ Serrano, 113b, Madrid 28006 (Spain)
http://juanjose.garciaripoll.googlepages.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman.common-lisp.net/pipermail/ecl-devel/attachments/20121111/b983b702/attachment.html>