CHANGELOG.md

Changelog

0.4.3 - 2024-???

The main change is support for Isabelle2024.

Added

• Support for Isabelle2024.
• Implicits.javaBooleanConverter, .javaIntConverter, .javaLongConverter: MLValue converters for the Java types Boolean, Integer, and Long. The Scala versions of these converters do not have the right types for use in Java.

Fixed

• Methods of Version did output some bogus error messages in Isabelle2021 and earlier.

0.4.2 - 2023-09-25

The main change is support for Isabelle2023.

Added

• Support for Isabelle2023.
• Position: New methods line, offset, endOffset, file, id to access the corresponding fields in the ML-type. extract, extractUntil to extract text from a string given position(s).
• TheoryHeader: New method name to get the name of the theory. read to parse a theory from a string.
• ToplevelState: New methods proofLevel, mode, isProofMode etc., proofStateDescription, localTheoryDescription. ToplevelState() creates a toplevel based on Pure.
• Transition: New Scala class. Represents A toplevel transition (roughly speaking one command in a theory file).
• JIsabelle: New methods setupSetVerbose, setupSetUserDir, setupSetWorkingDirectory, setupSetSessionRoots, setupSetLogic to set the corresponding fields in a Setup object from Java.

Changed

• Isabelle: Execution context is stored inside Isabelle instance, and configured via [Setup](https://javadoc.io/doc/de.unruh/scala-isabelle_2.13/0.4.2/de/unruh/isabelle/control/Isabelle$$Setup.html).executionContext. Most scala-isabelle methods now use that execution context.

Removed

None.

0.4.1 – 2022-11-27

Main changes are support for Isabelle2022 and improved support for handling of ML exceptions.

Added

• Support for Isabelle2022.
• Isabelle: Can configure a different ExceptionManager for handling exceptions in ML code (instead of raising IsabelleMLExceptions). See MLException.ExceptionManager for an alternative to the default.
• Added an ML value converter for IsabelleMLExceptions, see MLException.simpleIsabelleMLExceptionConverter and MLException.distinguishingIsabelleMLExceptionConverter.
• Symbols: Supporting Unicode subscript symbols when converting between Isabelle symbols and Unicode. (See constructor argument processSubSuper.)
• Symbols: Specify fallback translations for symbols (only used if the symbols table has no translation). (See constructor argument extraSymbolsLowPri.)
• Version.versionFromIsabelleDirectory: Guesses the version of an Isabelle distribution by looking at the Isabelle distribution directory (without initializing the Isabelle process).

Changed

• IsabelleException was renamed to IsabelleMLException. It is only used raised when exceptions occur in ML code. Use IsabelleMiscException for other purposes.
• IsabelleMLException contains the actual ML exception object
• IsabelleMLException: The exception message contains the associated data of the exception (e.g., a TERM exception will contain the terms in the message). This message is lazily computed when needed.
• Isabelle is initialized with quick_and_dirty flag true, this means imported theories can use sorry.

Removed

None

0.4.0 – 2021-12-27

The main changes are support up to Isabelle2021-1, and better invocation of the Isabelle process (takes into account ROOT files etc.).

Added

• String interpolators for creating Isabelle terms/types (see StringInterpolators)
• Support for up to Isabelle2021-1
• Added methods:
  • Term.fastType returns the type of a term (without type checking).
  • Context.setMode sets the syntax mode (pattern/schematic/abbrev) for parsing terms/types.
  • Theory.context returns a context for this theory.
  • Term.concreteRecursive / Typ.concreteRecursive converts a term/type recursively into a concrete term/type (i.e., represented fully inside the Scala process).
  • ToplevelState.apply initializes a new toplevel state based on a theory.
  • ToplevelState.context returns the proof context corresponding to a toplevel state.
• Debugging support:
  • Environment variable SCALA_ISABELLE_NO_CLEANUP: If set (values true or 1), the temporary directory created by scala-isabelle are not removed on exit.
  • Environment variable SCALA_ISABELLE_LOG_QUERIES: If set, all queries from scala-isabelle to the Isabelle are logged (see header comment in control_isabelle_logged.ml).
• In ML, exception Control_Isabelle.E_Data added to wrap ML type Control_Isabelle.data as an exception (for storing in the object store).

Changed

• The Isabelle process is invoked with full PIDE context. In particular, this means that sessions are properly initialized the same way as when running Isabelle directly, and theory files can be found without needing to register directories using Theory.registerSessionDirectories.
• Declarations in ML (e.g., via Isabelle.executeMLCode) do not affect the global Isabelle/ML namespace anymore but a separate namespace.
• Cterm.apply / Ctyp.apply avoid re-typechecking a term/typ that is already a cterm/ctyp when converting it to a cterm, when possible (optimization).
• IsabelleException decodes Isabelle symbols in error messages to Unicode for better printing.
• Term.apply / Typ.apply now support Unicode strings when parsing terms/types from strings.

Removed

• Setup.build is currently ignored. (Isabelle will always check all theory files whether a build is needed.)

0.3.0 – 2020-11-05

The biggest changes include support for Windows, multi-threaded execution in the Isabelle process, as well as support for more ML types.

Added

• Support for Windows (now runs on Linux, OS/X, Windows)
• MLValueWrapper: Utility class for adding support for new ML types (with corresponding Scala classes that simply reference them).
• AdHocConverter: Utility class for adding support for new ML types very quickly (like MLValueWrapper but with less boilerplate but also less customizability).
• Support for further ML types:
  • Position.T (class Position)
  • Thy_Header.header (class TheoryHeader)
  • Thy_Header.keywords (class Keywords)
  • Toplevel.state (class ToplevelState)
  • Path.T (Java's Path via PathConverter)
  • Mutex.mutex (class Mutex)
  • Proofterm.proof (experimental support, class Proofterm)
• Support for commands sent from Isabelle to Scala (via Control_Isabelle.sendToScala, handled by custom handler isabelleCommandHandler).
• Support for connecting to an already running Isabelle instance (experimental, no library support for establishin that connection, see SetupRunning).
• Class Isabelle supports to check/wait for successful initialization (by inheriting from FutureValue).
• Class Isabelle cleans resources (Isabelle process) after garbage collection (calling .destroy is optional).
• Java support:
  • Class JPatterns to allow pattern matching of terms/types in Java (based on java-patterns library).
  • JIsabelle.setupSetBuild to toggle the build flag of an Isabelle Setup.
• Added methods:
  • Utils.freshName for generating fresh (randomized) names.
  • Theory.mutex returns a mutex for synchronizing theory operations.
  • Thm.theoryOf and Context.theoryOf return theory behind a theorem/context.
  • Isabelle.checkDestroyed to assert that the Isabelle process is still available.
  • Theory.mergeTheories merges several theories into one.
• Supertrait PrettyPrintable for all classes that can invoke Isabelle for prettyprinting themselves.

Changed

• Execution of ML code in the Isabelle process is now multi-threaded. (Several operations triggered from the Scala side are automatically executed concurrently. Use Mutex if locking is needed.)
• Method pretty in classes Term, Typ, Thm return Unicode (instead of Isabelle's internal encoding with \<...> sequences). Use method prettyRaw if the old behavior is required.
• Class FutureValue was moved from package de.unruh.isabelle.mlvalue to de.unruh.isabelle.misc.
• Class Isabelle does not take constructor parameter build any more. Set this flag in Setup instead.
• Methods MLValue.Converter.exnToValue, .valueToExn, .mlType, MLStoreFunction, MLRetrieveFunction take additional implicit arguments of types Isabelle and ExecutionContext.

Removed

None

0.2.0 – 2020-10-01

The biggest changes include completed API documentation as well as improved support for loading theory files that are not in the session image.

Added

• API documentation completed.
• BigIntConverter and DataConverter: support for MLValue[BigInt], MLValue[Isabelle.Data]
• Theory.apply(Path): Allows to load Isabelle theories from a file.
• Theory.registerSessionDirectories, Theory.registerSessionDirectoriesNow: Register directories containing theory files. Required to find imports of theories.
• mlvalue.Version: Provides information about current Isabelle version.
• MLvalue.function0, MLValue.compileFunction0, MLFunction0: Support for MLFunctions with unit input.
• Term, Typ have method concreteComputed: Check whether concrete has already been computed (before, only MLValueTerm, MLValueTyp has this).
• MLFunction0 ... MLFunction7 now have unsafeFromId(ID). Before, they only has unsafeFromId(Future[ID]).
• MLValue.removeFuture: Converts Future[MLValue[A]] into MLValue[A] by moving the future inside the MLValue.
• Object JIsabelle with helper functions for accessing scala-isabelle from Java. (Not much in there yet.)

Changed

• Symbols.symbolsToUnicode, Symbols.unicodeToSymbols take additional optional argument failUnknown: Controls whether to silently ignore conversion errors.
• MLStoreFunction.apply: Removed implicit MLValue.Converter argument.
• MLValue.compileFunction: Implicit arguments renamed.
• Thm.cterm renamed to Thm.proposition: Returns the proposition of the theorem.
• TFree.apply, TVar.apply: The sort argument is now a Seq[String] instead of String*
• Type.unapply replaced by Type.unapplySeq: Use case Type(name, arg1, arg2, ...) instead of case Type(name, Seq(arg1, arg2, ...) now.
• Theory.importMLStructure takes only one argument now. The newName argument is gone, instead the new name of the imported structure is returned. (Two-argument version of Theory.importMLStructure is still available but deprecated.)
• Constructor argument of Isabelle.Setup have a different order. (Invocation using named arguments preferred.)

Removed

• MLRetrieveFunction.apply(ID), MLRetrieveFunction.apply(Future(ID)): Prefer the type-safe variant MLRetrieveFunction.apply(MLValue[A]). If the behavior of the removed functions is required, use MLRetrieveFunction.apply(MLValue.unsafeFromId(id)).
• MLValue.compileFunctionRaw: MLValue.compileFunction is type-safe and preferred. For low-level (unsafe) compilation, use MLValue.compileValueRawinstead.
• Cterm.mlValueTerm, Ctyp.mlValueTyp removed.