Port to MathComp 2 #560

proux01 · 2023-09-05T08:30:58Z

bgregoir

Thank a lot for this PR, I have the impression that a lot of boilerplate are simplified.
I have added some small remarks.
Also what is the level of maturity of mathcomp2 ?
I notice that our code is simplified but except that did you gain other things with this change ? I notice that we need a much recent version of Coq, did we loose something else ?

bgregoir · 2023-09-06T13:59:14Z

proofs/arch/arch_extra.v

@@ -273,7 +274,7 @@ Variant extended_op :=

 Definition extended_op_beq o1 o2 :=
  match o1, o2 with
-  | BaseOp o1, BaseOp o2 => eq_op (T:= prod_eqType _ ceqT_eqType) o1 o2
+  | BaseOp o1, BaseOp o2 => @eq_op (_ * ceqT_eqType)%type o1 o2


The name T is no longer available, or it is a question of style ?

It's now called s (for sort I guess) for all structures, we should maybe change that but this will require some hacking into hierarchy-builder, not sure it's worth it. Anyway, Enrico's solution is much better here:

| BaseOp o1, BaseOp o2 => o1 == o2 :> _ * ceqT_eqType

bgregoir · 2023-09-06T14:02:28Z

proofs/compiler/x86_instr_decl.v

 Definition wpblendw (m : u8) (w1 w2 : word U128) :=
  let v1 := split_vec U16 w1 in
  let v2 := split_vec U16 w2 in
  let b := split_vec 1 m in
-  let r := map3 (λ (b0 : word.word_ringType 0) (v3 v4 : mathcomp.word.word.word U16), if b0 == 1%R then v4 else v3) b v1 v2 in
+  let r := map3 (λ (b0 : (mathcomp.word.word.word 1 : ringType)) (v3 v4 : mathcomp.word.word.word U16), if b0 == 1%R then v4 else v3) b v1 v2 in


word.word_ringType 0 is the same than
mathcomp.word.word.word 1 ?

Yes, word.word_ringType 0 was a ring structure on word 0.+1 (which is moral since ring requires 0 != 1 which doesn't hold on empty words), at least this is now much clearer.

bgregoir · 2023-09-06T14:03:16Z

proofs/lang/expr.v

@@ -534,7 +527,7 @@ Variant saved_stack :=
 Definition saved_stack_beq (x y : saved_stack) :=
  match x, y with
  | SavedStackNone, SavedStackNone => true
-  | SavedStackReg v1, SavedStackReg v2 => v1 == v2
+  | (SavedStackReg v1), SavedStackReg v2 => v1 == v2


Why parenthesis here?

A nasty parsing error on v1:

Error: Syntax error: '|' or '=>' expected (in [eqn])

no idea where it comes from.

bgregoir · 2023-09-06T14:04:45Z

proofs/lang/memory_model.v

@@ -722,7 +722,8 @@ Proof.
  have [hle hlt] := wunsigned_range (p - wrepr Uptr sz).
  have := Z.mod_le _ _ hle (wsize_size_pos ws).
  have := Z_mod_lt (wunsigned (p - wrepr Uptr sz)) (wsize_size ws) ltac:(done).
-  by Psatz.lia.
+  move=> [? ?] ?; split; first exact: Zle_minus_le_0.


Psatz.lia does not work anymore with the change? Or it was very slow ?

lia was no longer working because we had for some reason both GRing_Zmodule__to__GRing_Nmodule (GRing_ComRing__to__GRing_Zmodule (word Uptr)) and GRing_ComRing__to__GRing_Nmodule (word Uptr) which are convertible but not syntactically equal, hence not the same variable for lia. Maybe using https://github.com/math-comp/mczify/ would help but not sure since there is a mix of stdlib and mathcomp in those arithmetic expressions.
I pushed a (slightly) better fix for now.

bgregoir · 2023-09-06T14:06:57Z

proofs/lang/word.v

@@ -2136,6 +2136,7 @@ Proof.

  rewrite Z.shiftl_mul_pow2; last done.
  split; first Psatz.lia.
-  rewrite /wbase (modulusD 64 64) modulusE -expZE /=.
-  exact: Zmult_lt_compat_r.
+  rewrite /wbase (modulusD 64 64) modulusE -expZE.


This seem much more complicated. What is the motivation for the change ?

The apply: Zmult_lt_compat_r was no longer working (or terribly slow) I didn't really investigate why. There might be a simpler fix.

gares

Some comments from the coffee room

gares · 2023-09-06T13:48:12Z

proofs/lang/memory_model.v

-  by Psatz.lia.
+  move=> [? ?] ?; split; first exact: Zle_minus_le_0.
+  by apply: Z.le_lt_trans hlt; apply: (Z.le_sub_nonneg _ _).1.


Can you explain why this lia does not work anymore?
Do we need algebra-tactics for this to work?

C.f. above #560 (comment)

gares · 2023-09-06T14:51:14Z

proofs/arch/arch_extra.v

-  | BaseOp o1, BaseOp o2 => eq_op (T:= prod_eqType _ ceqT_eqType) o1 o2
+  | BaseOp o1, BaseOp o2 => @eq_op (_ * ceqT_eqType)%type o1 o2


Maybe we could have an Arguments directive to name the implicit T (either here or in MC2).
Also putting the argument in type_scope should make the %type unneeded.
But I also wonder if o1 == o2 :> (_ * ceqT_eqType) would just do it.

We could indeed fix that in MC2, not sure it's worth the effort though.
Your solution here is much better anyway, I kept it.

proux01 · 2023-09-06T16:02:36Z

what is the level of maturity of mathcomp2 ?

A number of major reverse dependencies have already been successfully ported: abel, analysis, comp-dec-modal, coqeal, coquelicot, finmap, fourcolor, gaia, graph-theory, interval, mczify, multinomials, odd-order, real-closed, reglang, tarjan and others work with both MC1 and MC2 (basically devs that don't instantiate any structure).
It is now out since a bit more than three months. There has been some performance issues that we are still improving (particularly with Coq 8.17.0, fixed in 8.17.1). Mathcomp 1 remains maintained and features easily backported will be available there but major new developments now happen on MC2, so no hurry.

I notice that our code is simplified but except that did you gain other things with this change ?

Not much. There are new structures for semirings and semigroups (useful for instance for bigop with min and max when they don't have a neutral element and hence cannot be equipped with a monoid structure) that you may benefit. But honestly, my main motivation was that Jasmin is now among the main unported dev both in nixpkgs and Coq CI so if we want MC2 to be made the default there, this will have to be ported at some point.

I notice that we need a much recent version of Coq,

Coq >= 8.16, that's indeed one year more recent than 8.14 currently required by Jasmin.

did we loose something else ?

MC2 requires hierarchy-builder, itself requiring coq-elpi to build so the dependency chain is a bit longer. But that's more mathcomp developers' problem than yours.

Compilation time and memory use might also be a bit larger: on mathcomp itself and mathcomp Analysis, compilation typically requires 30 to 40% more memory and takes a bit less than 3 times longer, but those are heavy users of elaborate structures, for you use case the impact is probably much less.

proux01 · 2023-12-07T18:07:12Z

@vbgl please ping me whenever you plan to merge this so that we can avoid breaking Coq's CI too much.

vbgl · 2023-12-07T18:11:55Z

Sure. Thanks for your help. I’ve just rebased and launched CI.

vbgl · 2023-12-11T13:19:14Z

The CI machine ran out of memory. Is this just bad luck or the sign of a real regression?

gares · 2023-12-11T14:55:36Z

Compilation time and memory use might also be a bit larger: on mathcomp itself and mathcomp Analysis, compilation typically requires 30 to 40% more memory and takes a bit less than 3 times longer, but those are heavy users of elaborate structures, for you use case the impact is probably much less.

I think we need to look into it in order to know what happens in this specific case. Sometimes the new layout of structures/classes (that is flat) is a bit worse in terms of term comparison performance. The issue popped up a couple of times in MC. On the good side in MC2 we have a very handy locking mechanism which helps to hide "large terms" behind opaque symbols.

proux01 · 2023-12-11T22:58:48Z

Coq 8.17.0 is known to have a dramatic memory issue, could you try with another version?

gares · 2023-12-12T07:46:13Z

I did not spot that. If you are with that combo of coq, coq-elpi and HB the perfs are very bad.

proux01 · 2023-12-13T08:31:11Z

Indeed, apparently it's much better.
Let me pin jasmin in Coq's CI and as far as I'm concerned, this is mergable.

In order to be able to merge jasmin-lang/jasmin#560 without breaking Coq's CI.

vbgl · 2023-12-13T09:17:18Z

Indeed, apparently it's much better.

How do you know? What’s a good way to measure time & memory consumption of coqc?

proux01 · 2023-12-13T09:20:45Z

Indeed, apparently it's much better.

How do you know?

Well, it's working whereas it wasn't but I don't know more.

What’s a good way to measure time & memory consumption of coqc?

When using coq_makefile, doing make -j1 TIMED=1 works fine.

proux01 · 2023-12-13T12:01:37Z

@vbgl with coq/coq#18402 merged, merging the current PR won't break Coq's CI.

vbgl · 2024-01-08T07:34:18Z

What’s the meaning of all these new warnings? Should we pay attention to them or just silence them?

proux01 · 2024-01-08T07:43:15Z

Which one?

vbgl · 2024-01-08T07:50:15Z

All of them. Here is one, for instance:

File "./lang/utils.v", line 77, characters 0-90:
Warning: Ignoring canonical projection to isCountable.pickleK by
Choice_isCountable.pickleK in
choice_isCountable__to__choice_Choice_isCountable: redundant with
choice.choice_isCountable__to__choice_Choice_isCountable
[redundant-canonical-projection,records,default]

proux01 · 2024-01-08T08:14:37Z

All of them.

I was asking because I no longer see any CI result here.

Here is one, for instance:

File "./lang/utils.v", line 77, characters 0-90:
Warning: Ignoring canonical projection to isCountable.pickleK by
Choice_isCountable.pickleK in
choice_isCountable__to__choice_Choice_isCountable: redundant with
choice.choice_isCountable__to__choice_Choice_isCountable
[redundant-canonical-projection,records,default]

I see, the fact that those warnings are displayed is a bug of HB, they should be ignored, for the record, here is what we have in our _CoqProject for mathcomp:

-arg -w -arg -projection-no-head-constant
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -notation-overridden

eponier · 2024-05-22T16:43:01Z

I merged PR #801. The CI reveals an error with version 2.2.0 of mathcomp that I don't know how to fix.

proux01 · 2024-05-22T17:21:01Z

Looks like a Nix issue, you should ask @vbgl I guess.

vbgl · 2024-05-22T18:41:24Z

The fix is to wait for latest mathcomp to be available in CI. This might take a couple of weeks and require to address #803.

eponier · 2024-05-22T18:47:19Z

Sorry, I don't get it, what is the link between the latest mathcomp and this Jasmin bug?

vbgl · 2024-05-22T19:04:32Z

Updating the CI environment might bring in recent binutils.

gares · 2024-05-23T12:43:04Z

I did look at the other PR, and left a comment.

Can we consider this PR unblocked? I mean, it has to wait for CI, but other than that, is it sufficient? Should we put more energy in making it faster before the merge? Knowing that HB.instance will get faster, eventually.

vbgl · 2024-05-24T14:14:18Z

Rebased and run the measurements again.

Total run time: before 11mn, after 14mn.
Total memory (GiO): before 91, after 117.

I can no longer find any file with a dramatic increase in cost.

eponier · 2024-05-24T14:24:00Z

Ouch:

job coq-program: 25mn instead of 5mn
job coq-proof: 30mn instead of 10mn

Why is this so different from Pierre's numbers? I noticed you rolled back to mathcomp 2.1. Does this mean that we really need 2.2?

vbgl · 2024-05-24T14:26:01Z

I think you are comparing the time to build math-comp 2 vs the time to download math-comp 1. This does not look fair.

eponier · 2024-06-05T09:01:08Z

@vbgl Now that #822 is merged, can you rebase and select mathcomp 2.2 as a dependency? Or did I misunderstand once more how nix and our CI is working?

vbgl · 2024-06-05T09:34:58Z

I will, but there is no hurry.

vbgl · 2024-06-12T14:47:26Z

Rebased on top of recent main branch, updated to use mathcomp 2.2.0.

eponier · 2024-06-12T16:27:08Z

coq-master fails for whatever reason, but the other results are good.

job coq-program: 7mn instead of 5mn
job coq-proof: 10mn instead of 10mn

(I'm not sure that I didn't miss some external factor like I did previously, such as caching)

gares · 2024-06-12T20:27:18Z

Note that this very week we are having a sprint to optimize HB.instance, see https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Builder-devs-.26-users/topic/Hierarchy.20Builder.20optimization.20sprint

I guess we will make a release of HB soon, although I don't know how much you will gain now that the imports are minimized. For sure you won't lose anything ;-)

eponier · 2024-06-14T13:03:30Z

@vbgl please ping me whenever you plan to merge this so that we can avoid breaking Coq's CI too much.

@proux01 I'm about to merge.

eponier · 2024-06-14T13:31:26Z

Thanks everyone involved for your time on this PR!

Now that jasmin-lang/jasmin#560 is merged

bgregoir reviewed Sep 6, 2023

View reviewed changes

gares reviewed Sep 6, 2023

View reviewed changes

proux01 force-pushed the mathcomp2 branch from 44450ff to e050274 Compare September 6, 2023 15:31

proux01 force-pushed the mathcomp2 branch from e050274 to 38735b2 Compare September 11, 2023 09:25

ppedrot mentioned this pull request Nov 22, 2023

[CI] Temporary fix for coqword coq/coq#18344

Merged

vbgl force-pushed the mathcomp2 branch from 38735b2 to 498b1de Compare December 7, 2023 18:02

vbgl mentioned this pull request Dec 7, 2023

CI: update nixpkgs & nix #663

Merged

This was referenced Dec 7, 2023

[ssr] Backport from MathComp coq/coq#18374

Merged

[CI] Temporarily turn jasmin allow_failure coq/coq#18388

Merged

eponier mentioned this pull request Dec 12, 2023

CI: use Coq 1.18 & mathcomp 1.18.0 #665

Merged

vbgl force-pushed the mathcomp2 branch from 498b1de to 969690c Compare December 12, 2023 12:35

proux01 added a commit to proux01/coq that referenced this pull request Dec 13, 2023

Pin Jasmin

fe2687c

In order to be able to merge jasmin-lang/jasmin#560 without breaking Coq's CI.

proux01 mentioned this pull request Dec 13, 2023

Pin jasmin coq/coq#18402

Merged

vbgl force-pushed the mathcomp2 branch from 969690c to a0ea36d Compare December 21, 2023 12:09

vbgl force-pushed the mathcomp2 branch from a0ea36d to 2bf22dd Compare January 8, 2024 08:38

vbgl mentioned this pull request May 23, 2024

Do not require all_ssreflect jasmin-lang/coqword#30

Closed

vbgl force-pushed the mathcomp2 branch from cbad9fb to 6316d69 Compare May 24, 2024 12:22

proux01 marked this pull request as ready for review May 24, 2024 14:16

eponier mentioned this pull request Jun 3, 2024

CI: update nixpkgs (to channel 24.05) #822

Merged

vbgl added this to the 2024.06.0 milestone Jun 12, 2024

vbgl force-pushed the mathcomp2 branch from 6316d69 to 63a8460 Compare June 12, 2024 13:16

Port to MathComp 2

1039c07

vbgl force-pushed the mathcomp2 branch from 63a8460 to 1039c07 Compare June 13, 2024 14:03

vbgl approved these changes Jun 13, 2024

View reviewed changes

eponier merged commit 9abca78 into jasmin-lang:main Jun 14, 2024
1 check passed

proux01 deleted the mathcomp2 branch July 24, 2024 18:13

proux01 added a commit to proux01/coq that referenced this pull request Jul 30, 2024

[CI] Unpin Jasmin

234c612

Now that jasmin-lang/jasmin#560 is merged

proux01 mentioned this pull request Jul 30, 2024

[CI] Unpin Jasmin coq/coq#19432

Merged

proux01 added a commit to proux01/coq that referenced this pull request Jul 31, 2024

[CI] Unpin Jasmin

2a20f96

Now that jasmin-lang/jasmin#560 is merged

		\| BaseOp o1, BaseOp o2 => eq_op (T:= prod_eqType _ ceqT_eqType) o1 o2
		\| BaseOp o1, BaseOp o2 => @eq_op (_ * ceqT_eqType)%type o1 o2

Port to MathComp 2 #560

Port to MathComp 2 #560

Conversation

proux01 commented Sep 5, 2023

bgregoir left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gares left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

proux01 commented Sep 6, 2023

proux01 commented Dec 7, 2023

vbgl commented Dec 7, 2023

vbgl commented Dec 11, 2023

gares commented Dec 11, 2023

proux01 commented Dec 11, 2023

gares commented Dec 12, 2023

proux01 commented Dec 13, 2023

vbgl commented Dec 13, 2023

proux01 commented Dec 13, 2023

proux01 commented Dec 13, 2023

vbgl commented Jan 8, 2024

proux01 commented Jan 8, 2024

vbgl commented Jan 8, 2024

proux01 commented Jan 8, 2024

eponier commented May 22, 2024

proux01 commented May 22, 2024

vbgl commented May 22, 2024

eponier commented May 22, 2024

vbgl commented May 22, 2024

gares commented May 23, 2024

vbgl commented May 24, 2024

eponier commented May 24, 2024 • edited Loading

vbgl commented May 24, 2024

eponier commented Jun 5, 2024

vbgl commented Jun 5, 2024

vbgl commented Jun 12, 2024

eponier commented Jun 12, 2024 • edited Loading

gares commented Jun 12, 2024

eponier commented Jun 14, 2024 • edited Loading

eponier commented Jun 14, 2024

eponier commented May 24, 2024 •

edited

Loading

eponier commented Jun 12, 2024 •

edited

Loading

eponier commented Jun 14, 2024 •

edited

Loading