Vincent Laporte

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] ~~~

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

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?

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.

This is stuck due to performance regressions that would be induced by the move to MC2.

I’ve spent too much time on this PR already; I may give a try to hb1.7 in a couple of months.

Just rebased after the « less algebra » PR. Ooh, CI failed: > 11680 Killed

I don’t use `liquidsoap`. I’ve just observed that in its latest release, there is an ill-typed program that the build system will actively try to build. So here is a...

CI: https://gitlab.com/jasmin-lang/jasmin/-/pipelines/751942335 Do we want to run some benchmarks?