[isabelle-dev] Testing HOL/Import

[Florian Haftmann]

> On Wed, Jul 20, 2011 at 11:33 AM, Alexander Krauss <krauss at 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).  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!

I was thinking about a consistency check for documents some years ago
(motto: »fail if generated files differ«), but did not pursue this
further since sooner or later documents in doc-src should behave like
regular theory sessions.  Don't know whether the situation with import
is different enough to think about that again.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110720/a696a585/attachment.sig>