Makarius Wenzel

Makarius Wenzel

Isabelle/jEdit is the main application of the Prover IDE (PIDE) framework and the default user-interface of Isabelle, but it is not limited to theorem proving. This paper explores possibilities to use it as a general IDE for formal languages that are defined in user-space, and embedded into informal text documents. It covers overall document structure with auxiliary files and document antiquotations, formal text delimiters and markers for interpretation (via control symbols). The ultimate question behind this: How far can we stretch a plain text editor like jEdit in order to support semantic text processing, with support by the underlying PIDE framework?

Makarius Wenzel

This is an updated system description for Isabelle/jEdit, according to the official release Isabelle2014 (August 2014). The following new PIDE concepts are explained: asynchronous print functions and document overlays, syntactic and semantic completion, editor navigation, management of auxiliary files within the document-model.

Makarius Wenzel

The LCF tradition of interactive theorem proving, which was started by Milner in the 1970-ies, appears to be tied to the classic READ-EVAL-PRINT-LOOP of sequential and synchronous evaluation of prover commands. We break up this loop and retrofit the read-eval-print phases into a model of parallel and asynchronous proof processing. Thus we explain some key concepts of the Isabelle/Scala approach to prover interaction and integration, and the Isabelle/jEdit Prover IDE as front-end technology. We hope to open up the scientific discussion about non-trivial interaction models for ITP systems again, and help getting other old-school proof assistants on a similar track.

Makarius Wenzel

Isabelle/PIDE is the current Prover IDE technology for Isabelle. It has been developed in ML and Scala in the past 4-5 years for this particular proof assistant, but with an open mind towards other systems. PIDE is based on an asynchronous document model, where the prover receives edits continuously and updates its internal state accordingly. The interpretation of edits and the policies for proof document processing are determined by the prover. The editor front-end merely takes care of visual rendering of formal document content. Here we report on an experiment to connect Coq to the PIDE infrastructure of Isabelle. This requires to re-implement the core PIDE protocol layer of Isabelle/ML in OCaml. The payload for semantic processing of proof document content is restricted to lexical analysis in the sense of existing CoqIde functionality. This is sufficient as proof-of-concept for PIDE connectivity. Actual proof processing is then a matter of improving Coq towards timeless and stateless proof processing, independently of PIDE technicalities. The implementation worked out smoothly and required minimal changes to the refined PIDE architecture of Isabelle2013. This experiment substantiates PIDE as general approach to prover interaction. It illustrates how other provers of the greater ITP family can participate by following similar reforms of the classic TTY loop as was done for Isabelle in the past few years.

Makarius Wenzel

PIDE is a general framework for document-oriented prover interaction and integration, based on a bilingual architecture that combines ML and Scala. The overall aim is to connect LCF-style provers like Isabelle (or Coq or HOL) with sophisticated front-end technology on the JVM platform, overcoming command-line interaction at last. The present system description specifically covers Isabelle/jEdit as part of the official release of Isabelle2011-1 (October 2011). It is a concrete Prover IDE implementation based on Isabelle/PIDE library modules (implemented in Scala) on the one hand, and the well-known text editor framework of jEdit (implemented in Java) on the other hand. The interaction model of our Prover IDE follows the idea of continuous proof checking: the theory source text is annotated by semantic information by the prover as it becomes available incrementally. This works via an asynchronous protocol that neither blocks the editor nor stops the prover from exploiting parallelism on multi-core hardware. The jEdit GUI provides standard metaphors for augmented text editing (highlighting, squiggles, tooltips, hyperlinks etc.) that we have instrumented to render the formal content from the prover context. Further refinement of the jEdit display engine via suitable plugins and fonts approximates mathematical rendering in the text buffer, including symbols from the TeX repertoire, and sub-/superscripts. Isabelle/jEdit is presented here both as a usable interface for current Isabelle, and as a reference application to inspire further projects based on PIDE.

Makarius Wenzel, Burkhart Wolff

The Isabelle/PIDE platform addresses the question whether proof assistants of the LCF family are suitable as technological basis for educational tools. The traditionally strong logical foundations of systems like HOL, Coq, or Isabelle have so far been counter-balanced by somewhat inaccessible interaction via the TTY (or minor variations like the well-known Proof General / Emacs interface). Thus the fundamental question of math education tools with fully-formal background theories has often been answered negatively due to accidental weaknesses of existing proof engines. The idea of "PIDE" (which means "Prover IDE") is to integrate existing provers like Isabelle into a larger environment, that facilitates access by end-users and other tools. We use Scala to expose the proof engine in ML to the JVM world, where many user-interfaces, editor frameworks, and educational tools already exist. This shall ultimately lead to combined mathematical assistants, where the logical engine is in the background, without obstructing the view on applications of formal methods, formalized mathematics, and math education in particular.