"Makarius" <[EMAIL PROTECTED]> wrote:
The deeper reason for that is that Isabelle follows the ``LCF approach'' in a heavily elaborated version. Plain ``LCF'' means the user works on the ML toplevel all the time, adding definitions and proofs by invoking ML operations directly, binding results by "val" etc. In Isabelle we first bootstrap the core system (Pure), this is a plain static compilation (and it works now in Alice, ignoring a few minor problems). Then the process continues in alternating between running the system (definitions and proofs within our own toplevel loop), and adding further ML components as the logical environment evolves. The point is that ML modules may depend on previous definitions and proofs produced at runtime. This bootstrap process never stops, although some end-users may have the illusion that the environment distributed as "Isabelle/HOL" is something like a finished program.
OK, I see. I was aware of that "LCF approach" in general, but not how exactly Isabelle employs it. Thanks for the explanation.
Note that the result is shipped as a classical ``image'' of the whole ML environment, with a root function to invoke our own toplevel loop later. So once we have managed to make compilation at runtime work properly, we will be faced with the question if pickling of something like 10-100 MB really works in practice :-)
:-) I sincerely hope it does. - Andreas _______________________________________________ alice-users mailing list [email protected] http://www.ps.uni-sb.de/mailman/listinfo/alice-users
