Isabelle is usually positioned 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).
The ML IDE functionality of Isabelle + Poly/ML is manifold:
Continuous feedback from static analysis and semantic evaluation is already available for years, e.g. Isabelle2014 (August 2014). It is a corollary of how PIDE interaction works, and of the integration of the Poly/ML compiler into that framework. Source files are statically checked and semantically evaluated while the user is editing. The annotated sources contain markup about inferred types, references to defining positions of items etc.
Source-level debugging within the IDE is new in Poly/ML 5.6, which is bundled with Isabelle2016 (February 2016). 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. See also here.
IDE support for the Isabelle/Pure bootstrap process is new technology for the coming release of Isabelle2016-1 (December 2016). The ROOT.ML file acts like a quasi-theory in the context of theory ML_Bootstrap: this allows continuous checking of all loaded ML files. The theory file is presented with a modified header to import Pure from the running Isabelle instance.
It is also possible to modify standalone SML projects, to edit the sources freely in the ML IDE. For example, MetiTarski can participate after some trivial changes of its ROOT.ML file.
Overall, we move more and more to an integrated framework for development of formal-reasoning tools, but other applications are admissible as well.
The Slides are available, together with their sources (which are required for the live system demo).
Interactive theorem proving was historically tied to the read-eval-print loop, with sequential and synchronous evaluation of prover commands given on the command-line. This user-interface technology was adequate when Robin Milner introduced his LCF proof assistant in the 1970s, but today it severely restricts the potential of multicore hardware and advanced IDE front-ends.
The Isabelle Prover IDE breaks this loop and retrofits the read-eval-print phases into an asynchronous model of document-oriented proof processing. Instead of feeding a sequence of commands into the prover process, the primary interface works via edits over immutable document versions. Execution is implicit and managed by the prover in a timeless and stateless manner, making adequate use of parallel hardware.
PIDE document content consists of the theory sources (with dependencies via theory imports), and auxiliary source files of arbitrary user-defined format: this allows to integrate other languages than Isabelle/Isar into the IDE. A notable application is the Isabelle/ML IDE, which can be also applied to the system itself, to support interactive bootstrapping of the Isabelle/Pure implementation.
Further tool integration works via “asynchronous print functions” that operate on already checked theory sources. Thus long-running or potentially non-terminating processes may provide spontaneous feedback while the user is editing. Applications range from traditional proof state output (which often consumes substantial run-time) to automated provers and dis-provers that report on existing proof document content (e.g. Sledgehammer, Nitpick, Quickcheck in Isabelle/HOL). It is also possible to integrate “query operations” via additional GUI panels with separate input and output (e.g. for manual Sledgehammer invocation or find-theorems).
Thus the Prover IDE orchestrates a suite of tools that help the user to write proofs. In particular, the classic distinction of ATP and ITP is overcome in this emerging paradigm of Integrated Theorem Proving.
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.
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
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.
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.
The forthcoming release of Isabelle2016 provides substantial refinements of the Isar proof language, after many years. This is a consequence of clarification of Isar internals, in order to support the Eisbach proof method language (by Dan Matichuk et al).
These Slides provide an overview for Isabelle users who know classic Isabelle/Isar already.