Re: [isabelle] Proofmanagement
On Wed, 29 Aug 2012, Jan Keller wrote:
How do you do the management of proofs in Isabelle? Are there any tools?
Are there technics to react on changes of potential dependencies of
proof? Could you detect wether a proof is still valid or deprecated?
This is mainly part of the implicit "document model" of the prover, which
is then connected to jEdit via conventional text editing operations
(insert/remove intervals of text). The document model is declarative in
the sense that it reacts on changes in a (hopefully) sensible way. The
hard work of managing dependencies is in the core implementation, both
src/Pure/PIDE/document.ML and document.scala.
The main result of document processing is a markup tree that is associated
with the original source text. By querying that information (via a
document "snapshot") one can get some dependency-like information, say
where formal entities are defined and references. This is how hyperlinks
work in Isabelle/jEdit.
Are there tools for the dependencies of proofs? How are the dependencies
visualized? I saw something like a dependency graph in JEdit. Is that
correct? Have you tools to refractor proofs or requirements?
Most of that is still missing. I am already glad to have most of the
ascyncronous editing model running after several years of working on the
concepts and implementation.
What is coming in the next release is some offline dependency management
as part of Isabelle/Scala, to figure out which source files contribute to
an Isabelle "session" (say HOL or an application of it), and to figure out
changes here wrt. a persistent state in the file-system.
This archive was generated by a fusion of
Pipermail (Mailman edition) and