Email Gateway (Aug 22 2022 at 16:11): Email Gateway (Aug 22 2022 at 16:11):From: Lars Hupel <hupel@in.tum.de>
Dear Makarius,
what is the official way (from Isabelle/Scala) to invoke an Isabelle
tool without exiting the JVM? For example, if I want to invoke a
sequence of tools.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:11):From: Makarius <makarius@sketis.net>
Most Isabelle command-line tools are indeed implemented in
Isabelle/Scala today, but the tool wrapper assumes that it is the only
(or last) thing that this JVM runs. Thus the JVM will finally exit,
after printing exceptions properly without "Java vomit". See also the
module Command_Line (both in Scala and ML).
So multiple invocations of the tool wrapper require a separate process
each time. This can be done in Isabelle/Scala by the
Isabelle_System.bash operation, e.g. like this:
Isabelle_System.bash("isabelle build").check
Note that PATH within the Isabelle environment has $ISABELLE_HOME/bin
first, so "isabelle" above refers to the running Isabelle installation.
Further not that operations like File.bash_path and Bash.string help to
compose bash scripts reliably.
Another possibility (often better) is to invoke the underlying Scala
operations within the running JVM process. Every Isabelle tool should
have such an entry as a regular function, with typed interface and
normal exception behavior.
E.g. for the above that is Build.build, which I often use in the
Isabelle/Scala console of Isabelle/jEdit, in the absence of proper IDE
support for the build process.
Makarius
Email Gateway (Aug 22 2022 at 16:11):From: Lars Hupel <hupel@in.tum.de>
So multiple invocations of the tool wrapper require a separate process
each time. This can be done in Isabelle/Scala by the
Isabelle_System.bash operation, e.g. like this:Isabelle_System.bash("isabelle build").check
Thanks, I have used that now.
Another possibility (often better) is to invoke the underlying Scala
operations within the running JVM process. Every Isabelle tool should
have such an entry as a regular function, with typed interface and
normal exception behavior.
In this particular case it is about invoking a "dynamic" Scala script
from the AFP, so there's no Scala entry point visible statically.
With the ever-increasing importance of Isabelle/Scala as a systems
language (and thus, for the AFP), we should consider a more robust and
less ad-hoc way of adding Scala tools to the classpath from within
components.
Lars
Email Gateway (Aug 22 2022 at 16:11):From: Makarius <makarius@sketis.net>
On 04/10/17 16:01, Lars Hupel wrote:
In this particular case it is about invoking a "dynamic" Scala script
from the AFP, so there's no Scala entry point visible statically.
That is particularly slow, because the full Scala compiler needs to make
a cold start.
With the ever-increasing importance of Isabelle/Scala as a systems
language (and thus, for the AFP), we should consider a more robust and
less ad-hoc way of adding Scala tools to the classpath from within
components.
That is an old problem. Presently, I only know some partial solutions:
* Isolate general tool functionality and move that to the
Isabelle/Pure.jar (after the usual process of "change elimination" to
trim it down to the very core).
* Maintain an external tool-specific jar (e.g. via "isabelle scalac")
and add the result to the Isabelle classpath in the etc/settings of the
tool component directory. The Bash function "classpath" does that
properly; the only problem is to build the jar on the spot. Maybe the
build process is better done offline.
Makarius
Email Gateway (Aug 22 2022 at 16:11):From: Lars Hupel <hupel@in.tum.de>
That is particularly slow, because the full Scala compiler needs to make
a cold start.
Right. I don't know whether I have mentioned this before or not, but
<https://github.com/martylamb/nailgun> is a prime candidate to avoid
such problems.
* Isolate general tool functionality and move that to the
Isabelle/Pure.jar (after the usual process of "change elimination" to
trim it down to the very core).
Possibly. Feel free to have a look at "$AFP_BASE/tools" for what is
happening there.
* Maintain an external tool-specific jar (e.g. via "isabelle scalac")
and add the result to the Isabelle classpath in the etc/settings of the
tool component directory. The Bash function "classpath" does that
properly; the only problem is to build the jar on the spot. Maybe the
build process is better done offline.
I just tried doing that out of curiosity, but it seems that "$JAVA_HOME"
is not set in "etc/settings"; consequently, "isabelle_scala scalac"
fails. I'm not yet sure whether I'm doing something wrong there.
Lars
Last updated: May 01 2024 at 20:18 UTC