<div dir="ltr"><div>Hi Ramana,</div><div><br></div><div>I'm still not convinced that the proof format in Cezary & Alex's paper is more concise than OpenTheory, here is where the discussion ended last time:</div>
<div><br></div>On Wed, Jul 31, 2013 at 2:49 PM, Alexander Krauss <span dir="ltr"><<a href="mailto:krauss@in.tum.de" target="_blank">krauss@in.tum.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div class="">On 07/26/2013 11:29 PM, Joe Leslie-Hurd wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
Given these minor differences, I'm intrigued by the statement in the conclusion:<br><br>"In our development we defined a new format for proof exchange traces, despite<br>the existence of other exchange formats. We have tried writing the<br>
proof trace in the<br>OpenTheory format, and it was roughly 10 times bigger."<br><br>Cezary, Alex: Would it be possible to share this proof trace in the<br>two formats, so I can see what difference is responsible for the<br>
blow-up?</blockquote><br></div>I must pass this question on to Cezary, who made this specific experiment. I'm not even sure whether this is before or after compression... But just looking at the list of OpenTheory commands, it seems to me that building up substitutions as nested lists on the stack is rather complicated.</blockquote>
<div><br></div><div>So the 10x size increase may simply have been an artifact of comparing against an uncompressed OpenTheory proof file. If Cezary could dig up the proof files that were used for this comparison, I'd be very happy to take a look and see whether there's something deeper that is going on.<br>
<br></div><div>Unfortunately I think that proof formats (like both of these) that explicitly record every low-level inference are doomed to be bogged down by massive proofs. I've thought about some ways to scale better, such as adding a new "rewrite" OpenTheory command that behaves like REWRITE_CONV, but such rules are hard to specify precisely to guarantee identical behaviour on different platforms.</div>
<div><br></div><div>I'd be interested in hearing your ideas about how to scale better in proof formats while preserving portability.</div><div><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div><br></div></div>
<div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Feb 18, 2014 at 9:12 AM, 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">Hi Joe, Cezary, Alex,<br>
<br>
I am planning, in the next few months, to export an extremely large<br>
proof from HOL4 into a format where I can check it with a standalone<br>
checker. (This proof takes hours to construct in HOL4.) OpenTheory<br>
seems the obvious choice as a proof storage medium, but the current<br>
format and implementations struggle with even moderate-sized proofs.<br>
I'd be very interested to hear about progress towards using the ideas<br>
from Cezary and Alex's paper to improving the scalability of<br>
OpenTheory technology. Have you made any progress on this front? Would<br>
you be interested in working on it with me?<br>
<br>
I hope we will be able to coordinate on this, since I think it's<br>
important work and each of us has something crucial to offer towards<br>
it.<br>
<br>
As a first item, I would think that the OpenTheory article format<br>
needs to be updated, as we were discussing earlier. Joe, Alex, did you<br>
come to any conclusions about whether changes are necessary and what<br>
they would look like?<br>
<br>
Cheers,<br>
Ramana<br>
<div class="HOEnZb"><div class="h5"><br>
On Tue, Aug 6, 2013 at 1:02 AM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote:<br>
> On Mon, Aug 5, 2013 at 11:49 PM, Alexander Krauss <<a href="mailto:krauss@in.tum.de">krauss@in.tum.de</a>> wrote:<br>
>><br>
>><br>
>>> The opentheory tool post-processes articles extracted from theorem<br>
>>> provers, for compression and neatness purposes. To that end it does<br>
>>> both of the things you call out.<br>
>><br>
>><br>
>> Which command do I have to run to get this?<br>
><br>
><br>
> Install opentheory as per<br>
> <a href="http://www.gilith.com/software/opentheory/install.html" target="_blank">http://www.gilith.com/software/opentheory/install.html</a>.<br>
> Then run it like:<br>
>   opentheory info --article --output processed.art input.art<br>
</div></div></blockquote></div><br></div>