Email Gateway (Aug 19 2022 at 12:27): Email Gateway (Aug 19 2022 at 12:27):From: René Neumann <rene.neumann@in.tum.de>
There is 'isabelle findlogics', which gives me a list of all heaps. Is
there some equivalent for sessions? Or would it be possible to add a
switch to 'isabelle build'? So that e.g.
isabelle build -d . -L
just prints the list of sessions it can find?
Reason: Have a script select one from the list and pass it on as
'isabelle jedit -l $SESSION'
If it is not possible per se, but there is already some workaround
needing some scripting, I'd be fine with this too.
Email Gateway (Aug 19 2022 at 12:27):From: Makarius <makarius@sketis.net>
On Tue, 12 Nov 2013, René Neumann wrote:
There is 'isabelle findlogics', which gives me a list of all heaps.
findlogics is one of these obsolete Proof General tools. Its result is
not well-defined, it merely lists files that happen to lie around in
certain directories.
Is there some equivalent for sessions? Or would it be possible to add a
switch to 'isabelle build'? So that e.g.isabelle build -d . -L
just prints the list of sessions it can find?
Reason: Have a script select one from the list and pass it on as
'isabelle jedit -l $SESSION'If it is not possible per se, but there is already some workaround
needing some scripting, I'd be fine with this too.
You can either try to find suitable letter soups for "isabelle build" to
approximate in the shell what you have in mind, or use Isabelle/Scala as
the system programming language that it was meant to be. The "system"
manual has a brief entry on the "Scala script wrapper".
Then you are in statically typed Isabelle/Scala, with access to the
isabelle.Build module etc. So you can do "higher-order object-oriented
scripting" there with the official Isabelle/Scala interfaces.
Makarius
Email Gateway (Aug 19 2022 at 12:28):From: René Neumann <rene.neumann@in.tum.de>
I just came up with this little Scala-snippet, that seems to do what I
need (first time ever I touched Scala):
val options = isabelle.Options.init()
val path = isabelle.Path.explode("/home/necoro/cava")
val sessions = isabelle.Build.find_sessions(options, List((false, path)))
sessions.graph.keys.foreach{ s => print(s + " ") }
println
Unfortunately, this is rather slow. Both the startup (ie running
isabelle_scala_script), and also the Options.init() and find_sessions().
I don't know yet, if I want this to be called from a shell script.
Email Gateway (Aug 19 2022 at 12:29):From: Makarius <makarius@sketis.net>
On Tue, 12 Nov 2013, René Neumann wrote:
Reason: Have a script select one from the list and pass it on as
'isabelle jedit -l $SESSION'
I just came up with this little Scala-snippet, that seems to do what I
need (first time ever I touched Scala):
So far the question what you actually need was left open.
Isabelle/jEdit already provides a dialog to select the logic image, and it
is rebuilt automatically on startup. The reboot is a bit awkward, but it
should usually do the job.
Unfortunately, this is rather slow. Both the startup (ie running
isabelle_scala_script), and also the Options.init() and find_sessions().
By making a cold start from outside the Isabelle system, e.g. from the
shell, several startup-penalties are adding up: Scala script compilation,
JVM runtime warmup etc.
There are ways to reduce this a bit, although I am myself not an expert of
all the options to scalac and java runtime.
The general move in recent years is away from Isabelle command-line tools,
and towards the assumption that you have the Prover IDE already running
and do things from there.
Makarius
Email Gateway (Aug 19 2022 at 12:29):From: René Neumann <rene.neumann@in.tum.de>
I want jEdit to start right up with the correct session. This
Scala-snippet would mostly be needed for sanity-checks ("does the
session you want me to pass to jEdit exist"), and hence not doing them
is ok. The other usecase was that calling my script with a unique
substring of the session name was sufficient. But I rarely use this, and
if I really will, the dialog in jEdit should take care of it.
Last updated: Apr 24 2024 at 12:33 UTC