[isabelle-dev] Testing HOL/Import

[Makarius]

On Wed, 20 Jul 2011, Florian Haftmann wrote:

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

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