Gaëtan Gilbert (Aug 20 2020 at 12:08): Gaëtan Gilbert (Aug 20 2020 at 12:08):Interrupting after a few seconds makes it say it's stopped while building unicode tables (Unicode. mk_lookup_table_from_unicode_tables_for)
Pierre-Marie Pédrot (Aug 20 2020 at 12:10):There was a bug reported about this IIRC, which is due to a bad algorithmic complexity in debug tables
Gaëtan Gilbert (Aug 20 2020 at 12:24):looks like it starts with 4.10
Emilio Jesús Gallego Arias (Sep 17 2020 at 14:15):We should report this upstream.
Emilio Jesús Gallego Arias (Sep 17 2020 at 14:17):Asking in slack for now
Pierre-Marie Pédrot (Sep 17 2020 at 14:17):It's https://github.com/ocaml/ocaml/issues/9606 and should have been solved by https://github.com/ocaml/ocaml/pull/9635
Emilio Jesús Gallego Arias (Sep 17 2020 at 14:23):Unfortunately that is 4.12 only it seems
Pierre-Marie Pédrot (Sep 17 2020 at 14:24):Is there a recent version of OCaml devoid of any issue for Coq? :place_of_worship:
Paolo Giarrusso (Sep 18 2020 at 10:46):Do Coq devs have a way to test OCaml prereleases? Resources, I know, but it does seem necessary?
Paolo Giarrusso (Sep 18 2020 at 10:48):(unless you can shift that to the OCaml devs)
Karl Palmskog (Sep 18 2020 at 10:50):@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
Théo Zimmermann (Sep 18 2020 at 10:55):Emilio's comments without the context can be misinterpreted. The infrastructure is still available, it has been integrated into our GitLab CI infrastructure.
Théo Zimmermann (Sep 18 2020 at 10:55):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).
Paolo Giarrusso (Sep 18 2020 at 11:07):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
Théo Zimmermann (Sep 18 2020 at 12:44):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.
Paolo Giarrusso (Sep 18 2020 at 19:09):Sounds like a good idea?
Paolo Giarrusso (Sep 18 2020 at 19:09):I don't have perfect solutions, but there seems to be a systematic problem for some reason.
Paolo Giarrusso (Sep 18 2020 at 19:10):and it’s not unusual that “big enough consumers” (like you) end up doing some extra maintenance on their deps.
Paolo Giarrusso (Sep 18 2020 at 19:12):(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)
Paolo Giarrusso (Sep 18 2020 at 19:14):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: Dec 07 2023 at 09:01 UTC