[opentheory-users] Print unsatisfied assumptions

[Ramana Kumar]

Joe,

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).

Cheers,
Ramana

On 16 May 2016 at 14:54, Joe Leslie-Hurd <joe at gilith.com> wrote:

> 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
>
> On Mon, May 9, 2016 at 11:58 PM, Ramana Kumar <ramana at member.fsf.org>
> 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 <joe at gilith.com> 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 <ramana at member.fsf.org>
> >> 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
> >> > opentheory-users at gilith.com
> >> > http://www.gilith.com/opentheory/mailing-list
> >> >
> >>
> >> _______________________________________________
> >> opentheory-users mailing list
> >> opentheory-users at gilith.com
> >> http://www.gilith.com/opentheory/mailing-list
> >
> >
> >
> > _______________________________________________
> > opentheory-users mailing list
> > opentheory-users at gilith.com
> > http://www.gilith.com/opentheory/mailing-list
> >
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20160524/dce98af5/attachment.html>