Re: [isabelle] Status of HOL/Import



On Wed, 13 Jul 2011, Cezary Kaliszyk wrote:

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

I did not expect this to happen so quickly.


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).

It reminds me again of the setup from 2004/2005 for HOL4. If this is not becoming part of one of the automated tests in the background, it will not last very long.


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

do "export HOL4_PROOFS=~/tmp"

before running "isabelle make HOL-Generate-HOLLight"

Better use Isabelle settings for such things -- as was done in 2004 already.


	Makarius





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