Re: [isabelle] Status of HOL/Import



On Wed, Jul 13, 2011 at 4:09 AM, Makarius <makarius at sketis.net> wrote:
>> 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.

The setup for HOL4 and HOLLight is common, so indeed this
is exactly the setup for HOL4, and indeed it did not change since
that time. I only rediscovered how to make use of it with current
HOLLight Proof-Recorded version and inside current Isabelle.

> If this is not becoming part of one of the automated tests in
> the background, it will not last very long.

On an average computer it takes about 2 hours.

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

Of course, it would be nice to modernize the infrastructure; I just made
it work the way it was. There are a number of obvious things that could
be done with it, like you mention Isabelle settings but also proper use of
local theories (this would avoid the Stale theory errors), split conjunction
theorems and look them up separately, etc. However I am not sure there
is enough interest.

Regards,

Cezary





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