[isabelle-dev] [isabelle] Status of HOL/Import

[Cezary Kaliszyk]

Hi Florian,

On Wed, Jul 13, 2011 at 6:15 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> Of course there is a lot one could clean up.  In my eyes there are some
> issues which prevent an understanding of HOL-Import »in the large«, and
> maybe your experience could answer the following questions:
>
> a) HOL-Import seems to import both HOL4 and HOL Light, but the ROOT.ML
> file
> http://isabelle.in.tum.de/reports/Isabelle/file/e84239a47f32/src/HOL/Import/ROOT.ML
> only mentions HOL4Compat and HOL4Syntax as imported theories.  Where
> does HOL Light come in?

The setup is indeed confusing and it would be great to change it.

Currently IsaMakefile allows for two targets:
  HOL-Generate-HOL and HOL-Generate-HOLLight
(They cannot be called together, so the 'generate' target in the
makefile does not make sense).

Generate-HOL refers to the ROOT.ML you mentioned.
HOLLight refers to a ROOT.ML in a subdirectory:
  http://isabelle.in.tum.de/reports/Isabelle/file/e84239a47f32/src/HOL/Import/Generate-HOLLight/ROOT.ML

Which refers to the HOLLight generation script which uses some of the
files from the main Import directory.

> b) There seems to be no README or generated document which explains at
> least rudimentary how to actually use the importer.  Is there any
> reference for that?

There is a README in HOL-Light source code that explains how to get
the recorded proofs:

http://hol-light.googlecode.com/svn/trunk/Proofrecording/README

With the files generated this way, it is enough to set the HOL4PROOFS
environment variable and one can import the generated file or run
'isabelle make HOL-Generate-HOLLight' to regenerate it.

This is all I have used.

> There is also space for structural improvements;  one is mentioned in
> the at least parly outdated
> http://isabelle.in.tum.de/reports/Isabelle/file/e84239a47f32/src/HOL/Import/HOL/README
>  it is confusing that files *from* which files are generated are placed
> in a directory named »Generate…« and not the other way round.
> One could also ask whether generated files must be part of the versioning anyway.

Renaming the files and splitting them into the directories: HOL4,
HOLLight, Common and Generated would be a great idea.

I would however keep the generated "thy" files in the distribution. It
is a collection of 1300 lemmas. without proofs (so they do not take up
too much space), that do not exist in Isabelle in this form elsewhere
and (as the README says) could be used without getting HOLLight
running, exporting the proofs etc.

Cheers,

Cezary