Category Archives: PIDE

Coq/PIDE public beta

The first public beta of Coq/PIDE was released by Carst Tankink just a few days ago. See also the announcement on the coq-club mailing list from 26-Nov-2014.

Building it manually from individual parts was a bit tricky, but knowing in theory how things should fit together, I managed after two failed attempts. Note that COQBIN really needs an extra slash at the end, or the Makefile will break down.

Here is a screenshot of Coq/jEdit on Linux with GTK look-and-feel, editing a medium-sized file from the Coq library:

Coq-jEdit

There is an important conceptual difference to Isabelle/jEdit, which edits a whole project (or “session”) with many files active at the same time within the same prover process.

In contrast, Coq has capitalized separate compilation a long time ago, so it is likely that its one-to-one relation of files versus sessions (with a separate coqtop for each) will remain in years to come.

Update 02-Feb-2015: Carst Tankink has just announced the second public beta Coq/jEdit 0.2.0 for Coq 8.5beta1.

Flattr this!

Isabelle/PIDE as IDE for Standard ML

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

SML-PIDE

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

Flattr this!