<div dir="ltr"><div><div><div><div>Hello,<br><br></div>Michael Norrish and I have taken Brian's importer and got it to at least build on Isabelle2015. In the process we also converted to a git repository and put it on GitHub. You can find it here:<br><br><a href="https://github.com/xrchz/isabelle-opentheory">https://github.com/xrchz/isabelle-opentheory</a><br><br></div>We haven't been able to get Brian's demo OpenTheory.thy to work yet, and it's quite possible we made mistakes in updating opentheory.ML. I hope further updates can happen in the above repository, where it's easy for me to accept contributions (pull requests), although further coordination on the original repository would also be fine as long as it's being actively maintained.<br><br></div>Cheers,<br></div>Ramana<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 31 August 2015 at 15:24, Ramana Kumar <span dir="ltr"><<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>Hi Brian,<br><br></div>Could I trouble you to look for a copy of your OpenTheory-related code for Isabelle? I'd like to see if I can get it working.<br><br></div><div>Oh, actually I just found this link: <a href="http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/OpenTheory" target="_blank">http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/OpenTheory</a><br><br></div><div>So, I can get started with that, but if you have any comments or ideas they could probably still be helpful :)<br></div><div><br></div>Cheers,<br></div>Ramana<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 6 July 2015 at 20:54, Ramana Kumar <span dir="ltr"><<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Yes, if it works (or is close to working) I would like to get it incorporated into the Isabelle codebase. I'm not yet sure how to contribute things to Isabelle, but I imagine I'll find out within the next few months.<br></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On 23 May 2015 at 15:52, Brian Huffman <span dir="ltr"><<a href="mailto:brianh@cs.pdx.edu" target="_blank">brianh@cs.pdx.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I've hardly looked at it since I wrote it. It was never incorporated<br>
into the Isabelle codebase. I suppose it would probably work with the<br>
latest Isabelle, because it uses only the low-level proof kernel api,<br>
which doesn't change much any more.<br>
<br>
I'll have to look around to see where I have a copy of the source<br>
code; that was a couple of computers ago. Did you want to try to do<br>
something with it?<br>
<span><font color="#888888"><br>
- Brian<br>
</font></span><div><div><br>
<br>
On Sat, May 23, 2015 at 5:13 AM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>> wrote:<br>
> Hi Brian,<br>
><br>
> What's the status of your OpenTheory importer? Does it work with the<br>
> latest Isabelle? Was it incorporated into the main code base?<br>
><br>
> Cheers,<br>
> Ramana<br>
><br>
> On 15 April 2011 at 17:34, Brian Huffman <<a href="mailto:brianh@cs.pdx.edu" target="_blank">brianh@cs.pdx.edu</a>> wrote:<br>
>> On Thu, Apr 14, 2011 at 7:03 PM, Joe Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote:<br>
>>> Hi Brian,<br>
>>><br>
>>> That is really great work! Am I right in thinking you can import the<br>
>>> parser-1.5 article binding all the input symbols and axioms to<br>
>>> existing ones in Isabelle? I would have guessed that Isabelle type<br>
>>> classes would have managed to get in the way at some point, but<br>
>>> perhaps this would only be for converting Isabelle proofs to<br>
>>> OpenTheory format?<br>
>><br>
>> Yes, each of the input constants of the article is mapped to a<br>
>> pre-existing Isabelle constant. Some of these existing Isabelle<br>
>> constants happen to be overloaded, but that doesn't cause any<br>
>> problems. This mapping of constant names does not even need to be<br>
>> one-to-one; for example, I imagine that "Number.Natural.+" and<br>
>> "Number.Integer.+" would map to the same overloaded "plus" constant in<br>
>> Isabelle.<br>
>><br>
>> Of course, exporting proofs from Isabelle is a completely different story.<br>
>><br>
>>> You mentioned that you prove a lot of theorems that the OpenTheory<br>
>>> article relies on, but it seems you could reduce this by processing a<br>
>>> set of OpenTheory packages that don't make any definitions. When I was<br>
>>> designing the standard theory library I tried to isolate packages that<br>
>>> made definitions and have them export just a minimal theorem interface<br>
>>> - most of the theorems are proved in packages that make no definitions<br>
>>> and so can be safely run to populate the [opentheory] set of theorems.<br>
>><br>
>> Your idea of keeping definitions in separate, minimal modules is a<br>
>> good design. I'm sure I could have greatly reduced the number of<br>
>> [opentheory] lemmas that I needed by finding the right additional<br>
>> article files to import; I was just too lazy to figure out how the<br>
>> packages were organized.<br>
>><br>
>>>> The importer should also extend these tables whenever it defines a new<br>
>>>> constant or type, but I haven't implemented this yet. Another nice<br>
>>>> feature would be a way for users to influence how the importer chooses<br>
>>>> names for newly-defined constants and types. Right now it takes the<br>
>>>> names directly from the strings in the article file, which isn't so<br>
>>>> nice for names like "HOLLight._dest_rec" (Isabelle's parser can't<br>
>>>> handle names that start with underscores).<br>
>>><br>
>>> You should find that constants and type operators with names like this<br>
>>> are never exported from a theory (i.e., never appear in exported<br>
>>> theorems), so it's perfectly safe to normalize their names to<br>
>>> something more acceptable to Isabelle. They are `local definitions'<br>
>>> that are used only in proofs.<br>
>><br>
>> Actually, it seems like it would be safe to rename *any* constant<br>
>> (whether exported or not) to any name that I want in Isabelle, as long<br>
>> as the importer keeps track of the name mapping so that later imports<br>
>> can use the same names.<br>
>><br>
>> I suppose I should write an "import_name" function that converts from<br>
>> OpenTheory names to Isabelle-friendly ones. It would be nice to<br>
>> parameterize this by a list of user-specified exceptions to the<br>
>> mapping, so you could say something like, "import this article, but<br>
>> when you define constant 'foo', call it 'bar' instead."<br>
>><br>
>>>> Once I clean up the code, I'm not sure what I should do with it... I<br>
>>>> suppose I could add it to the Isabelle repo, but I'm not sure if I<br>
>>>> want to advertise to Munich crowd that I've been doing all this work<br>
>>>> that is unrelated to finishing my thesis :)<br>
>>><br>
>>> I would very much like to see it live on in some fashion - my hope is<br>
>>> that more and more theories will be converted to OpenTheory packages,<br>
>>> and your code could be used to import them into Isabelle in a<br>
>>> principled way.<br>
>><br>
>> I suppose I'll add it to the Isabelle distribution at some point,<br>
>> maybe after I finish writing my thesis. In the meantime, I guess I can<br>
>> post the code to the list, so it will be archived and people can try<br>
>> it out.<br>
>><br>
>> - Brian<br>
>><br>
>> _______________________________________________<br>
>> opentheory-users mailing list<br>
>> <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
>> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>