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 + 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 MHonArc.