How to set up Isabelle session from existing ROOT file in Java

[mi-ki]

Thanks very much for the nice tool and the ongoing development!

Disclaimer: For a Scala developer, this might be a trivial question, but since the comment within your JIsabelle class encouraged to file an issue for convenient wrappers, you and/or others might still consider my issue worthwhile.

I have some Java code that attempts to interact with my Isabelle session based on its ROOT file and the according theories. For an older version of scala-isabelle, I was setting it up the following way:

final List<Path> sessionDirs = new LinkedList<Path>();
sessionDirs.add(Path.of(new File(sessionDirectory).getAbsolutePath()));

Setup setup = new Setup(Path.of(isabelleHomeDirectory),
                        sessionName,
                        new Some<Path>(Path.of(isabelleHomeUserDirectory)),
                        Path.of(sessionDirectory),
                        JavaConverters.asScalaIteratorConverter(sessionDirs.iterator()).asScala().toSeq(),
                        true, null);

try {
    isabelle = new Isabelle(setup);
} catch (/* IsabelleBuild */final Exception e) {
    // Scala has no checked Exceptions and the constructor is not annotated.
    // Therefore, javac thinks that the (implicitly checked) IsabelleBuildException
    // cannot be thrown.
    e.printStackTrace();
    System.out.println("Building session " + sessionName + " failed.");
}
Isabelle isabelle = new Isabelle(setup);
// ... then further code to extract theories, theorems, functions, definitions, etc. from loaded session

However, the current version of scala-isabelle does not have the same setup method so that this code does not work anymore. Moreover, the two additional parameters (exceptionManager and isabelleCommandHandler) require a bit more Scala knowledge and your Java example only considers using the wrappers within the JIsabelle class. Hence, I wondered whether you could either advise on how to instrument one of those wrappers for my needs or advise on how a wrapper for it could be implemented. If there are any further issues within my instrumentation of scala-isabelle, I would also be happy for any advice!

I am thankful for any advice in this matter!

Best regards, Michael

[dominique-unruh]

Your example can probably be made to work by giving the defaults isabelle -> new DefaultExceptionManager(isabelle) and data -> Isabelle.defaultCommandHandler to those two new arguments (untested). This is derived by translating the default values from https://javadoc.io/doc/de.unruh/scala-isabelle_2.13/latest/de/unruh/isabelle/control/Isabelle$.html#SetupextendsIsabelle.SetupGeneralwithProductwithSerializable into Java syntax.

However, this leads to brittle Java code. (In Scala, one can address the individual parameters by name. In Java, this is not possible.) So I will add more methods of the form JIsabelle.setupSetXXX to cover this use case.

[dominique-unruh]

I added some additional methods in JIsabelle that should cover your use case (in the master branch). The release version will contain them shortly after Isabelle2023 is released.

[dominique-unruh]

@mi-ki Version v0.4.2-RC1 has the changes. Let me know if they solve your problem.

[mi-ki]

Dear Dominique,

thanks a lot for the quick reply, and sorry for coming back to you so late! Your updates were very helpful to me and solved the biggest part of my problem. The only additional thing I needed was the following addition (which was straightforward when seeing the additions which you had provided before), since I want to use theorems from a pre-existing session:

/** Sets the [[de.unruh.isabelle.control.Isabelle.Setup.logic logic]] directory in the setup `setup`.
   *
   * @return `setup` with [[de.unruh.isabelle.control.Isabelle.Setup.logic logic]] set to `logic`
   * @param logic the new value for `setup.`[[de.unruh.isabelle.control.Isabelle.Setup.logic logic]]
   * */
  def setupSetLogic(logic: String, setup: Isabelle.Setup): Isabelle.Setup =
    setup.copy(logic = logic)

So many thanks for your help!

[dominique-unruh]

@mi-ki I overlooked that one, apparently. I'll add this, unless you prefer to make a pull request with that change.