Makarius wrote:
On Fri, 19 Jun 2009, David Matthews wrote:
We're not yet at the point of releasing this although much of the code
is in SVN so it is possible to try it out. A major issue we're
struggling with is exactly what constitutes a "project". For other
languages and IDEs there's a clear distinction between compilation and
run-time. With ML, though, compilation involves execution.
Typically, a project will involve calling "use" on various files but
"use" is actually being executed. Creating an ML structure also
involves execution.
Even in more mainstream IDEs, the "project management" often does not
work as smoothly as it should. For example, I often find myself
"rebooting" Netbeans/Scala just to get in sync with external changes to
sources or jars. Whatever we will do for Isabelle (which integrates
theory sources with ML programs), we intend to do better :-)
I've not had problems with the IDEs I've used, such as Visual Studio for
C++ and Eclipse for Java.
The issue for an IDE for ML is that traditionally there has been a lot
more freedom about what an ML file can contain and what it may expect
than is true for a C or Java file. A C source file has to be
self-contained; the only context is provided by include files. That
means the IDE can compile files independently.
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.
Anyway, concerning the most basic "use" functionality in Poly/ML, for us
the main question is about global effects. Since Poly/ML already allows
the client (Isabelle) to provide an implementation of the ML environment
(for toplevel types, vals, structures etc.), the remaining question is
how to handle updates on references.
In your own IDE implementations I have seen the use of saved heap images
to achieve undoable global state. I wonder if this could be somehow
internalized, e.g. heap snapshots as plain ML values?
The current mechanism we're using is that there is a project file that
lists the source files and one of those files is marked as the root.
That file can be compiled in the standard Poly/ML compiler and it
typically contains "use" calls that compile the remainder of the files
in some order determined by the user. There is a special "project
build" phase that runs this but with a modified version of "use" that
saves the state of Poly/ML just before each file is compiled in a
project directory. By loading the appropriate saved state the IDE can
re-establish the context if the user subsequently starts editing one of
the files. Using a saved state means that both declarations and ref
values are saved and restored to the appropriate values. The current
working directory still needs to be saved and restored separately since
that's not in the saved state.
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.
Regards,
David.
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
