Room Schützenberger, bâtiment Turing, École Polytechnique, Palaiseau, 13 February 2014, 14:00-18:00
Participants: Bruno Barras, Pierre Courtieu, Lourdes del Carmen Gonzalez Huesca, Carst Tankink, Enrico Tassi, Makarius Wenzel, Burkhart Wolff.
Welcome to Carst Tankink.
Discussion about the definition of a protocol to connect the PIDE of Coq and Isabelle; it may include the work of Makarius presented his last article. Bruno suggested to use the plug-in of Isabelle and make some changes to adapt it for Coq. Burkhart explained the document model and Makarius gave a detailed explanation of the PIDE modules. The PIDE uses two API, one of high level which manages the snapshots updates and one at low level that communicate the document updates with the existing protocol for Isabelle; it is suggested to add one similar for Coq.
Enrico presented the updates to the asynchronous interaction mode with a demo showing the work of the Require command.