[opentheory-users] Print unsatisfied assumptions

[Joe Leslie-Hurd]

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
>