Stream: math-comp users

Topic: SSProve in MC CI?


view this post on Zulip Bas Spitters (May 15 2023 at 11:23):

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

view this post on Zulip Pierre Roux (May 15 2023 at 11:37):

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

view this post on Zulip Pierre Roux (May 15 2023 at 11:53):

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

view this post on Zulip Bas Spitters (May 15 2023 at 11:57):

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

view this post on Zulip Pierre Roux (May 15 2023 at 12:00):

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

view this post on Zulip Bas Spitters (May 15 2023 at 12:03):

https://github.com/arthuraa/deriving
Adding @Arthur Azevedo de Amorim .
Should deriving be replaced by the more modern (?) Elpi based solution by @Enrico Tassi ?

view this post on Zulip Enrico Tassi (May 15 2023 at 12:07):

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

view this post on Zulip Bas Spitters (May 15 2023 at 12:12):

I'm guessing extructures also needs those :-(

view this post on Zulip Bas Spitters (May 15 2023 at 12:19):

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.

view this post on Zulip Kazuhiko Sakaguchi (May 15 2023 at 12:24):

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.

view this post on Zulip Bas Spitters (May 15 2023 at 14:09):

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

view this post on Zulip Kazuhiko Sakaguchi (May 16 2023 at 10:04):

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

view this post on Zulip Arthur Azevedo de Amorim (May 16 2023 at 15:39):

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

view this post on Zulip Pierre Roux (May 16 2023 at 15:57):

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.

view this post on Zulip Pierre Roux (May 16 2023 at 15:58):

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

view this post on Zulip Pierre Roux (May 17 2023 at 15:48):

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

view this post on Zulip Bas Spitters (May 18 2023 at 08:10):

Thanks for trying!

view this post on Zulip Bas Spitters (Jun 04 2023 at 10:48):

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

view this post on Zulip Pierre Roux (Jun 04 2023 at 12:22):

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.

view this post on Zulip Bas Spitters (Jun 05 2023 at 10:31):

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?

view this post on Zulip Bas Spitters (Jun 05 2023 at 10:50):

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

view this post on Zulip Arthur Azevedo de Amorim (Jun 05 2023 at 13:35):

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

view this post on Zulip Enrico Tassi (Jun 05 2023 at 13:39):

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.

view this post on Zulip Enrico Tassi (Jun 05 2023 at 13:42):

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

view this post on Zulip Cyril Cohen (Jun 05 2023 at 13:44):

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

view this post on Zulip Arthur Azevedo de Amorim (Jun 05 2023 at 14:57):

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

view this post on Zulip Paolo Giarrusso (Jun 05 2023 at 17:23):

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?

view this post on Zulip Arthur Azevedo de Amorim (Jun 05 2023 at 19:56):

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

view this post on Zulip Enrico Tassi (Jun 05 2023 at 20:01):

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.

view this post on Zulip Paolo Giarrusso (Jun 05 2023 at 20:04):

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?

view this post on Zulip Paolo Giarrusso (Jun 05 2023 at 20:07):

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

view this post on Zulip Bas Spitters (Jul 06 2023 at 10:51):

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

view this post on Zulip Arthur Azevedo de Amorim (Jul 07 2023 at 14:22):

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

view this post on Zulip Bas Spitters (Jul 07 2023 at 14:49):

Thanks! That's great news.

view this post on Zulip Bas Spitters (Feb 22 2024 at 09:22):

@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