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

[Cezary Kaliszyk]

Hi Florian,

On Sun, Mar 04, 2012 at 10:15:38AM +0100, Florian Haftmann wrote:
> I've been working on the Importer stuff, not very deeply, but separating
> HOL4 and HOL Light contents, stripping generic parts of any name
> reference to HOL4, etc. [...]

Great!

> There could be done a lot more on the ML stuff to introduce basic coding
> practice there, of course, but for the moment I will leave that aside.

As I mentioned to you privately, we (w Alex) are trying to write a new
better import. So before working on the old one too much, lets first
see which parts are reused and which will not.

> Two questions:
> a) There is a README;  maybe you would like to update it according to
> your current expertise?
> b) After the pred/set issue, the generated HOL Light theories must be
> regenerated.  Do you have time to accomplish this?  Alternatively, I
> could follow the README instructions as soon as available.

There are two issues; first:

This is not as straightforward as it seems; apparently some of the
constant maps have types that are not valid anymore (for example
INSERT), so it is not going to work immediately. One can update it
with most of the constant maps removed immediately; but I would
suggest waiting a week or two for the new import and trying to get
the maps correct there.

But more importantly, the concept of generating these files and then
replaying them with 'sorrys' is very strange in an LCF approach.
Having built the session once, one can checkpoint the image and
this is much nicer than the generated sources. The only
thing this needs instead is some way to generate documentation.

Makarius once suggested an antiquotation, that does something like
'print_theorems'. I have not investigated how to implement one?

Cheers,

Cezary