On Sat, 12 May 2007, Andreas Rossberg wrote:
> It is hard for me to judge if this approach is workable for you.
> Isabelle's reliance on the 'use' function is likely to have imposed a
> program structure that is not particularly modular, at least not in the
> way Alice ML tries to support.
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.
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 will be unavailable for the next few weeks. Maybe Priya manages to get
more things to work in the meantime.)
Makarius
_______________________________________________
alice-users mailing list
[email protected]
http://www.ps.uni-sb.de/mailman/listinfo/alice-users
