Category Archives: Isabelle

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!

Intelligible semi-automatic reasoning in December 2015

A presentation on old and new aspects of Isabelle/Isar will happen 04-Dec-2015 10:00 at Univ. Bonn (Workgroup of Prof. Koepke). See also the web page of Oberseminar mathematische Logik.

Abstract:

Isabelle was introduced in 1989 (by L. Paulson) as a generic logical framework for higher-order natural deduction. Intelligible semi-automated reasoning (Isar) was introduced in 1999 (by M. Wenzel) as a structured proof language for human-readable formal proof documents. Today, in December 2015, we see large applications of Isabelle/Isar in the Isabelle/HOL object-logic, e.g. in the Archive of Formal Proofs with more than 240 entries.

After so many years, development of Isar is still not finished. Recent refinements of old concepts and additions of new concepts include: structured rule statements (Eigen-contexts), multi-branch elimination (case-splitting), structured backwards refinement. The new Eisbach language (by D. Matichuk et al) allows to define complex proof methods in their usual syntax, instead of traditional Isabelle/ML. Sledgehammer (by J. Blanchette et al) allows to generate semi-intelligible Isar proofs from machine-generated proofs (via external ATPs and SMTs).

The ultimate aim of Isabelle/Isar is to turn the results of formal proof production into mathematical documents with nice type-setting. Document source was mainly written in LaTeX in the past, but is now moving towards Markdown, with specific GUI support in the Prover IDE (Isabelle/jEdit).

The Slides are available.

Flattr this!

Isabelle Tutorial at Bonn

A tutorial on Isabelle for students of mathematics will happen 03/04-Dec-2015 at Univ. Bonn (Workgroup of Prof. Koepke). The detailed schedule is available on the web page of Praktikum Mathematische Logik. The main language of the tutorial is German; materials are in English.

Notable topics

  • Isabelle/Pure as logical framework for Natural Deduction
  • Isabelle/Isar as proof language for formalized mathematics
  • Isabelle/ML as environment for developing tools for logic applications (including Prover IDE support)

Prerequisites

The tutorial uses the following snapshot of the emerging winter release: Isabelle_01-Dec-2015.

Moreover, a full installation of LaTeX is required (Linux: TeX Live via package manager, Windows: MiKTeX, Mac OS X: MacTeX).

Materials

Flattr this!

Isabelle Tutorial at CADE-25

A full-day tutorial on Isabelle will happen Saturday 01-Aug-2015 in Berlin, as an associated event of the 25th International Conference on Automated Deduction (CADE-25). Here is some further organizational information about tutorials at CADE-25. Important materials for the tutorial are available at the bottom of this post.

More than 25 years ago, Isabelle was initiated by Larry Paulson as a logical framework for rapid prototyping of Natural-Deduction proof systems. Today, Isabelle is one of the major platforms for Interactive Theorem Proving (ITP), with notable support for automated reasoning tools (ATPs and SMTs). Isabelle/HOL is the main environment for applications; it is accompanied by the Archive of Formal Proofs (AFP) as repository for user-contributions. Isabelle supports logical tool development in Isabelle/ML and Isabelle/Scala, but it is also possible to connect external tools; this works routinely on Linux, Windows, and Mac OS X. The system presents itself to the end-user by an advanced Prover IDE: Isabelle/jEdit.

The purpose of the tutorial is to get acquainted with Isabelle, using the latest release Isabelle2015 (May 2015). Topics cover specifications in HOL, proofs in Isar, use of automated provers via Sledgehammer etc. The target audience are doctoral students or researchers with an interest in formalized reasoning, application of reasoning tools for interactive and automated proof development, maybe even with an interest to develop their own tools with/for Isabelle.

There will be presentations by Makarius Wenzel and Christian Sternagel, with hands-on tutoring and exercises done by the participants on their own computers (at least 2 cores and 4 GB memory).

Materials

Flattr this!

Release candidates for Isabelle2015

The release of Isabelle2015 is scheduled for this spring, presumably the end of May, or the start of June. As usual, there are several weeks for thorough testing of release candidates that are available here:

With ever increasing size and complexity of the system and its many add-on tools, it is important to take testing of release candidates seriously. Problems can be solved before the release, not after it!

The main forum for discussion is on isabelle-users mailing list.

The convergence towards the final release happens on the following repository.

Update: The final release of Isabelle2015 (May 2015) is now available from the Isabelle website. The above release candidates will disappear eventually.

Flattr this!

Proposal: document preparation improvements

(See also general notes on proposals.)

Isabelle/Isar is ultimately about beatiful proof documents, not profane “proof scripts”. This explains why high-quality rendering of theory files in PDF-LaTeX has been part of the game from early on. In the past 15 years, the Isabelle document preparation system has been applied to produce numerous articles, books, theses etc. based on content that is formally checked in the logic (usually Isabelle/HOL). Here is an arbitrary example from AFP.
The Isabelle manuals are usually produced as Isabelle documents as well, e.g. see the sources in the directory src/Doc of the Isabelle distribution.

Traditional Isabelle document preparation is a side-effect of a session build process that is run in batch-mode; see also the Isabelle System manual, chapters 2 and 3. The main command-line tools for session management with document preparation are isabelle mkroot and isabelle build. This edit-typeset-preview cycle works, but feels a bit awkward today, where interactive theory and proof development with continuous checking in the Prover IDE (PIDE) is used routinely. So it his high time for various renovations and reforms of Isabelle document preparation as sketched below.

Immediate build process of documents within the Prover IDE.
There is no particular reason why LaTeX should be run via batch-mode tools on the command-line. The Prover IDE could take care of that interactively, with much shorter turnaround cycles of the edit-typeset-preview cycle. To achieve that, parts of the document preparation in Isabelle/ML need to be moved to Isabelle/Scala, and slightly generalized to become stateless and applicable to partial/unfinished document sources.
GUI panel for document preparation in Isabelle/jEdit.
This should allow to control document preparation in the IDE, e.g. to specify which parts of the document are presently interesting, or to change options for LaTeX and add-on tools.
Improved error reporting from LaTeX

LaTeX error output should be parsed and presented within the Prover IDE adequately, with proper error positions over the original source text. The notoriously obscure LaTeX log files need to be overcome.
Light-weight document markup as in Markdown / Commonmark with approximative preview in the source.
Instead of old-fashioned LaTeX markup like \begin{itemize} \item ... \end{itemize} there could be more direct indication of itemization in the source (with actual bullets from the Isabelle symbol repertoire). Using conventions from Markdown, it would approximate a preview of the final typesetting already in the source text. Enumerations and description lists could be done similarly. Note that there is no need for sections (which are already supported via explicit Isar commands), nor for hyperlinks and other formal inserts (which are already supported via document antiquotations).
Improved HTML output
A subset of document markup that fits into the limited Markdown / Commonmark format sketched above could be taken as starting point for better HTML presentation, with relatively modest ambitions and technical requirements. It is important to recall that “HTML” as such is a huge and vaguely defined collection of standards: producing portable output that looks nice on most browsers requires significant expertise or special tools, or both.

A few improvements have already made it into the repository after Isabelle2014. For example, the repository version Isabelle/872f330a0f8a provides support for BibTeX files in Isabelle/jEdit. In Isabelle/9986fb541c87 there is also support for @{cite} antiquotations, with formal links etc.

Flattr this!

Proposal: remote prover connectivity for Isabelle/PIDE

(See also general notes on proposals.)

“Cloud computing” is one of these buzzwords without any particular meaning, but the idea to run heavy-duty computations remotely is rather old: some “big-iron” in the background provides the CPU and memory resources for substantial applications, while the user interacts with the system via some small local terminal. Already in the classic days of Proof General (around 1999) it was common-place to run Emacs locally on a workstation and the prover process remotely on a server (via rsh). Alternatively it was possible to run both the editor and the prover remotely and use X11 as display protocol, which was especially important for the rather heavy XEmacs of that time.

This normal mode of distributed computing was almost forgotten, when the performance of local laptops and remote servers were approaching the same order of magnitude (due to the demands of the gaming industry). This was only an episode over a single decade, though, and we are already back to the traditional situation where local and remote machines can differ significantly. In 2014, typical mobile devices were limited to 2–8 CPU cores and 2–8 GB RAM. This is very little compared to low-end workstations or high-end servers, with something like 8–36 CPU cores and 32–512 GB RAM, or more.

Note that some big Isabelle applications already go beyond the possibilities of small machines with only 4–8 GB RAM, but for more memory Poly/ML process needs to be switched from 32-bit to 64-bit mode, which also doubles the memory demands. Thus there is a discontinuity here: stepping out of the “small device” category means to go for 16–32 GB RAM minimum.

This motivates the demand for remote prover connectivity for Isabelle and its Prover IDE (PIDE). The most basic approach is to run the internal socket connection for the PIDE protocol between ML and Scala over ssh. This should be sufficient for fast and reliable local networks. For non-local networks, there are the usual questions about bandwidth, latency, and reliability of the connection. The PIDE protocol requires relatively high bandwidth (which is easily provided by common DSL connections), but can afford high latency due to its asynchronous nature. Lack of reliability might turn out a real problem, though: resetting a lost TCP/IP connection naively means to restart the prover process and recheck the whole session from start, which could take minutes or hours.

Thus a more advanced approach would keep both the ML and Scala side of PIDE together on the server. Remote access then works via a separate PIDE display protocol, which is postulated here and still needs to be defined and implemented. Depending on active buffers and open text areas in the editor, the remote side would provide continuous access to incoming PIDE document markup, without demanding persistent management of the whole PIDE state locally. Loosing the connection would merely mean to reconnect the IDE to the remote Isabelle/Scala/ML component, which keeps running indefinitely.

Thus the mode of operation becomes more like the re-connection facility of VNC or RDP (but not X11). Of course it is already possible today with Isabelle2014 to use VNC or RDP for a completely remote ML/Scala/IDE process, but remote ML/Scala and local IDE would make this more comfortable for the user, with better graphics performance and reactivity.

Taking this perspective of remote PIDE sessions one step further could mean to support low-bandwidth, high-latency, unreliable connections of mobile networks: sitting on a train with a laptop and local IDE, while re-connecting to a remote PIDE session on a big server, would really count as cloud computing. We should think here of editing whole libraries like AFP on the spot, with immediate feedback. A bit more efforts will be required to get there, though.

In summary, the following stages are possible, depending on the amount of resources spent on this subject:

  1. Simple remote PIDE socket connection via ssh, usable for fast and reliable local networks. (The jEdit text editor already provides some means to manage ssh, so this merely requires the usual study of sources with subsequent tinkering and polishing to make it work smoothly.)
  2. Separate PIDE display protocol where the editor is local and the Isabelle/Scala/ML session is remote. This should be usable for fast DSL network connections.
  3. Support for smooth disconnection and re-connection for mobile networks.
  4. Development of a completely different PIDE front-end that works on tablets or smart-phones (Android or iOS).

The last point is speculative: it merely sketches to horizon of what could eventually be targeted, if there were lots of resources and several enthusiastic people working on it.

Flattr this!