On Wed, 20 Jul 2011, Florian Haftmann wrote:
On Wed, Jul 20, 2011 at 11:33 AM, Alexander Krauss <kra...@in.tum.de>
wrote:
Now my question is: What do we actually know when
HOL-Generate-HOLLight completes without error? Should the generated
file be compared with the version in the repository and should the
test fail when they are not identical? Are there other things that
should be checked?
I view the matter similar to our documents in doc-src: both source and
generated files are included in the repository. For the documents,
there is the building of the PDFs from the generated tex sources, and
the generation of the tex sources from the theories (for bootstrap
reasons in that order).
This is due to many historical oddities. We have to live with it some
more time, but should not give up moving towards plain formal document
sessions uniformly, without any special tricks (such as the now obsolete
"rail" executable as part of the process).
For the importer, there is the loading of the generated files, and, only
if HOL4/Light is available, the re-generation of the files. The first
can happen in a regular makeall, the second in a dedicated test. The
only thing to keep in mind is that before releasing the generated files
should be updated manually for consistency: inconsistency can always
eliminated as long as the two build steps work!
In all these years I've never understood the purpose of the generation
process -- generated sources are a bit like self-modifying code.
Does it mean that the generation process is where the actual proofs are
imported (still quite slowly for due accidental technical reasons), and
the regular sessions are based on oracles only? Which purpose do the
generated theory files have in the first place? The smart_string_of
functions are a bit odd, reparsing not really cheap, and the result is an
artificial sequentialization of the import graph. E.g. there could be a
single command to load all desired theorems (with explicit proofs inside),
and potentially another command to pretty print some of the content in
human-readable form.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev