Email Gateway (Aug 22 2022 at 16:37): Email Gateway (Aug 22 2022 at 16:37):From: Tobias Nipkow <nipkow@in.tum.de>
If it is just for testing, how about a much smaller test case?
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 16:37):From: Lars Hupel <hupel@in.tum.de>
If it is just for testing, how about a much smaller test case?
I have now measured what I assume is "the bare minimum". That's about
3.7 MB uncompressed, and less than 750 KB compressed. That should be
manageable. It includes some basic proofs on bools, naturals, lists and
relations.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:37):From: Brandon Bohrer <bbohrer@cs.cmu.edu>
Being able to use the CakeML definitions in Isabelle via OpenTheory would
be very useful to us at CMU as well, allowing us to do all our work in
Isabelle instead of pulling in HOL4 as well with all the obvious
implications on trusted computed base size.
I have no opinion whether it should go in AFP vs. somewhere else.
My impression from talking to Chalmers folks though is that what is really
needed is someone who is willing to put in the maintenance effort and avoid
bitrot like Lars says. The CakeML definitions are, unsurprisingly, complex
enough that tools which haven't been maintained in years won't cut it.
On Thu, Feb 22, 2018 at 4:14 AM, <cl-isabelle-users-request@lists.cam.ac.uk>
wrote:
Date: Wed, 21 Feb 2018 17:46:17 +0100
From: Lars Hupel <hupel@in.tum.de>
Subject: [isabelle] OpenTheory import for Isabelle
To: isabelle-users@cl.cam.ac.uk
Cc: Ramana Kumar <ramana.kumar@gmail.com>
Message-ID: <f4dffe9e-4c4a-3e38-c5e5-ea040be0d99c@in.tum.de>
Content-Type: text/plain; charset=utf-8Dear list,
some people here might have heard of this project:
<https://github.com/xrchz/isabelle-opentheory>
Originally implemented by Brian Huffman for Isabelle2011 [5] it sat
around for a long time, until it's been picked up by Ramana Kumar again,
who thankfully ported it to Isabelle2016.The current state is that it works for Isabelle2017 and can also import
a lot of existing library theories form the OpenTheory repository [0].Today I've updated that repository to add a ROOT file and a script to
download the necessary .art file. [1]I'm posting this here because that importer appears to be quite
bitrot-prone. It is in a state where it is "working", but many things
are unidiomatic, e.g. pervasive use of global theories and lack of
parallelism. It would be a pity if it would stop working after 1–2 more
Isabelle releases with nobody around to fix it.I wanted to ask around what people would feel about having this importer
in the AFP (I don't think it's ready for the distribution).Some points for consideration:
- The CakeML folks at Chalmers and apparently at Data61 are interested
in using it to work with the "real" (i.e. the one in HOL4) CakeML
specification in Isabelle.
- Submitting CakeML to the AFP will require this (likely, eventually) [4].
- The importer reads ".art" files as produced by a separate "opentheory"
executable. This is related to the other thread [2] I posted here today,
because something needs to produce these files.
- ".art" files are relatively large. Mercurial can cope but doesn't like
it very much [3]. The entirety of the required files for the test cases
in the repository can be compressed by Mercurial (i.e. gzip) to ~80 MB.
That's hefty. Maybe it should be an Isabelle component instead?There's no particular rush for any of this. In fact, the code should
probably be cleaned up a bit before it goes anywhere "official".Cheers
Lars[0] <http://opentheory.gilith.com/>
[1] Instructions: <https://github.com/xrchz/isabelle-opentheory/pull/1>
[2]
<
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-February/msg00089.html[3] You'll get messages like:
hol-words-1.2.art: up to 266 MB of RAM may be required to manage this file
(use 'hg revert hol-words-1.2.art' to cancel the pending addition)[4] In the short term, this is better solved by submitting the
Lem-generated .thy files.[5]
<
http://telperion.gilith.com/pipermail/opentheory-users/2011-April/000099.html
Email Gateway (Aug 22 2022 at 16:37):From: Gerwin.Klein@data61.csiro.au
I agree with Tobias in that don’t think the importer is a good match for the AFP.
How about putting the importer and/or a minimal set of .art files into the distribution? Downloading might work for the distribution, in the sense that this minimal set of .art files could be a component.
Making sure that the larger collection of .art files works could be handled separately. It sounds like there is a bunch of interested parties (we are one of them), and we (Data61) can possibly provide a regression test infrastructure (need to check). If there are a few groups who are willing to maintain the collection and keep it up to date, that approach might work.
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 16:37):From: Lars Hupel <hupel@in.tum.de>
How about putting the importer and/or a minimal set of .art files into the distribution? Downloading might work for the distribution, in the sense that this minimal set of .art files could be a component.
Right. Today I've been doing some digging into the implementation and I
think it should be possible to clean it up with modest effort to make it
ready for inclusion.
Making sure that the larger collection of .art files works could be handled separately. It sounds like there is a bunch of interested parties (we are one of them), and we (Data61) can possibly provide a regression test infrastructure (need to check). If there are a few groups who are willing to maintain the collection and keep it up to date, that approach might work.
Sure, that would work, I guess. But keep in mind that the distinction
between what should be tested and what shouldn't is pretty much
arbitrary. My starting point was the repository by Brian et.al. For
example, Maksym Bortin has put some .art files about ARM machine code in
there. (Is there a good reason why we don't try to import the entirety
of the OpenTheory database? In some sense, that database serves a
similar purpose as the AFP. There are 54 packages as of this writing.)
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:37):From: Lars Hupel <hupel@in.tum.de>
Nice to hear that you're also interested in this! Keep in mind though
that there are currently some technical issues preventing CakeML to be
exported to OpenTheory (<https://github.com/CakeML/cakeml/issues/321>).
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:38):From: Makarius <makarius@sketis.net>
In the Isabelle distribution the quality standards are even higher than
for AFP.
I would welcome a proper version of the OpenTheory importer for
Isabelle, but it needs to be done properly, as usual.
Makarius
Email Gateway (Aug 22 2022 at 16:51):From: Lars Hupel <hupel@in.tum.de>
Dear list,
some people here might have heard of this project:
<https://github.com/xrchz/isabelle-opentheory>
Originally implemented by Brian Huffman for Isabelle2011 [5] it sat
around for a long time, until it's been picked up by Ramana Kumar again,
who thankfully ported it to Isabelle2016.
The current state is that it works for Isabelle2017 and can also import
a lot of existing library theories form the OpenTheory repository [0].
Today I've updated that repository to add a ROOT file and a script to
download the necessary .art file. [1]
I'm posting this here because that importer appears to be quite
bitrot-prone. It is in a state where it is "working", but many things
are unidiomatic, e.g. pervasive use of global theories and lack of
parallelism. It would be a pity if it would stop working after 1–2 more
Isabelle releases with nobody around to fix it.
I wanted to ask around what people would feel about having this importer
in the AFP (I don't think it's ready for the distribution).
Some points for consideration:
The CakeML folks at Chalmers and apparently at Data61 are interested
in using it to work with the "real" (i.e. the one in HOL4) CakeML
specification in Isabelle.
Submitting CakeML to the AFP will require this (likely, eventually) [4].
The importer reads ".art" files as produced by a separate "opentheory"
executable. This is related to the other thread [2] I posted here today,
because something needs to produce these files.
".art" files are relatively large. Mercurial can cope but doesn't like
it very much [3]. The entirety of the required files for the test cases
in the repository can be compressed by Mercurial (i.e. gzip) to ~80 MB.
That's hefty. Maybe it should be an Isabelle component instead?
There's no particular rush for any of this. In fact, the code should
probably be cleaned up a bit before it goes anywhere "official".
Cheers
Lars
[0] <http://opentheory.gilith.com/>
[1] Instructions: <https://github.com/xrchz/isabelle-opentheory/pull/1>
[2]
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-February/msg00089.html>
[3] You'll get messages like:
hol-words-1.2.art: up to 266 MB of RAM may be required to manage this file
(use 'hg revert hol-words-1.2.art' to cancel the pending addition)
[4] In the short term, this is better solved by submitting the
Lem-generated .thy files.
[5]
<http://telperion.gilith.com/pipermail/opentheory-users/2011-April/000099.html>
Email Gateway (Aug 22 2022 at 16:51):From: Tobias Nipkow <nipkow@in.tum.de>
I do not like the idea of putting something in the AFP because it is not ready
for the distribution. And 80 MB of compressed, generated files is unappealing as
well and likely to create trouble. I am guessing that .art files are opentheory
files. If that is the case, can't they reside in the opentheory repository?
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 16:51):From: Lars Hupel <hupel@in.tum.de>
Yes, they are OpenTheory files. The "isabelle-opentheory" session reads
them in (as test cases, essentially) during regular "isabelle build" or
when opening them in Isabelle/jEdit. So they need to be somewhere
Isabelle can find them. I'm assuming that downloading them on-the-fly is
not an option. In principle the OpenTheory import for Isabelle can be
built without reading any .art files, but then there's nothing testing
that it actually works.
Cheers
Lars
Last updated: Nov 21 2024 at 12:39 UTC