Re: [isabelle] OpenTheory import for Isabelle



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

On 21/02/2018 17:46, Lars Hupel wrote:
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>


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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