[isabelle] Isabelle as an SML environment and IDE

[Aleks Kissinger]

It recently came up on the Poly/ML mailing list that Isabelle/jEdit
makes a pretty efficient SML IDE these days. I manage a fairly large
SML project called Quantomatic, so I thought I'd have a go at getting
a setup to work. I've got a setup now that I am pretty happy with, so
I thought I'd share my results. Hopefully other people will find this
helpful.

Quantomatic is fairly unique in that it is designed to run inside of
Isabelle or as a standalone project. As a result, the whole codebase
is implemented on top of an Isabelle/ML-like environment, obtained by
importing chunks of the ML code in Pure. This can be done by copying
src/Pure from Isabelle 2014 into an SML project and using this file:

https://github.com/Quantomatic/quantomatic/blob/integration/core/isabelle_env.ML

In the past, we used a slightly hacked-up version of Pure, but for the
sake of maintainability, we now use an exact copy.

The project itself is loaded with special "thy" files that only
contain comments and "ML_file" commands. These can be run from inside
Isabelle/jEdit (in the "real" Isabelle/ML environment), or they can be
imported in poly/ML with the function "use_thy":

https://github.com/Quantomatic/quantomatic/blob/integration/core/use_thy.ML

This implements a baby version of the outer syntax parser, which
ignores imports and translates the ML_file commands into use
statements. This makes the external ROOT.ML tiny and easy to maintain:

https://github.com/Quantomatic/quantomatic/blob/integration/core/ROOT.ML

This can be executed with, e.g. "poly --use ROOT.ML"

[Omar Montano Rivas]

Really useful. Thanks for sharing.

Best,
Omar.

Post by Aleks Kissinger
It recently came up on the Poly/ML mailing list that Isabelle/jEdit
makes a pretty efficient SML IDE these days. I manage a fairly large
SML project called Quantomatic, so I thought I'd have a go at getting
a setup to work. I've got a setup now that I am pretty happy with, so
I thought I'd share my results. Hopefully other people will find this
helpful.
Quantomatic is fairly unique in that it is designed to run inside of
Isabelle or as a standalone project. As a result, the whole codebase
is implemented on top of an Isabelle/ML-like environment, obtained by
importing chunks of the ML code in Pure. This can be done by copying
https://github.com/Quantomatic/quantomatic/blob/integration/core/isabelle_env.ML
In the past, we used a slightly hacked-up version of Pure, but for the
sake of maintainability, we now use an exact copy.
The project itself is loaded with special "thy" files that only
contain comments and "ML_file" commands. These can be run from inside
Isabelle/jEdit (in the "real" Isabelle/ML environment), or they can be
https://github.com/Quantomatic/quantomatic/blob/integration/core/use_thy.ML
This implements a baby version of the outer syntax parser, which
ignores imports and translates the ML_file commands into use
https://github.com/Quantomatic/quantomatic/blob/integration/core/ROOT.ML
This can be executed with, e.g. "poly --use ROOT.ML"