dominique-unruh / scala-isabelle Goto Github PK
View Code? Open in Web Editor NEWA Scala library for controlling/interacting with Isabelle
Home Page: https://dominique-unruh.github.io/scala-isabelle
License: MIT License
A Scala library for controlling/interacting with Isabelle
Home Page: https://dominique-unruh.github.io/scala-isabelle
License: MIT License
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?
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
scala-isabelle/src/main/scala/de/unruh/isabelle/mlvalue/Version.scala
Lines 35 to 40 in 545fe4e
which is wrapped within a try block. So, not sure if this is a bug of scala-isabelle or Isabelle2021.
I'd like to use scala-isabelle to call sledgehammer/try on an open proof of an existing theory.
To this end I've been trying to workout how the sledgehammer experiment in this repo could be transferred from Scala to Java.
But I've found a few oddities like BooleanConverter, StringConverter, etc... not extending the Converter Class for their respective types.
Is there a way to call sledgehammer from Java?
Use the table from Isabelle2021-1 once released.
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?
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
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
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.