Room Flageolet, bâtiment Turing, École Polytechnique, Palaiseau, 3 October 2013, 9:30-14:00
Participants: Bruno Barras, Pierre Courtieu, Lourdes del Carmen Gonzalez Huesca, Enrico Tassi, Makarius Wenzel, Burkhart Wolff.
Enrico presented the current trunk version in the repository of Coq, linked up with CoqIde. It is based on a 1-server n-slave approach sitting in own UNIX processes, and message passing to communicate the necessary proof states before starting the local checking activities in the slaves. Although unoptimized and not yet connected to the PIDE framework, it is already quite useable. When the Coq release finally gets out (not before next year), the user will actually have a quite sensible speed-up even for "real proofs" resulting from work of this project.
Makarius basically implemented what was called in the project definition "asynchronous agent framework for Sledgehammer & Co" under the new name "asynchronous printing functions". The ITP paper contains new measurements. A number of other optimizations have been undertaken - among other things a kernel modification that simplifies the sub-context test implementation (slides).
Burkhart presented key aspects of the Kernel model in Isabelle. The model works on:
Discussion for preparing the review meeting.