based on my local testing, 1.17.0 works fine with 8.18+rc1. Should I relax bounds in opam? (2.0.0 still needs Coq-Elpi/HB tags before test)
I did a PR and people can comment there if something is amiss: https://github.com/coq/opam-coq-archive/pull/2648
I released HB 1.5.0 which works with the last coq-elpi (and the last elpi). That is the combo which makes MC2 compile with reasonable memory footprint
OK, can/should I do the MC2 bound relaxation PR?
As soon as we have 8.18 docker images I believe the MC2.0 ecosystem can be tested.
I think so.
memory usage for MC 2.0 on 8.18 is looking pretty good, but the time to compile all of core MathComp 2.0.0 still feels pretty slow, even on state-of-the-art hardware. I guess we can count on binary distributions helping out.
another thing that might help would be to get better file-level parallelism, but I don't think there are any plans in that direction
I guess after the summer break we will make another point on performance. At the time of the first release It was pretty bad but now it seems reasonable. I surely need a detailed analysis to see what to optimize further.
sounds good, the above was just my intuition after compiling a bunch of opam switches with various MC versions ("MC 2.0 on 8.18 still feels kinda slow")
actually, let me compare MC2 on 8.18 on OCaml 4.14.1 vs. OCaml 5.1-rc1
Last updated: Nov 29 2023 at 20:01 UTC