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 MHonArc.