Re: [isabelle] Isabelle/Eclipse prover IDE released!
On Wed, 17 Apr 2013, René Neumann wrote:
4a.) Allow to use the logics in ~/.isabelle/Isabelle-yyyy/heaps, so that
I can use them directly without 'session dirs'.
You can build sessions into your home directory by selecting "Build
sessions to user home directory" in Build tab of Isabelle launch
configuration. Or do you mean that the dialog should look for additional
heaps already pre-built there and list them in the session selection?
The latter. Because then, my current setup (ROOT.ML + build.sh) would
still work, and I wouldn't need any session directories.
I am not sure how much Isabelle.Build tool covers this
(Isabelle/Eclipse just provides a UI for it).
Well ... there still is `isabelle findlogics`. But I don't know, how
this is implemented.
This sounds all very ancient, even before the IsaMakefile/usedir setup
that was used between 1997 and 2012. Isabelle2013 still has some remains
of the old stuff, but there is no point to go back to it. (Files that
happen to lie around in some directory are not a proper session.)
Andrius was rather quick to pick up the isabelle.Build Scala module, which
is standard session management component of Isabelle2013. Quite
impressive work what he did in Isabelle/Eclipse.
I feel motivated to trash the old IsaMakefile/usedir scripting stuff
rather soon. Then users merely have to spend 15min reading the Isabelle
system manual, and then save a lot of everyday build time.
This archive was generated by a fusion of
Pipermail (Mailman edition) and