<div dir="ltr"><div><div><div>Joe,<br><br></div>Thank you very much for implementing that. The design you chose looks very nice. I will try it out as soon as I get a chance (it may be a couple of weeks from now, though).<br><br></div>Cheers,<br></div>Ramana<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 16 May 2016 at 14:54, 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,<br>
<br>
I've implemented this functionality, which is available in the latest<br>
released version and the github development snapshot.<br>
<br>
I simply changed the semantics of the --assumptions information to<br>
make it respect the --show-assumptions flag, so<br>
<br>
opentheory info --assumptions<br>
<br>
now only outputs the unsatisfied assumptions in article format, and<br>
the old behaviour is recovered by<br>
<br>
opentheory info --show-assumptions --assumptions<br>
<br>
which outputs all the assumptions of a theory. This mirrors the<br>
behaviour of opentheory info --theory.<br>
<br>
Hopefully this gives you what you need.<br>
<br>
Cheers,<br>
<br>
Joe<br>
<div class="HOEnZb"><div class="h5"><br>
On Mon, May 9, 2016 at 11:58 PM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote:<br>
> Abstractly, my use-case is:<br>
> I have a package A that develops some concepts that are already in a<br>
> standard library package, B.<br>
> A is developed from scratch, but goes much further than B.<br>
> I want to present A as if it were based on B, rather than developed from<br>
> scratch.<br>
> So, I pull out the foundations from A, replace them by B, and then I want to<br>
> see what remaining foundational assumptions need to be proved manually<br>
> (starting from what is provided by B).<br>
><br>
> On 10 May 2016 at 16:08, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:<br>
>><br>
>> I can't think of any way of persuading the existing opentheory tool to<br>
>> give you this functionality, except in the way you describe.<br>
>><br>
>> I'd be happy to add the functionality to the tool, but it may take a<br>
>> little while.<br>
>><br>
>> As a matter of curiosity, what is your use-case for this functionality?<br>
>><br>
>> Cheers,<br>
>><br>
>> Joe<br>
>><br>
>> On Sun, May 8, 2016 at 7:09 PM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>><br>
>> wrote:<br>
>> > Hi,<br>
>> ><br>
>> > How can I get the unsatisfied assumptions of a theory in article format?<br>
>> ><br>
>> > I know about the info --assumptions option, but it prints _all_<br>
>> > assumptions,<br>
>> > including the satisfied ones.<br>
>> ><br>
>> > The only way I have found so far to do it is to create a fake package<br>
>> > that<br>
>> > imports all the required packages and print the assumptions of that. But<br>
>> > it's rather cumbersome to do so. Especially because importing the<br>
>> > required<br>
>> > packages also means figuring out all their dependencies and recreating<br>
>> > them<br>
>> > as blocks within the theory file in the right order.<br>
>> ><br>
>> > I know the opentheory tool knows how to calculate just the unsatisfied<br>
>> > assumptions. How can I get them out of it?<br>
>> ><br>
>> > Cheers,<br>
>> > Ramana<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>
><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>