Stream: Hierarchy Builder devs & users

Topic: ✔ More Tool Support


view this post on Zulip Laurent Théry (Oct 31 2023 at 13:53):

I've just been porting my code to mathcomp 2.1.

Here are some of the problems I've encountered and maybe some more tooling would have helped.
Often I want to find inspiration from examples of how the structures has been built by other people.
Let's suppose it is Equality, from what I know I need at least 3 steps

HB.about Equality.
HB.about hasDecEq.
HB.about hasDecEq.eq_op.

so now I get the precious information

HB: hasDecEq.eq_op has the following canonical values:
    - @eq_op (from "./eqtype.v", line 137)
    - eqb
    - BinNat.N.eqb
    - eqn
    - @eqseq
    - @opt_eq
    - @pair_eq
    - @sum_eq
    - @tag_eq
    - true

maybe having directly on which types there is an equality would be good.

The most valuable tool for me has been the #[verbose], seeing what is actually created is great but
I have no idea how to cope with the message

Ignoring canonical projection to ... redundant with ...

Does it mean that I've been doing something wrong? is there always a way to get rid of these messages?
It also makes me wonder if the way I build things is not the proper way to do it.
Maybe some support on guiding the user would be interesting. Given a state, being able to get what is
actually missing to equip a type T with a structure S would be great.

view this post on Zulip Pierre Roux (Oct 31 2023 at 16:24):

Laurent Théry said:

I have no idea how to cope with the message

Ignoring canonical projection to ... redundant with ...

Does it mean that I've been doing something wrong? is there always a way to get rid of these messages?
It also makes me wonder if the way I build things is not the proper way to do it.

FWIW we have disactivated that warning in mathcomp itself so it's prebably fine ignoring it. That being sai, I don't know how hard it would be to avoid it, disactivating that important warning doesn't feel good to me either.

Laurent Théry said:

Maybe some support on guiding the user would be interesting. Given a state, being able to get what is
actually missing to equip a type T with a structure S would be great.

Have you tried HB.howto? (see https://github.com/math-comp/math-comp/blob/master/etc/porting_to_mathcomp2/porting.pdf )

view this post on Zulip Cyril Cohen (Nov 02 2023 at 07:03):

For the warning, there used to be a missing piece of API in Coq and/or Coq Elpi to selectively disable canonical projections (hence without silencing warnings altogether), we should definitely implement it now. I thought there was an open issue for this, but it does not seem to be the case yet. Would you be willing to open it?

view this post on Zulip Laurent Théry (Nov 02 2023 at 09:33):

@Pierre Roux howto is nice but I think it is static : it does not take into account my current state. What would be nice if , let's say I want to be build a FiniteFieldType on some type T, the tool would tell me that I just need to fullfil isFinite. This Ignoring made me feel I was unnecessary redoing something. I guess HB has lots of information on how best it is to build a given structure.

view this post on Zulip Cyril Cohen (Nov 02 2023 at 09:38):

@Laurent Théry howto is dynamic and tells you what remains to instantiate

view this post on Zulip Laurent Théry (Nov 02 2023 at 09:41):

So you do HB.about eqType T and it tells you how to equip T with an eqType?

view this post on Zulip Cyril Cohen (Nov 02 2023 at 09:47):

Laurent Théry said:

So you do HB.about eqType T and it tells you how to equip T with an eqType?

The other way around and with howto (HB.howto T eqType) but yes:
Usage: HB.howto [(<type>)|<structure>] <structure> [<search depth>].

view this post on Zulip Laurent Théry (Nov 02 2023 at 09:51):

Perfect, Thanks!

view this post on Zulip Cyril Cohen (Nov 02 2023 at 09:52):

If you do not have a type at hand I think you can even put a structure instead and it will do the diff, e.g. back to your original example:
HB.howto fieldType finiteFieldType will tell you to use isFinite

view this post on Zulip Cyril Cohen (Nov 02 2023 at 09:53):

(and HB.howto T finiteFieldType too if T was already canonically a field)

view this post on Zulip Laurent Théry (Nov 02 2023 at 09:57):

so if there are several possibilities how are they ranked?

view this post on Zulip Pierre Roux (Nov 02 2023 at 10:03):

shortest first (heuristically it's often what you are looking for but not always)

view this post on Zulip Laurent Théry (Nov 02 2023 at 10:04):

Not sure what you mean by shortest.

view this post on Zulip Pierre Roux (Nov 02 2023 at 10:10):

by number of factories to successively use, for instance

From mathcomp Require Import all_ssreflect ssralg.
From HB Require Import structures.

HB.howto choiceType ringType.

answers

HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
    - GRing.isRing
    - GRing.isSemiRing; GRing.Nmodule_isZmodule
    - GRing.isZmodule; GRing.Nmodule_isSemiRing
    - GRing.isZmodule; GRing.Zmodule_isRing
    - GRing.isNmodule; GRing.Nmodule_isZmodule; GRing.Nmodule_isSemiRing
    - GRing.isNmodule; GRing.Nmodule_isZmodule; GRing.Zmodule_isRing

where isRing comes before isZmodule; Zmodule_isRing

view this post on Zulip Laurent Théry (Nov 02 2023 at 10:16):

Thanks a lot!

view this post on Zulip Laurent Théry (Nov 02 2023 at 10:27):

I have this kind of sequence

HB.instance Definition _ := [Equality of GI by <:].
HB.instance Definition _ := [Choice of GI by <:].
HB.instance Definition _ := [Countable of GI by <:].
HB.instance Definition _ := [SubChoice_isSubZmodule of GI by <:].
HB.instance Definition _ := [SubZmodule_isSubRing of GI by <:].
HB.instance Definition _ := [SubRing_isSubComRing of GI by <:].

what is the strategy to minimize it?

view this post on Zulip Pierre Roux (Nov 02 2023 at 10:45):

You can try to remove the Equality and Choice (if Countable does them). Then you can look in the doc if there isn't some SubChoice_isSubComRing that would compund the last three

view this post on Zulip Laurent Théry (Nov 02 2023 at 11:48):

Ok

HB.instance Definition _ := [Countable of GI by <:].
HB.instance Definition _ := [SubChoice_isSubComRing of GI by <:].

seemd to be equivalent

view this post on Zulip Laurent Théry (Nov 02 2023 at 13:10):

Cyril Cohen said:

For the warning, there used to be a missing piece of API in Coq and/or Coq Elpi to selectively disable canonical projections (hence without silencing warnings altogether), we should definitely implement it now. I thought there was an open issue for this, but it does not seem to be the case yet. Would you be willing to open it?

done

view this post on Zulip Pierre Roux (Nov 02 2023 at 13:17):

Do we really want to silence the warning? Shouldn't we rather, when adding a canonical instance, check if it already exist (and maybe also check that the already existing one is indeed the expected one)?

view this post on Zulip Notification Bot (Nov 03 2023 at 09:30):

Laurent Théry has marked this topic as resolved.

view this post on Zulip Cyril Cohen (Nov 03 2023 at 16:26):

Pierre Roux said:

Do we really want to silence the warning? Shouldn't we rather, when adding a canonical instance, check if it already exist (and maybe also check that the already existing one is indeed the expected one)?

These warnings are about projections that are not used for canonical inference. They keep getting the same keys because the proofs or ops may be the same (or have the same head symbol), but not the main key (S.sort) which must be different each time, and for these: yes there should be a check in HB that occurs before Coq discovers a duplicate key. The latter problem should indeed have the solution you described, whereas the former (which AFAIK is the one Laurent encounters) should be solved by informing Coq which projections are not keyed.


Last updated: Apr 21 2024 at 02:41 UTC