Interrupting after a few seconds makes it say it's stopped while building unicode tables (Unicode. mk_lookup_table_from_unicode_tables_for)
There was a bug reported about this IIRC, which is due to a bad algorithmic complexity in debug tables
looks like it starts with 4.10
We should report this upstream.
Asking in slack for now
It's https://github.com/ocaml/ocaml/issues/9606 and should have been solved by https://github.com/ocaml/ocaml/pull/9635
Unfortunately that is 4.12 only it seems
Is there a recent version of OCaml devoid of any issue for Coq? :place_of_worship:
Do Coq devs have a way to test OCaml prereleases? Resources, I know, but it does seem necessary?
(unless you can shift that to the OCaml devs)
@Paolo Giarrusso there used to be this: https://github.com/coq/coq-bench
But as per an earlier comment from Emilio, it seems it has been decommissioned
Emilio's comments without the context can be misinterpreted. The infrastructure is still available, it has been integrated into our GitLab CI infrastructure.
By "testing", I don't mean if you meant specifically performance testing or something more general but FYI Coq is usually tested with OCaml trunk (for compatibility).
Testing for compatibility is good, but it seems your goals are that OCaml releases work “well” with Coq (defining “well” is up to you), and that doesn’t seem to be the case
Yeah, well. You can always test so much. Sure, we could do more, but the ocamldebug issue for instance really needs developers actively using the new version to be discovered.
Sounds like a good idea?
I don't have perfect solutions, but there seems to be a systematic problem for some reason.
and it’s not unusual that “big enough consumers” (like you) end up doing some extra maintenance on their deps.
(e.g. as a mere postdoc, I’ve tweaked Coq’s opam packages for my own need, which are still public, and now I shared them with my colleagues — luckily we’re progressing toward a fix for that problem, as extensively discussed here)
OTOH, of course, resources. “git bisect ocamlc to identify the GC regressions” doesn’t sound easy (and doesn’t guarantee a fix), and tuning GCs is pretty expensive anyway...
Last updated: Oct 21 2021 at 21:03 UTC