Karl Palmskog (Aug 04 2023 at 17:39): Karl Palmskog (Aug 04 2023 at 17:39):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)
Karl Palmskog (Aug 04 2023 at 17:46):I did a PR and people can comment there if something is amiss: https://github.com/coq/opam-coq-archive/pull/2648
Enrico Tassi (Aug 04 2023 at 21:26):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
Karl Palmskog (Aug 04 2023 at 21:27):OK, can/should I do the MC2 bound relaxation PR?
Enrico Tassi (Aug 04 2023 at 21:27):As soon as we have 8.18 docker images I believe the MC2.0 ecosystem can be tested.
Enrico Tassi (Aug 04 2023 at 21:27):I think so.
Karl Palmskog (Aug 08 2023 at 14:43):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.
Karl Palmskog (Aug 08 2023 at 14:43):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
Enrico Tassi (Aug 10 2023 at 12:00):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.
Karl Palmskog (Aug 10 2023 at 12:14):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")
Karl Palmskog (Aug 10 2023 at 12:19):actually, let me compare MC2 on 8.18 on OCaml 4.14.1 vs. OCaml 5.1-rc1
Last updated: Sep 09 2024 at 04:02 UTC