Stream: math-comp users

Topic: How to automate inheriting two canonical structures ?


view this post on Zulip walker (Nov 13 2022 at 20:06):

So I have a canonical structure as follows:

Structure serDe :=  Pack{
    CST: Type;
    ops: operations CST;
    lms: lemmas ops;
}.

and then there eqType and I am trying to specify types that implement both serDe + eqType

so I had:

Module SerDeEqType.

Record mixin T := Mixin {
    Eq_type: Equality.mixin_of T;
    SerDe_ops: SerDe.operations T;
    SerDe_lemmas: SerDe.lemmas SerDe_ops;

}.
Record type := Class {
    SEQ: Type;
    ops: mixin SEQ;
}.
Definition to_eq (t: type) : eqType :=
    Equality.Pack (Eq_type (SEQ t) (ops t)).
Definition to_serde (t: type) : serDe :=
    SerDe.Pack (SerDe_lemmas (SEQ t) (ops t)).
End SerDeEqType.

Canonical Structure SerDeEqType.to_eq.
Canonical Structure SerDeEqType.to_serde.

But the problem is I still need to manually implement SerDeEqType.type for every type that implements both CS, I tried thinking of way of doing it automatically, but it didn't work. What would be the mathcomp idomatic way of handling this problem?

view this post on Zulip Cyril Cohen (Nov 16 2022 at 12:42):

Hi, the modern answer to that problem is https://github.com/math-comp/hierarchy-builder
Unfortunaltely to work properly with eqType you need to wait for the next major release of mathcomp...

view this post on Zulip Enrico Tassi (Nov 16 2022 at 13:16):

An alpha release is scheduled for Christmas

view this post on Zulip Enrico Tassi (Nov 16 2022 at 13:16):

(really)

view this post on Zulip walker (Nov 16 2022 at 13:27):

alright, here is a question,

Scared of making your project depend on HB? This section is for you.

so what make you think that people would think that depending on HB is problem in this particular when compared to other coq code ?

view this post on Zulip walker (Nov 16 2022 at 13:28):

also does that mean that mathcomp will also depend on HB ?

view this post on Zulip Alexander Gryzlov (Nov 16 2022 at 13:59):

Yeah I think that's the plan for 2.0

view this post on Zulip Enrico Tassi (Nov 16 2022 at 14:04):

walker said:

alright, here is a question,

Scared of making your project depend on HB? This section is for you.

so what make you think that people would think that depending on HB is problem in this particular when compared to other coq code ?

It is not specific to HB or Coq either. People who wants to build a project in the long term do look at what they depend on. This is not always the case for research projects, but sometimes it is. And it is also subjective, some people buy stock options some other don't ;-)

view this post on Zulip Enrico Tassi (Nov 16 2022 at 14:05):

I think that explaining what HB commands do in terms of regular Coq commands is reassuring for a non negligible class of users, this is what that documentation section is about

view this post on Zulip Enrico Tassi (Nov 16 2022 at 14:07):

On a side note, the fact that we can run MC 2.0 + HB + ... in the browser is quite reassuring for me, e.g. it will make my teaching life a lot easier. I would not have bet on this one year ago. [I'm still working on that page, it may be broken from time to time].

view this post on Zulip Enrico Tassi (Nov 16 2022 at 14:08):

There are many aspects to be considered, and "how hard will it be for students to run it" is one of them.

view this post on Zulip Ricardo (Nov 17 2022 at 23:06):

Cyril Cohen said:

Hi, the modern answer to that problem is https://github.com/math-comp/hierarchy-builder
Unfortunaltely to work properly with eqType you need to wait for the next major release of mathcomp...

What do you mean by to work properly? So far I've been under the impression that eqType works properly, at least in some senses. In what sense does eqType doesn't work properly?


Last updated: Feb 08 2023 at 08:02 UTC