PGIP Meeting agenda

Some discussion points:

• Simplification of PGIP protocol: see PGIPVersionThree

• Unicode everywhere: MakariusW says: let's see again in another 10 years!
  • how much support from other OS parts is required? (e.g. CVS, grep...)
  • Cezary: works fine in a web browser
  • Mixed support: some people use UTF-8, some raw ASCII.
  • Have a unicode print mode for Isabelle? Or maybe a filter?
  • Julien: would MathML be supported in Eclipse? (yes; modulo font support & symbol mapping required)
  • Stylesheets for PGML: prover or interface? Standard ones?

• Unifying input and output: round-trip problem:
  • how is handled in Mizar?
  • Matita uses disambiguation mechanism which asks user
  • Coq: supposed to support output as input
  • Makarius: should work for Isabelle 99% (for provided libraries; all bets off in general because computationally complete)

• Discussion about translation functions, stacking up layers and getting further from the core

• Providing structure on syntax output
  • Data flow of structure in Isabelle is lost during printing: default should be to preserve it
  • Term structure markup for providing position information
  • --- Makarius: still hard to get markup for positions, but can get atom information for location

• Trimming down PGIP / Isabelle?
  • We need redo when the user want's to go back to inspect the situation Normally we can postpone the undo/redo untill the user commits to the position.
  • What about nested proofs and history management? It would be nice to support flat history.
  • What

• Multi-threaded support
  • David Matthews is working on multi-threaded support for PolyML
  • Can we have multi-threaded proof?
  • Exciting but needs more thought how to do this
    • Exploring branches of proof in parallel
    • Re-checking of parallel branches and ``back-patching``
    • Multi-threaded loading of theories: the most basic multi-threading(!)
    • Should degenerate into single threaded (uses higher-order combinators)
  • BUT: for interface, PGIP already supports possibility for asynchronous output
  • Should be possible for inspection of state

• Coq vs Isabelle differences and object files:
  • LCF style doesn't store difference, so for safety offline storage of what can you use?
  • MakariusW : very few things have a syntactic representation in Isabelle, proofs are not important
  • Me: use certification as Coq does anyway
  • In PolyML 5 can produce object files
  • Separate compilation automatically benefits multi-core by processing several files at once (make -j 2)

• Parsing proof scripts --- challenges!
  • What is the point?
  • Answer: used for indentation, folding/outlining, also semantic information for undo
  • It marks up document as spans, so tells end points for sending commands
  • Can attach additional meta information either during the parse or during execution
  • Manage state of metainformation alongside state of elements
    • Need to outdate meta info appropriately as well, of course
  • Xavier Leroy: one of the best things he did was to implement separate compilation in OCaml

• Message model --- needs discussion
  • Potentially unlimited amount of output for a single command

• Notes about skipping proofs:
  • Pierre Courbineu's declarative mode for Coq allows to pass over incomplete places in proofs and issues a warining that gets shown in yellow by the interface
  • We could implement this in the broker by skipping or backing out in case of errors

-- DavidAspinall - 08 Mar 2007