Re: [isabelle] Status of HOL/Import



On Tue, Jul 12, 2011 at 5:15 PM, Alexander Krauss <krauss at in.tum.de> wrote:
>> 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.

It does work now.
To build it one needs the proof objects from HOL-Light.

I packed the ones generated from the current version at:
  http://prover.cs.ru.nl/~cek/22SHOLLIGHT.tbz

(Archive is 13Mb, but it takes nearly 1Gb after extracting).

If you extract it so the files are in:
  ~/tmp/hollight/hollight/

do "export HOL4_PROOFS=~/tmp"

before running "isabelle make HOL-Generate-HOLLight"

Cezary





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