jasmin
jasmin copied to clipboard
jasmin-lang
Port to MathComp 2
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.
@vbgl please ping me whenever you plan to merge this so that we can avoid breaking Coq's CI too much.
The CI machine ran out of memory. Is this just bad luck or the sign of a real regression?
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.
Coq 8.17.0 is known to have a dramatic memory issue, could you try with another version?
I did not spot that. If you are with that combo of coq, coq-elpi and HB the perfs are very bad.
Indeed, apparently it's much better. Let me pin jasmin in Coq's CI and as far as I'm concerned, this is mergable.
Indeed, apparently it's much better.
How do you know? What’s a good way to measure time & memory consumption of coqc?
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.
@vbgl with https://github.com/coq/coq/pull/18402 merged, merging the current PR won't break Coq's CI.
What’s the meaning of all these new warnings? Should we pay attention to them or just silence them?
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]
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
Thanks. I’ve thus disable this warning, rebased, and launched CI.
There are some deprecated notations that should be fixed.
Some timing measurements were done with with make -j1 TIMED=1 on main (c262bdfa5fb11ae87f036409663608a4fbd6fdfc) and on this branch, on an otherwise idle machine. Here are a few selected highlight.
Total run time: before 11mn, after 17mn. Total memory (GiO): before 93, after 123.
Before: arch/arch_decl.vo (real: 1.82, user: 1.73, sys: 0.08, mem: 698964 ko) lang/expr.vo (real: 2.68, user: 2.56, sys: 0.11, mem: 720996 ko) lang/warray_.vo (real: 3.57, user: 3.43, sys: 0.14, mem: 653992 ko) lang/slh_ops.vo (real: 1.14, user: 1.00, sys: 0.13, mem: 644856 ko)
After: arch/arch_decl.vo (real: 9.99, user: 9.82, sys: 0.17, mem: 1152512 ko) lang/expr.vo (real: 9.73, user: 9.56, sys: 0.16, mem: 1175444 ko) lang/warray_.vo (real: 7.27, user: 7.09, sys: 0.17, mem: 948232 ko) lang/slh_ops.vo (real: 5.50, user: 5.34, sys: 0.16, mem: 933132 ko)
With which version of Coq \ coq-elpi \ hierarchy-builder? In any case, that seems typical of what we observe on mathcomp or mathcomp analysis themselves.
Coq 8.18, mathcomp 2.1.0, hb 1.5.0, coq-elpi 1.19.0 (ocaml-elpi 1.17.0)
Good to know it is typical. But is it acceptable?
Those are indeed the last released versions. We still have ideas for improvement so it is likely to further improve in the future. For instance, the forthcoming release of HB will come with https://github.com/math-comp/hierarchy-builder/pull/391
I think we’ll wait a bit before moving to mathcomp-2. Currently, the performance regression is to large, and the benefits are not clear.
Have you tried with the latest hierarchy-builder 1.7? this may bring interesting performance improvements.
What is the status of this? We have updated SSProve to MC2.0 and would also like to update the jasmin part.
This is stuck due to performance regressions that would be induced by the move to MC2.
Is the performance regression still unacceptable with hierarchy-builder 1.7?
I’ve spent too much time on this PR already; I may give a try to hb1.7 in a couple of months.
Is the performance regression still unacceptable with hierarchy-builder 1.7?
@cmester0 mentioned that HB 1.7 still has similar timings on his machine :-(
A short investigation hints that HB.instance is slow. We know that, and the only workaround (for now) is to minimize imports.
With this patch:
diff --git a/proofs/arch/arch_decl.v b/proofs/arch/arch_decl.v
index f607225e..81f8b430 100644
--- a/proofs/arch/arch_decl.v
+++ b/proofs/arch/arch_decl.v
@@ -1,6 +1,6 @@
(* -------------------------------------------------------------------- *)
From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
From mathcomp Require Import word_ssrZ.
From Coq Require Import
Relation_Operators
I go from
$ time make arch/arch_decl.vo
make -f Makefile.coq arch/arch_decl.vo
make[1]: Entering directory '/home/tassi/COQ/master/_build_ci/jasmin/proofs'
COQDEP VFILES
COQC arch/arch_decl.v
make[1]: Leaving directory '/home/tassi/COQ/master/_build_ci/jasmin/proofs'
real 0m7,645s
user 0m7,219s
sys 0m0,386s
to
$ time make arch/arch_decl.vo
make -f Makefile.coq arch/arch_decl.vo
make[1]: Entering directory '/home/tassi/COQ/master/_build_ci/jasmin/proofs'
COQDEP VFILES
COQC arch/arch_decl.v
make[1]: Leaving directory '/home/tassi/COQ/master/_build_ci/jasmin/proofs'
real 0m3,863s
user 0m3,543s
sys 0m0,319s
since order.vo declares a load of structures, and HB.instance has a bad complexity on that factor.