Stream: Coq devs & plugin devs

Topic: Puzzling error


view this post on Zulip Ali Caglayan (Oct 08 2021 at 12:28):

What is going on here:
https://github.com/coq/coq/pull/15000/checks?check_run_id=3838330986

view this post on Zulip Pierre-Marie Pédrot (Oct 08 2021 at 12:30):

Looks like an OCaml bug?

view this post on Zulip Gaëtan Gilbert (Oct 08 2021 at 12:35):

https://github.com/ocaml/ocaml/issues/10027

view this post on Zulip Pierre-Marie Pédrot (Oct 08 2021 at 12:39):

Coq: the only in-depth user of the worst parts of the OCaml type system out there

view this post on Zulip Guillaume Melquiond (Oct 08 2021 at 12:43):

So, we have exception definitions that use inline records? Was someone really concerned about the cost of OCaml exceptions?

view this post on Zulip Gaëtan Gilbert (Oct 08 2021 at 12:59):

inline records aren't about cost, they're about being able to give names to the fields without having to do some

type contents_of_foo = ...
... of contents_of_foo

boilerplate

view this post on Zulip Pierre-Marie Pédrot (Oct 08 2021 at 13:04):

Bah, it's not useful for exceptions since most of the time there is only one single client destructing the record, i.e. the printer


Last updated: Feb 06 2023 at 18:03 UTC