Re: [isabelle] Calling Isabelle tools without exiting



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.