Dependency issues

Open palmskog opened this issue 9 months ago • 3 comments

MathComp 1.X is end-of-life and will soon not be supported by Rocq
Dependency on CompCert rules out compilation on OCaml 5 (may be better to bundle required .v files)

Mar 14 '25 08:03 palmskog

The issue of compcert and ocaml5 is here: https://github.com/AbsInt/CompCert/issues/477

Mar 14 '25 09:03 spitters

Thanks for the notice and the pointer! Updates ongoing.

Mar 15 '25 22:03 raoxiaojia

The repository has now moved to MathComp 2.x (#65). I'll leave the CompCert/OCaml 5 compilation for now -- this issue is therefore not closed at the moment.

Mar 17 '25 14:03 raoxiaojia