Email Gateway (Aug 18 2022 at 18:07): Email Gateway (Aug 18 2022 at 18:07):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Dear all,
After some struggling I succeeded running HOL/Import for HOLLight.
(I wanted to port some of my older HOL-Light developments)
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.
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?
Cezary
Email Gateway (Aug 18 2022 at 18:07):From: Tobias Nipkow <nipkow@in.tum.de>
Alas, nobody has been using this for some time and it has fallen into
disrepair. If you can get it to work again, you are very welcome!
Tobias
Email Gateway (Aug 18 2022 at 18:07):From: Alexander Krauss <krauss@in.tum.de>
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
Email Gateway (Aug 18 2022 at 18:07):From: Steven Obua <steven.obua@googlemail.com>
On 12.07.2011, at 09:56, Cezary Kaliszyk wrote:
Dear all,
After some struggling I succeeded running HOL/Import for HOLLight.
(I wanted to port some of my older HOL-Light developments)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.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?
It would be great if you manage to update this stuff. Let me know in case you get stuck somewhere.
Cezary
Email Gateway (Aug 18 2022 at 18:07):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
On Tue, Jul 12, 2011 at 5:05 PM, Tobias Nipkow <nipkow@in.tum.de> wrote:
Alas, nobody has been using this for some time and it has fallen into
disrepair. If you can get it to work again, you are very welcome!
I pushed the changes to the repository. Apart from small modifications
to existing compat theorems that made it work with current HOL Light
and adapting to current Isabelle the changes are:
I added about 100 new constant maps along with compat theorems which
means many theorems can be translated to ones talking about Isabelle
constants, in particular theorems about lists, sets (union, ...) and
number theory (gcd, ...) are translated now.
I also tried to add maps for reals and integers; this works only
partially so I do not enable it by default in the build. Enabling
those allows translating theorems that talk about reals and integers
to Isabelle reals and integers but it fails for more complicated types
that are based on reals, mostly because I have not been able to map
'mk_real'. Without these maps all theorems are translated correctly to
copies or reals and integers.
I also needed to update 'smart_string_of_thm' as it was failing for
all theorems and I was getting the fully bracketed output.
Cezary
Am 12/07/2011 09:56, schrieb Cezary Kaliszyk:
Dear all,
After some struggling I succeeded running HOL/Import for HOLLight.
(I wanted to port some of my older HOL-Light developments)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.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?Cezary
Email Gateway (Aug 18 2022 at 18:07):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
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
Email Gateway (Aug 18 2022 at 18:08):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 18:08):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
On Wed, Jul 13, 2011 at 4:09 AM, Makarius <makarius@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
Last updated: Apr 26 2024 at 12:28 UTC