Category Archives: Coq

The Isabelle Prover IDE after 9 years of development, and beyond

On Mon 24-Jul-2017, I gave a presentation at the BigProof event in Cambridge. Title: The Isabelle Prover IDE (PIDE) after 9 years of development, and beyond. Abstract:

The main ideas around Isabelle/PIDE go back to summer 2008. This is an overview of what has been achieved in the past 9 years, with some prospects for the future. Where can we go from here as Isabelle community? (E.g. towards alternative front-ends like Visual Studio Code; remote prover sessions “in the cloud”; support for collaborative editing of large formal libraries.) Where can we go as greater ITP community (Lean, Coq, HOL family)?

Here are some notable VSCode projects that were briefly mentioned in the talk:

Social Networks in the Isabelle and Coq community

Here is an interesting (draft) paper about Social Network structures in the Isabelle and Coq community, based on the main mailing lists of the two systems:

J. Fleuriot, S. Obua, Ph. Scott: Social Network Processes in the Isabelle and Coq Theorem Proving Communities. arXiv:1609.07127, September 2016.

Just a few comments of mine:

  • The isabelle-users mailing list is still the main forum for Isabelle users, but Stackoverflow is gaining more and more importance. Note that I helped to bring it in form in Mar-2013 (earning a badge for 30 days of continuous activity :-), but I am rarely participating there now, because I am too busy with the classic mailing lists.
  • The seasonal peaks on isabelle-users in Fig. 1 are due to the release process, which happens approx. every 8-10 months. In 2012, I started to make discussion of release candidates fully public on isabelle-users; before it was confined to isabelle-dev, which is also open to everyone, but has fewer participants.
  • Page 12: “This seems to indicate that there is some clear separation of expertise when it comes to the tool.” This is correct and follows a general principle of Isabelle development: there are areas of undisputed “experts” for certain parts of the system. Thus there is a clear responsibility to make that thrive in the long term. Often this assignment is a consequence of starting that area in the first place, or investing significant work in upgrading it (e.g. by a designated PhD or research project). My recurring appearance on Sledgehammer threads is mainly technological: I am responsible for underlying infrastructure for parallel ML programming and the Prover IDE; it also overlaps with overall system integration and release management due to the add-on ATP and SMT systems.
  • In recent years, I have economized my appearance on isabelle-users as follows:
    1. Incoming messages are marked as important, when the topic overlaps with my areas of expertise. I rarely answer on the spot.
    2. After some days, weeks, or months, I revisit marked message and make sure that questions are actually answered, or add a few remarks to discussion threads.
    3. During the release candidate phases, I revisit all marked messages back to the previous release (or even one before that), to make sure that old technical problems are solved or remain in a reasonably well-defined state.

    This means the mailing list also serves as an “issue tracker”. I’ve made some experiments with an explicit tracker just for the release process, but there was very little participation. Trackers tend to become a long-term storage for well-known and unresolved problems.

Release of Coq 8.5

On 21-Jan-2016 Coq 8.5 has been released, with an unusually long distance of about 3.5 years to Coq 8.4.

Coq 8.5 is notable for having a little bit of PIDE (Prover IDE) support (by Enrico Tassi), without using that name nor the Scala-based PIDE library of Isabelle. It is all based on OCaml, and connects to the regular CoqIde frontend.

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.