larsrh / libisabelle Goto Github PK

A Scala library which talks to Isabelle (DISCONTINUED)

License: Apache License 2.0

Java 0.13% Isabelle 0.31% Scala 98.57% Shell 0.11% Standard ML 0.59% CSS 0.23% OCaml 0.01% Ruby 0.01% HTML 0.03% Python 0.01%

scala isabelle

libisabelle's Introduction

libisabelle

As a possible replacement for this library, check out scala-isabelle.

libisabelle's People

Stargazers

Watchers

Forkers

wneuper fthomas rklaehn gitter-badger alexarchambault dominique-unruh scala-steward

libisabelle's Issues

P.O.S.T.

When Isabelle is loaded with the wrong configuration (i.e. a configuration which doesn't include libisabelle-protocol), nothing happens when trying to send a request.

Solution: Try to make an initial request upon creating a System with a short timeout. If it doesn't succeed, call it invalid.

Change link in repo description to https

You should change the link in the description from http://lars.hupel.info/libisabelle, which rendered poorly, to https://lars.hupel.info/libisabelle/ which looks awesome.

I only found out because the README links to the nice https link. In addition (or alternatively) you can make the, I assume, CSS work in http.

Support Isabelle 2019

Currently, Isabelle2019-RC4 is supported (under Linux), but Isabelle2019 not yet. (See also #78)

In certain cases, libisabelle fails to remove etc/components.
The consequence is that subsequent builds of Isabelle fail.
The following sequence of commands leads to that error (with libisabelle 0.9.2)

  val version = Version.Stable("2017")
  val localStoragePath = Paths.get("/tmp/isabelle-temp")

  val platform : Platform = Platform.guess match {
    case Some(p) => p.withLocalStorage(localStoragePath)
  }

  val setup : Setup = Setup(Paths.get("/tmp/xxx"), platform, version)

  val resources = Resources.dumpIsabelleResources() match {
    case Right(r) => r
  }

  val environment = Await.result(setup.makeEnvironment(resources, Nil), Duration.Inf)

Now there is a file /tmp/isabelle-temp/user/Isabelle2017/.isabelle/Isabelle2017/etc/components (that should be removed by an invocation of Environment.cleanEtcComponents()).

2018-RC1 incompatibility

I think there is an incompatibility between Isabelle 2018-RC1 and libisabelle-1.0.0-RC2.
From the build process:

### theory "Protocol.Common"
### 0.270s elapsed time, 0.475s cpu time, 0.000s GC time
*** Failed to load theory "Protocol.Codec_Class" (unresolved "Classy.Classy")
*** Failed to load theory "Protocol.Protocol" (unresolved "Protocol.Codec_Class")
*** Failed to load theory "HOL-Protocol.HOL_Operations" (unresolved "Protocol.Protocol")
*** Failed to load theory "Protocol.ML_Expr" (unresolved "Protocol.Protocol")
*** Failed to load theory "Protocol.Basic" (unresolved "Protocol.Protocol")
*** Failed to load theory "HOL-Protocol.Protocol_Main" (unresolved "HOL-Protocol.HOL_Operations", "Protocol.Basic", "Protocol.ML_Expr")
*** Failed to load theory "QRHL-Protocol.QRHL_Operations" (unresolved "HOL-Protocol.Protocol_Main")
*** ML error (line 199 of "/tmp/libisabelle_resources5894943446203832053/classy/ml_types.ML"):
*** Value or constructor (ml_env_context) has not been declared
*** ML error (line 206 of "/tmp/libisabelle_resources5894943446203832053/classy/ml_types.ML"):
*** Value or constructor (context_set_thread_data) has not been declared
*** ML error (line 207 of "/tmp/libisabelle_resources5894943446203832053/classy/ml_types.ML"):
*** Value or constructor (secure_use_text) has not been declared
*** At command "ML_file" (line 45 of "/tmp/libisabelle_resources5894943446203832053/classy/Classy.thy")
[main] DEBUG info.hupel.isabelle.api.Environment - QRHL-Protocol: Unfinished session(s): QRHL-Protocol

I am not 100% sure it's libisabelle's fault, but it happened when I changed the Isabelle version from 2018-RC0 to 2018-RC1.

Async lock does not get released

libisabelle/modules/libisabelle/src/main/scala/Platform.scala

Line 134 in c2ae5f2

f().map { a =>

isabellectl: --fresh-user in combination with build does not rebuild heap files

When I run isabellectl --version 2016 --session HOL jedit, that builds the HOL heap image. However, when I then run isabellectl --version 2016 --session HOL --fresh-user build, the image is not rebuilt as expected. Running isabellectl --version 2016 --session HOL --fresh-user jedit, on the other hand, does rebuild the image as expected.

Local storage cannot be symlinked

When the local storage path (configured, e.g., via Platform.withLocalStorage) is a symlink to an existing directory, Setup.detect fails with a FileAlreadyExistsException.

This is because Platform.acquireLock calls Files.createDirectories which (in accordance with its Javadoc description) fails when the directory already exists but is not a directory (but a symlink).

A fix should probably be to prefix the call to Files.createDirectorieswith if (!Files.isDirectory(localStorage))
(see https://docs.oracle.com/javase/7/docs/api/java/nio/file/Files.html#isDirectory(java.nio.file.Path,%20java.nio.file.LinkOption...) )

refined plugin

Add bindings for @fthomas' refined library.

Progress

convert Scala values to Isabelle (#24)
make term codecs more robust (don't choke on <, > and YXML nested inside terms) (eacd998)
libisabelle-refined subproject (WIP)
make the protocol available as a JAR file (huge yak) (#32)
resident Isabelle process (in SBT, via JNDI?)

Use consistent executor services

Executor services are all over the place.

Codec.string should fail on chars >=256

Currently, Codec.string.encode will send any string passed to it to Isabelle.

However, Isabelle can only handle character codes 0-255. Anything else leads to a Chr exception being thrown in Isabelle. (By function Char.chr.)

For example system.invoke(Operation.Hello)("α") will fail.

I think Codec.string.encode should already raise an exception if the input contains chars >=256 since otherwise one gets a hard to track down exception (The exception from Char.chr comes without any information why this exception is raised.)

Runtime extensibility of Codec.exn

Currently, exceptions thrown in operations are encoded using Codec.exn before being sent to the invoking Scala code. Codec.exn basically just uses @{make_string}. This is a useful default for unknown exceptions, but it means that we can get quite unreadable error messages on the Scala side, such as Par_Exn [CONTEXT (<context>, ERROR "Failed to apply initial proof method <markup>:\n<markup>")].

To avoid this, it would be useful to be able to overwrite behavior of Codec.exn. Two solutions come to mind:

Very simple: Codec.string_of_exn is made into a reference, and a function is exported in Codec that allows to replace Codec.string_of_exn with own code. (This might not be the nicest way but it would be sufficient for my purposes.)
Better, slightly more complex: Add a function for converting exceptions to string in Codec, and Codec.string_of_exn simply uses the first function that returns SOME string. @{make_string} is used as a fallback.

Rewrite XML ↔ YXML conversion

(see XML.scala)

Should use a more functional style, or maybe parser combinators.

This is a starter issue. Pull requests are welcome, and I'm happy to assist in implementing this.

Update coursier to 1.0.x

Can't run `bootstrap` twice in a row in SBT shell

https://stackoverflow.com/q/34107672/4776939

Missing operations in ML causes Scala future to hang

Reason is simple: When ML looks up an operation and finds none, it raises an exception that doesn't get passed through to Scala.

Setup.makeEnvironment throws an exception if setup is incomplete

This can be reproduced by creating an empty setup directory:

$ rm -rf .local/share/libisabelle/setups/Isabelle2015/
$ mkdir -p .local/share/libisabelle/setups/Isabelle2015/

Now, running this program

val version = Version("2015")
val setup = Setup.defaultSetup(version)
val env = setup.flatMap(_.makeEnvironment)
Await.result(env, Duration.Inf)

yields the following exception

java.lang.reflect.InvocationTargetException
        at sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
        at sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:62)
        at sun.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
        at java.lang.reflect.Constructor.newInstance(Constructor.java:422)
        at edu.tum.cs.isabelle.Implementations$.makeEnvironment(Implementations.scala:40)
        at edu.tum.cs.isabelle.Implementations$$anonfun$makeEnvironment$2.apply(Implementations.scala:110)
        at edu.tum.cs.isabelle.Implementations$$anonfun$makeEnvironment$2.apply(Implementations.scala:110)
        at scala.Option.map(Option.scala:146)
        at edu.tum.cs.isabelle.Implementations.makeEnvironment(Implementations.scala:110)
        at edu.tum.cs.isabelle.setup.Setup$$anonfun$makeEnvironment$1.apply(Setup.scala:171)
        at edu.tum.cs.isabelle.setup.Setup$$anonfun$makeEnvironment$1.apply(Setup.scala:169)
        at scala.util.Success$$anonfun$map$1.apply(Try.scala:237)
        at scala.util.Try$.apply(Try.scala:192)
        at scala.util.Success.map(Try.scala:237)
        at scala.concurrent.Future$$anonfun$map$1.apply(Future.scala:235)
        at scala.concurrent.Future$$anonfun$map$1.apply(Future.scala:235)
        at scala.concurrent.impl.CallbackRunnable.run(Promise.scala:32)
        at scala.concurrent.impl.ExecutionContextImpl$AdaptedForkJoinTask.exec(ExecutionContextImpl.scala:121)
        at scala.concurrent.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260)
        at scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.pollAndExecAll(ForkJoinPool.java:1253)
        at scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1346)
        at scala.concurrent.forkjoin.ForkJoinPool.runWorker(ForkJoinPool.java:1979)
        at scala.concurrent.forkjoin.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:107)
Caused by: java.io.IOException: Cannot run program "/home/frank/.local/share/libisabelle/setups/Isabelle2015/bin/isabelle": error=2, No such file or directory
        at java.lang.ProcessBuilder.start(ProcessBuilder.java:1048)
        at isabelle.Isabelle_System$.raw_execute(isabelle_system.scala:284)
        at isabelle.Isabelle_System$.init(isabelle_system.scala:122)
        at edu.tum.cs.isabelle.impl.Environment.<init>(Environment.scala:13)
        at sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
        at sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:62)
        at sun.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
        at java.lang.reflect.Constructor.newInstance(Constructor.java:422)
        at edu.tum.cs.isabelle.Implementations$.makeEnvironment(Implementations.scala:40)
        at edu.tum.cs.isabelle.Implementations$$anonfun$makeEnvironment$2.apply(Implementations.scala:110)
        at edu.tum.cs.isabelle.Implementations$$anonfun$makeEnvironment$2.apply(Implementations.scala:110)
        at scala.Option.map(Option.scala:146)
        at edu.tum.cs.isabelle.Implementations.makeEnvironment(Implementations.scala:110)
        at edu.tum.cs.isabelle.setup.Setup$$anonfun$makeEnvironment$1.apply(Setup.scala:171)
        at edu.tum.cs.isabelle.setup.Setup$$anonfun$makeEnvironment$1.apply(Setup.scala:169)
        at scala.util.Success$$anonfun$map$1.apply(Try.scala:237)
        at scala.util.Try$.apply(Try.scala:192)
        at scala.util.Success.map(Try.scala:237)
        at scala.concurrent.Future$$anonfun$map$1.apply(Future.scala:235)
        at scala.concurrent.Future$$anonfun$map$1.apply(Future.scala:235)
        at scala.concurrent.impl.CallbackRunnable.run(Promise.scala:32)
        at scala.concurrent.impl.ExecutionContextImpl$AdaptedForkJoinTask.exec(ExecutionContextImpl.scala:121)
        at scala.concurrent.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260)
        at scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.pollAndExecAll(ForkJoinPool.java:1253)
        at scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1346)
        at scala.concurrent.forkjoin.ForkJoinPool.runWorker(ForkJoinPool.java:1979)
        at scala.concurrent.forkjoin.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:107)
Caused by: java.io.IOException: error=2, No such file or directory
        at java.lang.UNIXProcess.forkAndExec(Native Method)
        at java.lang.UNIXProcess.<init>(UNIXProcess.java:248)
        at java.lang.ProcessImpl.start(ProcessImpl.java:134)
        at java.lang.ProcessBuilder.start(ProcessBuilder.java:1029)
        at isabelle.Isabelle_System$.raw_execute(isabelle_system.scala:284)
        at isabelle.Isabelle_System$.init(isabelle_system.scala:122)
        at edu.tum.cs.isabelle.impl.Environment.<init>(Environment.scala:13)
        at sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
        at sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:62)
        at sun.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
        at java.lang.reflect.Constructor.newInstance(Constructor.java:422)
        at edu.tum.cs.isabelle.Implementations$.makeEnvironment(Implementations.scala:40)
        at edu.tum.cs.isabelle.Implementations$$anonfun$makeEnvironment$2.apply(Implementations.scala:110)
        at edu.tum.cs.isabelle.Implementations$$anonfun$makeEnvironment$2.apply(Implementations.scala:110)
        at scala.Option.map(Option.scala:146)
        at edu.tum.cs.isabelle.Implementations.makeEnvironment(Implementations.scala:110)
        at edu.tum.cs.isabelle.setup.Setup$$anonfun$makeEnvironment$1.apply(Setup.scala:171)
        at edu.tum.cs.isabelle.setup.Setup$$anonfun$makeEnvironment$1.apply(Setup.scala:169)
        at scala.util.Success$$anonfun$map$1.apply(Try.scala:237)
        at scala.util.Try$.apply(Try.scala:192)
        at scala.util.Success.map(Try.scala:237)
        at scala.concurrent.Future$$anonfun$map$1.apply(Future.scala:235)
        at scala.concurrent.Future$$anonfun$map$1.apply(Future.scala:235)
        at scala.concurrent.impl.CallbackRunnable.run(Promise.scala:32)
        at scala.concurrent.impl.ExecutionContextImpl$AdaptedForkJoinTask.exec(ExecutionContextImpl.scala:121)
        at scala.concurrent.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260)
        at scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.pollAndExecAll(ForkJoinPool.java:1253)
        at scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1346)
        at scala.concurrent.forkjoin.ForkJoinPool.runWorker(ForkJoinPool.java:1979)
        at scala.concurrent.forkjoin.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:107)

Removing the Isabelle2015 directory and running the above program again fixes the problem.

It seems that this happened to me because the first download of Isabelle2015 was incomplete (there was only an empty ANNOUNCE file). It would be nice if libisabelle would check if a setup is complete before running bin/isabelle.

No proper error message if resources are missing

libisabelle/modules/setup/src/main/scala/Resources.scala

Line 97 in ea0649b

val in = classLoader.getResourceAsStream(s".libisabelle/$file")

After this line, I think it would be good to check if in==null, and, if so, output an error (this happens if the resource does not exist). That should make it easier to track down errors w.r.t missing resources.

Better tutorial/examples needed

Are there any more extensive tutorial available? I only see "hello world" example, and it only seems to show how to run a single thy file.

Looking at the code there must be more functionality provided by the library. What does this library do? Can one use this library to submit proof statement by statement to isabelle and get back diagnostics?

Are there projects that use libisabelle that I could use as example?

Support Isabelle 2019 release candidate

Is it possible to support RC0 (and follow-ups) to do early testing with the new release candidate?

Switch to Apache license

Needs consent by:

@alexarchambault (coursier code)

Cross-release doesn't work anymore

since about v0.9.1

Proper downloading of files

Uses URLConnection right now, which is a blocking API.

`validateSlow` builds both 2016 and 2016-1

Can we mention libisabelle in cats' README?

in the list of cats ecosystem projects.

Isabelle threads should be daemon threads

When an Isabelle instance has been created (using System.create), several threads are started for communicating with Isabelle. These are all non-daemon threads. This means that when the main program ends, the JVM does not return but waits indefinitely.

The following snippets shows the threads that keep the JVM from exiting:

    import scala.collection.JavaConverters._
    val threadSet = Thread.getAllStackTraces.keySet.asScala
    for (t <- threadSet if !t.isDaemon)
      println(t.getName)

The output is:

standard_error
standard_output
process_manager
command_input
message_output
process_result
main

Only main should be a non-daemon thread.

(Of course, one can always exit via sys.exit, but that puts the burden on the developer to make sure all possible execution paths end with sys.exit.)

Protocol_Main breaks simplifier

In the following code, the by simp command fails, even though test_def is a simplifier rule.
When replacing imports Protocol_Main by imports Main, the by simp command works.
(This problem also occurs when one programatically access the simplifier via libisabelle.)

theory Scratch  
  imports Protocol_Main
begin
  
definition test where "test (x::int) = x"
declare test_def[simp]
  
lemma test2: "a=1 ⟶ test a=1"
  by simp

Detection whether theory Protocol loaded does not work

When starting an Isabelle session (using Isabelle 2018), the message "Protocol theory not contained in image, scheduling to be loaded ..." is logged. If the resource component is not loaded, there is even an error "protocol not loaded but component not registered", even if the Protocol theory is in the session image.

I suspect the reason is the check

    if (loaded.contains("Protocol"))

in info.hupel.isabelle.api.Environment.protocolTheory. I assume it should be "Protocol.Protocol" for Isabelle 2018.

Manually creating environments is unsafe

From the implementation of Implementations.makeEnvironment, as of 185db1b:

def makeEnvironment(home: Path, clazz: Class[_ <: Environment]): Environment =
  clazz.getConstructor(classOf[Path]).newInstance(home)

This is unsafe in the sense that the limitation of Environments apply (documented in the scaladoc):

/**
 * Users may instantiate implementations manually, although there is a caveat:
 * After one implementation has been instantiated, the behaviour of subsequent
 * instantiations with a different path or instantiations of a different
 * implementation is undefined. For most applications, this is not a
 * significant restriction, because they only deal with a single setup.
 */

Now, makeEnvironment is explicitly marked as "low-level". However, there should at least be a safety check.

Proposal: A mutable WeakHashMap in the companion of Environment, mapping Class[_ <: Environment] objects to the paths with which they have been instantiated. Fail at runtime if they don't match.

Caveat: That map probably needs to be wrapped into Collections.synchronizedMap.

Test XML ↔ YXML conversion

Currently completely without unit/property tests. Only the integration tests in LibisabelleSpec exercise the parser and printer.