Email Gateway (Nov 09 2021 at 08:15): Email Gateway (Nov 09 2021 at 08:15):From: Dominique Unruh <unruh@ut.ee>
Hi,
when initializing Isabelle in a situation where the classpath contains a
directory (not only jars), and exception is thrown. (This can happen,
for example, if Isabelle is initialized via Isabelle/Scala in a project
that does not have a pure JAR classpath.)
java.io.FileNotFoundException:
/home/unruh/svn/qrhl-tool/scala-isabelle/target/scala-2.13/test-classes
(Is a directory)
at java.base/java.io.RandomAccessFile.open0(Native Method)
at
java.base/java.io.RandomAccessFile.open(RandomAccessFile.java:343)
at
java.base/java.io.RandomAccessFile.<init>(RandomAccessFile.java:258)
at
java.base/java.io.RandomAccessFile.<init>(RandomAccessFile.java:213)
at java.base/java.util.zip.ZipFile$Source.<init>(ZipFile.java:1260)
at java.base/java.util.zip.ZipFile$Source.get(ZipFile.java:1225)
at
java.base/java.util.zip.ZipFile$CleanableResource.<init>(ZipFile.java:706)
at java.base/java.util.zip.ZipFile.<init>(ZipFile.java:240)
at java.base/java.util.zip.ZipFile.<init>(ZipFile.java:171)
at java.base/java.util.jar.JarFile.<init>(JarFile.java:349)
at java.base/java.util.jar.JarFile.<init>(JarFile.java:320)
at java.base/java.util.jar.JarFile.<init>(JarFile.java:286)
at PIDEWrapper@1//isabelle.setup.Build.get_services(Build.java:342)
at
PIDEWrapper@1//isabelle.Isabelle_System$.from_jar$1(isabelle_system.scala:81)
at
PIDEWrapper@1//isabelle.Isabelle_System$.$anonfun$make_services$4(isabelle_system.scala:83)
at
PIDEWrapper@1//scala.collection.immutable.List.flatMap(List.scala:293)
at
PIDEWrapper@1//isabelle.Isabelle_System$.make_services(isabelle_system.scala:83)
at
PIDEWrapper@1//isabelle.Isabelle_System$.init(isabelle_system.scala:89)
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).
Best wishes,
Dominique.
Email Gateway (Nov 09 2021 at 10:52):From: Makarius <makarius@sketis.net>
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
Email Gateway (Nov 09 2021 at 11:42):From: Dominique Unruh <unruh@ut.ee>
Yes, we've had long discussions about the obsolete scala-isabelle
library already.
I would disagree that it is obsolete.
At least not in the sense that there is a different approach that covers
the same needs, to my knowledge.
The core Isabelle framework, as far as I can tell, covers the following
use cases well:
* Invoking Scala code from a standalone Isabelle process (e.g.,
Isabelle services)
* Invoking Isabelle from other tools as a more-or-less standalone
process with coarse operations (such as building a session)
What is not supported (as far as I can tell) is:
* Running an Isabelle process as a slave to an existing application
(where the application has its own toplevel interface, be it GUI,
command line, or REPL).
* Invoking fine grained operation (e.g., constructing a term, proving
a theorem).
If there is a mechanism that covers those things, then I'd be happy to
use that mechanism. (Ideally, scala-isabelle would be nothing than a
simpler to use helper library that just passes through everything to
Isabelle/Scala.)
I'm also happy to use the "proper way" of invoking Isabelle inside the
library.
(Note that, if I wouldn't use the library, I would still have exactly
the same problems because in the qrhl-tool theorem prover, I need to
invoke Isabelle, and if I do it by calling Isabelle/Scala directly, I
will still have exactly the same questions.)
Best wishes,
Dominique.
Last updated: Apr 24 2024 at 16:18 UTC