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
This topic: PG
> PGIP >
PGIPMunichMeetingFeb07 > PGIPMeetingAgenda
Topic revision: r3 - 09 Mar 2007 - 14:58:12 -
CezaryKaliszyk