Agenda for Meeting at TUM to discuss PGIP, March 2007

DavidAspinall , ChristophLueth , CezaryKaliszyk will visit MakariusW .

• David will give a talk on Thu 14:00
• Cezary will give a talk on Fri 11:30

The audience will be the local Isabelle group, talks need not be long and can include a system demo.

• Thu night for dinner; again everybody from the Isabelle group is welcome to join.

Concerning the topics to be discussed in the inner circle, everybody should start to collect some thoughts. Please contribute them to this page in sections below and add any useful links, contents of old email discussions, etc. Feel free to make new pages for separate issues if it helps. To avoid going over old ground/motivations, etc, please also study the existing contents of this wiki under the PGIP page (some linked below), as well as the material at http://proofgeneral.inf.ed.ac.uk/Kit.

-- DavidAspinall - 23 Feb 2007

Refining and improving PGIP support in Isabelle, in time for Isabelle 2007

Issues here will be listed as tickets on http://proofgeneral.inf.ed.ac.uk/trac against the component prover-isabelle (TODO).

PGIP support for proof assistants other than Isabelle (i.e. Coq)

Of course, PGIP has been designed by taking the existing Proof General protocol, so in theory it should be easy to get things working. But things have moved on a bit with new prover versions. There are two main issues to make sure we work well with other provers:

1. Compatible document structure
2. Compatible interaction structure. See: CoqHistoryMechanismNotes

PGIP support for new interfaces (i.e. the Nijmegen interface)

• PGIPDisplaysHowTo --- this needs to be improved/completed, of course, maybe during the meeting using the Nijmegen interface as a driving example

Improvements, fixes and extensions needed in PGIP

• Various minor issues
  
  • see PGIPDevelNotes
• Several important extensions to support ProofEngineering
  
  • e.g., dependency reporting both at library and document level

Future improvements, fixes and extensions needed in Provers to support advanced interfaces

• For example, the ugly but one-day-we'll-have-to-confront-it issue of term syntax
  • Can Isabelle (ever) support subterm markup structure?
  • Should we instead aim at a prover-independent syntax mechanism?

Possible future simplifications of PGIP

• Existing ideas are here: PGIPVersionThree
• Other obvious ideals: splitting the schema into pieces (technical probs); better documentation