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