Re: [isabelle] Isabelle2021-1-RC2: Exception when initializing services



On 09/11/2021 09:06, Dominique Unruh wrote:
> 
> The reason is the following:
> 
> Isabelle_System.make_services calls isabelle.setup.Build.get_services with
> every classpath element. get_services calls new JarFile if that classpath
> element exists in the filesystem. However, if the classpath element exists but
> is a directory, then new JarFile raises an exception.

> I assume the easiest fix would be to invoke new JarFile only on regular files
> (i.e., replace Files.exists(jar_path) by Files.isRegularFile(jar_path) in
> get_services). This would simply ignore directory-classpath-elements (i.e.,
> services can only be loaded from jars but Isabelle does not fail in the
> presence of directory-classpath-elements).

OK, I have made this more robust via Files.isRegularFile here:
https://isabelle-dev.sketis.net/rISABELLEcba1da393958ac15a155abaadf5d3472705d83ff


Can you say where the directory in the your classpath is coming from?

Note that the isabelle.setup module is a step towards better integration (or
assimilation) of Java/Scala into Isabelle (not Isabelle into Java/Scala).
There will be further steps after the coming release, e.g. jars as exports
within the session database --- e.g. for services that build the document.

The current state is documented in the "system" manual, see "isabelle
scala_project" and "isabelle scala_build". The "build.props" file is where
everything comes together.


	Makarius




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