[Openmcl-devel] problem quitting the compiler

Gergely Buday gbuday at gmail.com
Thu Jul 17 08:40:24 PDT 2014


On 17 July 2014 17:32, Gail Zacharias <gz at clozure.com> wrote:
> You're probably in some random package. Try (ccl:quit).

Thanks. Starting the compiler with scripts/ccl64 I was able to compile
my software and save the image by (save-application). Upon loading it
it does not behave as if it were run from the REPL -- it does not
recognise the definitions that are in theory there. What should I pay
attention for here?

This is nqthm-1992, an archaic theorem prover. I compiled it according
to its README, then I restarted ccl, loaded nqthm, loaded a proof
script and then I used (save-application).

- Gergely



More information about the Openmcl-devel mailing list