Stream: Coq devs & plugin devs

Topic: ocamldebug slow on ocaml 4.11?


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

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

view this post on Zulip Gaëtan Gilbert (Aug 20 2020 at 12:24):

looks like it starts with 4.10

view this post on Zulip Emilio Jesús Gallego Arias (Sep 17 2020 at 14:15):

We should report this upstream.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 17 2020 at 14:17):

Asking in slack for now

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 17 2020 at 14:23):

Unfortunately that is 4.12 only it seems

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

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

view this post on Zulip Paolo Giarrusso (Sep 18 2020 at 10:48):

(unless you can shift that to the OCaml devs)

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Sep 18 2020 at 19:09):

Sounds like a good idea?

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

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

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

view this post on Zulip 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: Oct 21 2021 at 21:03 UTC