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



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.




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