On Wed, Oct 31, 2012 at 1:17 AM, Matthias Hölzl <tc@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).



Instituto de Física Fundamental, CSIC
c/ Serrano, 113b, Madrid 28006 (Spain)