On Sat, 20 Jun 2009, David Matthews wrote:
The model we've traditionally used for ML, or at least Poly/ML, is that of a
sequence of files compiled in a defined order with each file providing some
context for its successors. The context generally includes declarations in
the global name space but can include other context such as the current
working directory. This makes it more difficult for the IDE to know exactly
what context to use for a particular source file. The reason this is
important is that we want to be able to compile a source file when the user
edits it so that the IDE can provide information about internal types and
that's only possible if all the top-level declarations that the file expects
are available.
This traditional ML model of "incremental compilation", i.e. compilation
that is intertwined with execution, is exactly what is required for
applications like Isabelle. It is one of the reaons why we could never
use separate compilation versions of ML like MLton or MLkit.
An "Isabelle project" (which is called "session" in our terminology)
consists of a collection of theory files that may also "use" ML text,
either as separate files or embedded into our source format. This works
by our own runtime invocation of the Poly/ML compiler.
For our ongoing Isabelle IDE efforts, we essentially assume that ML
compilation can be invoked frequently and works more or less in real time
(Poly/ML compilation is quite fast, especially if compared to the time for
checking specifications and proofs in Isabelle.)
Fundamentally, the issue is how far should the user be required to
change existing source code and manner of working in order to be able to
use the IDE. Must each file contain just one top-level declaration?
Is a file allowed to call OS.FileSys.chDir to change the current
directory? Can a file declare its own version of "use" by wrapping up
PolyML.compiler and then compiling some files with it? This is less of
an issue for new code but there's a lot of existing code around.
In Isabelle/ML we now more or less assume that there are no chdirs and no
side effects on refs. We are lucky enough to can afford this in our
specific framework, which provides its own ways to manage context data
without side effects.
Makarius
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
