PGIP Meeting agenda

Some discussion points:

  • 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

Topic revision: r3 - 09 Mar 2007 - 14:58:12 - CezaryKaliszyk
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies