Isabelle applications (e.g. from AFP) are growing steadily in size and number. To outline requirements and possibilities of the technology, I have produced a document on Scaling Isabelle Proof Document Processing.

Abstract:

This is a study of performance requirements, technological side-conditions, and possibilities for scaling of formal proof document processing in Isabelle and The Archive of Formal Proofs (AFP). The approaches range from simple changes of system parameters and basic system programming with standard APIs to more ambitious reforms of Isabelle and the underlying Poly/ML system. The running examples for typical scalability issues are existing formalizations of classical analysis and differential equations. Such applications can be further extrapolated towards a development of Financial Mathematics (e.g. Itô calculus).

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.

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 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.

Strictly speaking the Isabelle environment is for interactive and automated theorem proving, but its SML IDE support is quite sophisticated: 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.

As a quick start, see the Documentation panel, section Examples, entry src/Tools/SML/Examples.thy (as of Isabelle2014).

The time where SML sources need to be edited with vi or emacs are over. See also this related thread on Stackoverflow.