<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On 2 October 2015 at 13:27, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Ramana and Michael,<br>
<br>
Thank you for updating the Isabelle importer and moving it to a new<br>
home. I'll update the link on the OpenTheory project page<br>
<br>
<a href="http://www.gilith.com/research/opentheory/" rel="noreferrer" target="_blank">http://www.gilith.com/research/opentheory/</a><br>
<br>
to point to the github repo, and should I also change the maintainer<br>
to you both?<br></blockquote><div><br></div><div>I'm fine with that.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Perhaps one day it will be possible to replace the "R" with an "R/W"<br>
too, to match the other interfaces :-)<br></blockquote><div><br></div><div>That is the hope.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Cheers,<br>
<br>
Joe<br>
<span class="im HOEnZb"><br>
On Thu, Oct 1, 2015 at 5:25 PM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote:<br>
</span><div class="HOEnZb"><div class="h5">> Hello,<br>
><br>
> Michael Norrish and I have taken Brian's importer and got it to at least<br>
> build on Isabelle2015. In the process we also converted to a git repository<br>
> and put it on GitHub. You can find it here:<br>
><br>
> <a href="https://github.com/xrchz/isabelle-opentheory" rel="noreferrer" target="_blank">https://github.com/xrchz/isabelle-opentheory</a><br>
><br>
> We haven't been able to get Brian's demo OpenTheory.thy to work yet, and<br>
> it's quite possible we made mistakes in updating opentheory.ML. I hope<br>
> further updates can happen in the above repository, where it's easy for me<br>
> to accept contributions (pull requests), although further coordination on<br>
> the original repository would also be fine as long as it's being actively<br>
> maintained.<br>
><br>
> Cheers,<br>
> Ramana<br>
><br>
> On 31 August 2015 at 15:24, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote:<br>
>><br>
>> Hi Brian,<br>
>><br>
>> Could I trouble you to look for a copy of your OpenTheory-related code for<br>
>> Isabelle? I'd like to see if I can get it working.<br>
>><br>
>> Oh, actually I just found this link:<br>
>> <a href="http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/OpenTheory" rel="noreferrer" target="_blank">http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/OpenTheory</a><br>
>><br>
>> So, I can get started with that, but if you have any comments or ideas<br>
>> they could probably still be helpful :)<br>
>><br>
>> Cheers,<br>
>> Ramana<br>
>><br>
>> On 6 July 2015 at 20:54, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote:<br>
>>><br>
>>> Yes, if it works (or is close to working) I would like to get it<br>
>>> incorporated into the Isabelle codebase. I'm not yet sure how to contribute<br>
>>> things to Isabelle, but I imagine I'll find out within the next few months.<br>
>>><br>
>>> On 23 May 2015 at 15:52, Brian Huffman <<a href="mailto:brianh@cs.pdx.edu">brianh@cs.pdx.edu</a>> wrote:<br>
>>>><br>
>>>> 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>
>>>><br>
>>>> - Brian<br>
>>>><br>
>>>><br>
>>>> On Sat, May 23, 2015 at 5:13 AM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>><br>
>>>> 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">brianh@cs.pdx.edu</a>> wrote:<br>
>>>> >> On Thu, Apr 14, 2011 at 7:03 PM, Joe Hurd <<a href="mailto:joe@gilith.com">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<br>
>>>> >> in<br>
>>>> >> Isabelle.<br>
>>>> >><br>
>>>> >> Of course, exporting proofs from Isabelle is a completely different<br>
>>>> >> 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<br>
>>>> >>> a<br>
>>>> >>> set of OpenTheory packages that don't make any definitions. When I<br>
>>>> >>> was<br>
>>>> >>> designing the standard theory library I tried to isolate packages<br>
>>>> >>> that<br>
>>>> >>> made definitions and have them export just a minimal theorem<br>
>>>> >>> interface<br>
>>>> >>> - most of the theorems are proved in packages that make no<br>
>>>> >>> definitions<br>
>>>> >>> and so can be safely run to populate the [opentheory] set of<br>
>>>> >>> 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<br>
>>>> >>>> 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<br>
>>>> >>>> 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<br>
>>>> >>> 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<br>
>>>> >> 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...<br>
>>>> >>>> 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<br>
>>>> >>>> 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<br>
>>>> >>> is<br>
>>>> >>> that more and more theories will be converted to OpenTheory<br>
>>>> >>> 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<br>
>>>> >> 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">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>
>>><br>
>>><br>
>><br>
><br>
><br>
> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="mailto:opentheory-users@gilith.com">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>
><br>
<br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">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>