Stream: math-comp devs

Topic: 8.18 compatibility


view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Aug 04 2023 at 21:27):

OK, can/should I do the MC2 bound relaxation PR?

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Aug 04 2023 at 21:27):

I think so.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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")

view this post on Zulip 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...

5.1 was actually a few percent faster on getting to coq-mathcomp-character.2.0.0 from scratch. I guess this might be because nearly all files are so large, so the many-small-files problems on OCaml 5 don't kick in


Last updated: May 18 2024 at 08:40 UTC