Albert Jiang reports:

I recently found that there might be a potential bug with scala-isabelle. Although I cannot be sure whether it was a bug or that my execution was faulty.

In the following is a very simple script that initialises an isabelle process and then destroys it.

package pisa.server

import _root_.java.nio.file.Path
import de.unruh.isabelle.control.Isabelle

object TestIsa {
  val setup: Isabelle.Setup = Isabelle.Setup(isabelleHome = Path.of("/Applications/Isabelle2020.app/Isabelle"),
    sessionRoots = Nil,
    userDir = None,
    logic = "HOL",
    workingDirectory = Path.of("./"),
    build=false
  )

  implicit val isabelle: Isabelle = new Isabelle(setup)

  println("Initialised isabelle")
  def main(args: Array[String]): Unit = {
    Thread.sleep(10000)
    isabelle.destroy()
    println("Destroyed isabelle")
    Thread.sleep(100000)
  }
}

However, if you execute the code, you will find that there is a poly process that can be caught by the activity manager to use ~400MB of memory and persists even after isabelle is destroyed or even the scala application terminates. I have to kill the process manually.

I wonder if you think this is a bug? Or is there something I didn't do properly to cause the memory issue?

Thanks for the nice tool, and it works very well before I met this problem.

I am trying to prove the following theorem using the sledgehammer.

theory Test imports Main HOL.HOL HOL.Real Complex_Main  
begin
theorem fixes r :: real assumes r: "r >= 0" and "r^3 = 8" 
shows "r = 2"
proof-
  have eq1: "r = root 3 8" using assms sledgehammer 
  by (simp add: real_root_pos_unique) 
  show ?thesis sledgehammer
  by (simp add: eq1) 
qed 

This simple theorem can be proved when using vscode isabelle plugin; while it failed for normal_with_Sledgehammern.
The theorem proving is conducted on the same machine, and I have set
[("provers", "cvc4 vampire verit e spass z3 zipperposition"),("timeout","60"),("verbose","true")]

Is there something I didn't do properly?

Use the table from Isabelle2021-1 once released.

The following two ways of creating ToplevelState variable are inconsistent, the first one works fine with Isabelle2021, but the second one throws an exception.

// first one
// as in https://github.com/dominique-unruh/scala-isabelle/blob/master/src/test/scala/de/unruh/isabelle/experiments/TheoryManager.scala
val init_toplevel = compileFunction0[ToplevelState]("Toplevel.init_toplevel")
var toplevel = init_toplevel().force.retrieveNow

// second one
// with implicit Isabelle defined
val toplevel = ToplevelState()

The second way is supported after 0.4.2 release, and it works fine with version 2021-1 and 2022, but not with 2021. The error messages are as follows:

[scala-execution-context-global-26] ERROR de.unruh.isabelle.mlvalue.MLValue - Error while compiling value "(E_Option o Option.map (E_String)) ((Isabelle_System.isabelle_identifier()) : ((string) option))":
de.unruh.isabelle.control.IsabelleMLException: ML error:
Value or constructor (isabelle_identifier) has not been declared in structure Isabelle_System, when compiling let open Control_Isabelle val result = ((E_Option o Option.map (E_String)) ((Isabelle_System.isabelle_identifier()) : ((string) option))) in store 57 result end
	at de.unruh.isabelle.control.IsabelleMLException$.unsafeFromId(Isabelle.scala:1076)
	at de.unruh.isabelle.control.DefaultExceptionManager.createException(ExceptionManager.scala:43)
	at de.unruh.isabelle.control.Isabelle.$anonfun$parseIsabelle$3(Isabelle.scala:292)
	at java.base/java.util.concurrent.ForkJoinTask$RunnableExecuteAction.exec(ForkJoinTask.java:1426)
	at java.base/java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:290)
	at java.base/java.util.concurrent.ForkJoinPool$WorkQueue.topLevelExec(ForkJoinPool.java:1020)
	at java.base/java.util.concurrent.ForkJoinPool.scan(ForkJoinPool.java:1656)
	at java.base/java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1594)
	at java.base/java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:183)

Basically, it complains that Isabelle_System.isabelle_identifier is not defined.
Indeed, isabelle_identifier is not declared in Isabelle_System (src/Pure/System/isabelle_system.ML) in Isabelle2021, but the only place that it is accessed seems to be in

which is wrapped within a try block. So, not sure if this is a bug of scala-isabelle or Isabelle2021.

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

It would be useful to add the following at the beginning of the example (I was running in an ammonite REPL). The full name de.unruh.isabelle.pure is needed due to clash with isabelle.control.isabelle.

import de.unruh._, isabelle.control._
import de.unruh.isabelle.pure._
import java.nio.file._
implicit val ec: scala.concurrent.ExecutionContext = scala.concurrent.ExecutionContext.global