Congratulations on the release of 2.0.

https://github.com/math-comp/math-comp/releases/tag/mathcomp-2.0.0

I see MC has it's own CI. Would it be possible to add SSProve there?

https://github.com/SSProve/ssprove

Sure, MC's CI is mostly based on Nix so the first step would be to add it to nixpkgs.

But this probably won't work with MC 2 since we are lacking deriving hence extructures (Hierarchy-Builder was lacking support for universe polymorphism at the time I attempted to port it, some support has been added since but deriving ended up never being ported).

We've been considering moving from extructures to finmap. Are you saying that this would actually be required for getting into CI?

For the master branch (MC 2) yes, either that or porting deriving.

https://github.com/arthuraa/deriving

Adding @Arthur Azevedo de Amorim .

Should deriving be replaced by the more modern (?) Elpi based solution by @Enrico Tassi ?

It depends what you need. Elpi's derive can do eqType, but not countType or choiceType for example.

I'm guessing extructures also needs those :-(

I recall @Yannick Forster and co-workers made a similar functionality based on meta-coq, https://arxiv.org/abs/2006.15135

I don't know whether it would be relevant here.

If `concrete_groups.v`

is the only place you actually use the Deriving package, it seems to me that it shouldn't be difficult to get rid of the dependency by declaring instances by hand.

@Kazuhiko Sakaguchi Thanks that's a great suggestion. That indeed appears to be the case.

https://github.com/search?q=repo%3ASSProve%2Fssprove+deriving&type=code

However, I understand that @Pierre Roux was mostly worried about the dependency of extructures on deriving.

I think that the same argument applies to extructures. It does not seem to depend on deriving in an essential way.

Bas Spitters said:

https://github.com/arthuraa/deriving

Adding Arthur Azevedo de Amorim .

Should deriving be replaced by the more modern (?) Elpi based solution by Enrico Tassi ?

I am trying to port deriving to mathcomp 2.0. But I am not sure how much time this might take...

Great, I'd expect the port to be either relatively easy (following the tutorial) if the universe thing is no longer an issue or impossible.

Here was my initial attempt: https://github.com/proux01/deriving/tree/hierarchy-builder

I gave it a second try but it seems that universe polymorphism is still a blocking point.

Thanks for trying!

@Pierre Roux Would making a universe monomorphic version of deriving and extructures be a possible temporary solution?

I'm not sure how crucial the use of polymorhpism is in deriving/extructures.

Universe polymorphism seems to be the only blocker so I would indeed expect a monomorphic version to work with MC 2. Following the porting tutorial https://github.com/math-comp/math-comp/blob/master/etc/porting_to_mathcomp2/porting.pdf should be enough to complete the port but feel free to ask if you have more precise questions.

I expect that a monomorphic version would be enough for SSProve.

@Arthur Azevedo de Amorim what do you think would be the best way to proceed?

I'm inclined to think that getting a monomorphic deriving into MC CI will already catch many things, but I may be overlooking something.

I've been trying to port Deriving to math-comp 2.0.0, but it's proving a bit more challenging than I expected. The universe issues turned out to be easy to solve, but it's unclear how to interface properly with Hierarchy Builder. In particular, Deriving uses directly some of the boilerplate code that used to be written by hand in math-comp 1.X, and is now considered part of the HB internals. I wonder if it'll be necessary to interface with HB directly at the level of Elpi. @Enrico Tassi I might need some help with this :)

Sure, but not this week (or not interactively). If you have the time to open an issue (on HB) explaining your exact need, that would help. Otherwise we can set up a visio next week. Next week, Wednesday, 10AM (paris time) is also the regular math-comp virtual meeting, but I guess the time does not suite you.

I suspect this feature https://github.com/math-comp/hierarchy-builder/wiki/FeatherFactory is what you need, but it is just an educated guess.

I can also try to help asynchronously (for now). If you want to share a blocking point I can take a look

@Enrico Tassi @Cyril Cohen Thanks! I'll write you once I have a clearer picture of what the issue is.

naive question but how would `deriving`

compare/overlap with https://github.com/LPCIC/coq-elpi/tree/master/apps/derive/theories/derive ? The builtin instances clearly overlap, I'm curious about the rest — they seem like they could be a bit complementary?

@Paolo Giarrusso As far as I know, the Elpi derivation infrastructure only works for `eqType`

. It could in principle handle other classes as well, but right now there isn't any support for this.

I think that Deriving's way of generating instances would in principle yield smaller terms, because everything is done using dependently typed meta programming. Everything should be linear in the size of the inductive declaration in question. However, in practice we have noticed that Deriving doesn't scale as well as it should, for reasons yet to be understood. Maybe @Enrico Tassi can add a few words to this.

I think you are right on both your remarks.

I can only add that the classes of inductives supported by the two tools are different, or have different requirements.

Elpi's derive has no support for mutual inductives, but requires less input when used on containers.

Elpi's derive supports types with parameters which are values (e.g. mathcomp's tuples) if these parameters are only used in irrelevant fields (e.g. boolean propositions).

IIRC my last paper on derive has a table comparing features more precisely, but I think I did point out the main ones.

what about CPP'23 https://dl.acm.org/doi/abs/10.1145/3573105.3575683 ? That claims linear times as well, with benchmarks? Fig. 8 seems close or better than `deriving`

?

hmm, I guess I should just look more closely at the paper

@Arthur Azevedo de Amorim Did you manage to find out what the issue is?

@Bas Spitters I've managed to get it to compile, but I think it still needs some work before a stable release. FYI, I am tracking some of the issues here: https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/Porting.20Deriving.20to.20math-comp.202.2E0.2E0.

Thanks! That's great news.

@Lasse Letager Hansen has now upgraded SSProve. He will do a release. What are the next steps to get this in CI.

We'll also have a nix build if it helps.

Upgrading to MC2.0 is waiting for the inefficiencies in HB 1.7 to be fixed:

https://github.com/jasmin-lang/jasmin/pull/560

Last updated: Jul 15 2024 at 20:02 UTC