Category Archives: Isabelle

The Isar proof language in 2016

At the Isabelle Workshop 2016 in Nancy, I presented a paper about recent renovations of the Isar proof language:

This is a description of the Isar proof language as it stands today in 2016. This means the official release Isabelle2016 (February 2016), and the next release that is presumably published towards the end of the year. Relevant NEWS entries and updated portions from the Isabelle/Isar Reference Manual are summarized in one comprehensive article.

See also the full paper and the slides.

Flattr this!

Video for Isabelle presentation at Curry Club Augsburg

Another Isabelle presentation at Curry Club Augsburg (19-May-2016) has been recorded and uploaded to Youtube.

Materials from the presentation:

  • Exercise from Haskell Workshop 1 + 2 (Dec-2015).
  • Solution produced during the presentation.
  • Slides that were briefly shown towards the end.

To try it interactively (with Prover IDE markup), it is possible to open the URL of the Solution directly in Isabelle/jEdit.

Flattr this!

PIDE as Standard ML IDE for bootstrapping Isabelle

Isabelle is usually advertized as environment for interactive and automated theorem proving, but its Prover IDE (PIDE) may be used for regular program development as well. Standard ML is particularly important here, since it is the bootstrap language of Isabelle/ML (i.e. SML with many add-ons) and Isabelle/Pure (i.e. the logical framework).

Using Isabelle/PIDE for bootstrapping Isabelle itself is now possible in recent repository versions, e.g. Isabelle/1c1f8531ca37 – see also README_REPOSITORY for general explanations how to build and run that. Here is the relevant NEWS entry from that version:

IDE support for the Isabelle/Pure bootstrap process. The initial files src/Pure/ROOT0.ML or src/Pure/ROOT.ML may be opened with Isabelle/jEdit: they act like independent quasi-theories in the context of theory ML_Bootstrap. This allows continuous checking of ML files as usual, but results are isolated from the actual Isabelle/Pure that runs the IDE
itself.

The ML project consists of a sequence of ML_file commands in ROOT.ML. Projects other than Isabelle can do the same with SML_file for official Standard ML. Afterwards, the following Poly/ML command line is able to build the project without the IDE: poly --eval "val SML_file = PolyML.use" --use ROOT.ML

What is also notable in the Isabelle/Pure bootstrap environment is the structure Thread_Data for global state variables within the current thread. There are two implementations: (1) physical and (2) virtual. The virtual version is used when Isabelle/Pure is loaded into itself: it allows to manage many versions of the load process with different intermediate states in a value-oriented manner.

Flattr this!

Isabelle no longer supports SML/NJ

17-Feb-2016 marks the historic day when support for SML/NJ was removed from the Isabelle code base, see the main changeset and another changeset concerning ML multithreading.

The changes of the source illustrate the amount of conditional compilation that has accumulated in the past decades of Isabelle development. In the future, we will be able to proceed faster in just one direction, and pick up more advanced features of Poly/ML.

Already ten years ago, SML/NJ had little practical relevance for Isabelle users. It was occasionally used by tool developers to figure out difficult situations of type-inference, at a time when the SML/NJ compiler errors were better than the ones of Poly/ML. This has changed dramatically in recent years, with fairly good compiler errors and full IDE support in Poly/ML.

Performance of SML/NJ had always been a problem (after 1993): growing with the total heap size of Isabelle applications. This is inherent in the “CPS approach” of SML/NJ, see also this brief discussion on Stackoverflow.

The reason for giving up these tons of extra weight right after shipping Isabelle2016 are rather profane: in the routine tests of SML/NJ for the release, many basic Isabelle sessions (e.g. HOL-Library) no longer worked, running out of memory (within 32bit address space) after many hours.

Flattr this!

Announcing Isabelle2016

Isabelle2016 is now available.

This version improves upon Isabelle2015 in many ways, see the NEWS file in the distribution for further details. Some highlights are as follows:

  • Enhanced Isabelle/jEdit Prover IDE, with separate State versus Output panel and more asynchronous task management within the prover/GUI.
  • Additional Isar language elements for structured statements and proofs.
  • Document language refinements, with Markdown-like text structure.
  • More Isabelle symbols in theory and document sources.
  • Pure/HOL: uniform treatment of overloaded constant definitions versus type definitions; upgrade of HOL typedef to definitional principle.
  • HOL tool enhancements: Sledgehammer, Nitpick, Quickcheck, Transfer.
  • HOL library additions and improvements, notably HOL-Multivariate_Analysis, HOL-Probability, HOL-Data_Structures.
  • Upgrade to Poly/ML 5.6 with debugger IDE support (Isabelle/ML and Standard ML), per-thread profiling, native Windows version (32bit and 64bit).

You may get Isabelle2016 from the following mirror sites:

Flattr this!

ML debugging within the Prover IDE

Isabelle/ML is based on Poly/ML and thus benefits from the source-level debugger of that implementation of Standard ML. The Prover IDE provides the Debugger dockable to connect to running ML threads, inspect the stack frame with local ML bindings, and evaluate ML expressions in a particular run-time context. A typical debugger session is shown in the screenshot below.

[ML debugger]

ML debugging depends on the following pre-requisites.

  1. ML source needs to be compiled with debugging enabled. This may be controlled for particular chunks of ML sources using any of the subsequent facilities.

    1. The system option ML_debugger as implicit state of the Isabelle process. It may be changed in the menu Plugins / Plugin Options / Isabelle / General. ML modules need to be reloaded and recompiled to pick up that option as intended.
    2. The configuration option ML_debugger, with an attribute of the same name, to update a global or local context (e.g. with the declare command).
    3. Commands that modify ML_debugger state for individual files: ML_file_debug, ML_file_no_debug, SML_file_debug, SML_file_no_debug.

    The instrumentation of ML code for debugging causes minor run-time overhead. ML modules that implement critical system infrastructure may lead to deadlocks or other undefined behaviour, when put under debugger control!

  2. The Debugger panel needs to be active, otherwise the program ignores debugger instrumentation of the compiler and runs unmanaged. It is also possible to start debugging with the panel open, and later undock it, to let the program continue unhindered.

  3. The ML program needs to be stopped at a suitable breakpoint, which may be activated individually or globally as follows.

    For ML sources that have been compiled with debugger support, the IDE visualizes possible breakpoints in the text. A breakpoint may be toggled by pointing accurately with the mouse, with a right-click to activate jEdit’s context menu and its Toggle Breakpoint item. Alternatively, the Break checkbox in the Debugger panel may be enabled to stop ML threads always at the next possible breakpoint.

Note that the state of individual breakpoints gets lost when the coresponding ML source is re-compiled! This may happen unintentionally, e.g. when following hyperlinks into ML modules that have not been loaded into the IDE before.

The debugger panel (see screenshot) shows a list of all threads that are presently stopped. Each thread shows a stack of all function invocations that lead to the current breakpoint at the top.

It is possible to jump between stack positions freely, by clicking on this list. The current situation is displayed in the big output window, as a local ML environment with names and printed values.

ML expressions may be evaluated in the current context by entering snippets of source into the text fields labeled Context and ML, and pushing the Eval button. By default, the source is interpreted as Isabelle/ML with the usual support for antiquotations (like ML, ML_file). Alternatively, strict Standard ML may be enforced via the SML checkbox (like SML_file).

The context for Isabelle/ML is optional, it may evaluate to a value of type theory, Proof.context, Context.generic. Thus the given ML expression (with its antiquotations) may be subject to the intended dynamic run-time context, instead of the static compile-time context.

The buttons labeled Continue, Step, Step over, Step out recommence execution of the program, with different policies concerning nested function invocations. The debugger always moves the cursor within the ML source to the next breakpoint position, and offers new stack frames as before.

Flattr this!

Isabelle presentation at Curry Club Augsburg

On Thu 17-Mar-2016 there will be a presentation about “Programs and Proofs in Isabelle/HOL” at Curry Club Augsburg.

Start: approximately 19:30–20:00
Duration: approximately 60min
Language of the talk: German

Outline:

  • Isabelle and the LCF prover family: origin of ML (Meta-Language)
  • Isabelle as framework for domain-specific formal languages
  • Isabelle document preparation: formal LaTeX + Markdown
  • Isabelle/ML: tool implementation language
  • Isabelle/Scala: system programming language
  • “Programming” in Isabelle/HOL: the main Object-Logic
  • Example: list operations and induction proofs (with code-generation to SML, OCaml, Scala, Haskell)
  • Structured proofs in Isabelle/Isar
  • Example: Cantor’s Theorem in HOL
  • Example: Run-Length Encoding in HOL

Flattr this!

Release candidates for Isabelle2016

The coming Isabelle2016 release is scheduled for February 2016. This spot is continuously updated to inform about the ongoing process of testing release candidates.

  • On 01-Jan-2016 an informal snapshot Isabelle2016-RC0 was published. In this version, the website, NEWS, ANNOUNCE etc. are already mostly up-to-date. Some documentation is still lagging behind, notably the Isabelle/jEdit manual.
  • On 15-Jan-2016 the first formal release candidate Isabelle2016-RC1 was published. The main work is finished. Some documentation requires further revisions. We now need serious testing by users to expose remaining problems.
  • On 25-Jan-2016 the second release candidate Isabelle2016-RC2 was published. It includes the latest jdk-8u72 from Oracle: it is important to test this thoroughly on all platforms.
  • On 01-Feb-2016 the third release candidate Isabelle2016-RC3 was published. It includes the official Poly/ML 5.6 release. Some minor points have been polished in the Isabelle code base and documentation.
  • On 06-Feb-2016 the fourth release candidate Isabelle2016-RC4 was published. Some minor points have been improved in Sledgehammer and Isabelle/jEdit GUI reactivity.
  • On 12-Feb-2016 the fifth release candidate Isabelle2016-RC5 was published. It includes more material on Isar language updates in the isar-ref manual. Poly/ML 5.6 has been modified to use GNU bash for OS.Process.system, in order to help Debian-testing-unstable propagate the Isabelle settings environment – with shell functions, as documented in the bash man page!

As usual it is important to keep general laws of causality in mind: release candidates may still change, but the final release is final. So the best time to start testing is now!

The main forum for discussion of Isabelle2016 release candidates is on isabelle-users mailing list.

Update: The final release of Isabelle2016 (February 2016) is now available from the Isabelle website. The above release candidates will disappear eventually.

Flattr this!