Re: [isabelle] Status of HOL/Import



Hi Cezary,

After some struggling I succeeded running HOL/Import for HOLLight.
(I wanted to port some of my older HOL-Light developments)

Nice. I had already accepted the thought that we must abandon this as soon as anybody notices how broken it is.

The files present in the current repository version of Isabelle
seem not to have been updated for quite a while (they still use
the syntax "theory = ... + ..." which doesn't work for a while).
Also the generation script refers to HOLLight constants not present
at least since early 2005.

This is because the regression test only covers a tiny part of the whole procedure. Hence, the usual bit rot applies.

Is anyone using HOL/Import or the theorems translated from HOLLight
or can I update the generation and compatibility scripts to work
with current Isabelle and svn HOLLight, add some constant maps
and update the generated theorems?

If you manage to revive the whole thing go ahead. But we should extend the regression test as soon as it works again.

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.