TWiki
>
PG Web
>
PGIP
>
PGIPMunichMeetingFeb07
>
PGIPMeetingAgenda
(revision 1)
Edit
Attach
PGIP
Meeting agenda
Some discussion points:
Simplification of
PGIP
protocol: see
PGIPVersionThree
Unicode everywhere:
MakariusW
says it will be 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?
Makarius: shall we get rid of redo?
What about nested proofs and history management?
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
Batch mode 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
Xavier Leroy: one of the best things he did was to implement separate compilation in OCaml
--
DavidAspinall
- 08 Mar 2007
Edit
|
Attach
|
P
rint version
|
H
istory
:
r3
<
r2
<
r1
|
B
acklinks
|
R
aw View
|
Raw edit
|
More topic actions...
Topic revision: r1 - 08 Mar 2007 - 11:34:48 -
DavidAspinall
PG
PG Web
PG Web Home
Changes
Index
Search
Notifications
RSS Feed
Copyright © 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