[isabelle-dev] Testing HOL/Import

[Cezary Kaliszyk]

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?

Completing without error is already quite good; I am not sure about
the file comparison:

At the moment there are two generated files, the 'thy' file and the 'imp' file.
The 'thy' file has all the theorems that are present in HOL Light but
not in Isabelle.
The 'imp' file includes theorem mappings. If new things are proved in
Isabelle that
are identical to the ones that were in HOL-Light, theorems with
disappear from the
'thy' file and the mapping in the 'imp' file will refer to the new
theorems. This does
not sound like a reason for failing?

Cezary