[isabelle-dev] New HOL/Import

[Cezary Kaliszyk]

On Thu, Mar 29, 2012 at 8:04 PM, Makarius <makarius at sketis.net> wrote:
> Wow, I am impressed by the brevity of it.  You should mention the secret
> http://cl-informatik.uibk.ac.at/~cek/proofs which is a bzip stream to be
> uncompressed, before it can be used with import_file in the example.

That's the preprocessed proof image for importing basic hol-light.

> You are no longer using any XML/YXML now.  Is the format somehow related to
> OpenTheory by Joe Hurd?

No; the information stored is similar to the old format, but more brief and
easier to parse: every line contains a next typ/term/thm to read, with
arguments space separated and last uses of an object marked with a minus.

It could be converted (possibly automatically) to OpenTheory; however the
sharing is done at a different level so it would be hard to recover additional
sharing and without it, Opentheory would be at least an order of
magnitude bigger.

>> - Does anyone have opinions about the HOL4 code that has been long dead?
> Which HOL4 code do you mean exactly?

The code currently in isabelle repository is in 3 places:
  Import, Import/HOL_Light and Import/HOL4

The Import/HOL_Light is functional but the proposed code replaces it.
The Import/HOL4 has not been functional for a while, (I have not been able
to use it even with proofs from 2004); should it still stay in the repository?

Regards,
Cezary