Re: [isabelle] OpenTheory import for Isabelle



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 at lists.cam.ac.uk>
wrote:
>
> Date: Wed, 21 Feb 2018 17:46:17 +0100
> From: Lars Hupel <hupel at in.tum.de>
> Subject: [isabelle] OpenTheory import for Isabelle
> To: isabelle-users at cl.cam.ac.uk
> Cc: Ramana Kumar <ramana.kumar at gmail.com>
> Message-ID: <f4dffe9e-4c4a-3e38-c5e5-ea040be0d99c at in.tum.de>
> Content-Type: text/plain; charset=utf-8
>
> 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
>
>



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