Stream: Coq devs & plugin devs

Topic: ocaml 4.12


view this post on Zulip Gaëtan Gilbert (Feb 26 2021 at 17:12):

Are we compatible with ocaml 4.12? If not what's missing?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 26 2021 at 17:34):

Yes, I have been tracking 4.12 for a while, at least the dune build should work fine [with 4.08, not sure if older dune versions may need a workaround due to some changes when stubs are module-less]

view this post on Zulip Emilio Jesús Gallego Arias (Feb 26 2021 at 17:35):

Will submit a PR, the only thing I found is that warning 16 appears in a few places, and it is indeed a warning we may want to get rid of?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 26 2021 at 17:35):

The warning is when functions are of the form val func : ?foo:t -> bar:t -> t , so ?foo cannot be indeed eliminated in partial application

view this post on Zulip Emilio Jesús Gallego Arias (Feb 26 2021 at 17:36):

Usually this is solved by adding a dummy unit argument, what do you think? [For example as we do in Declare.CInfo.make () etc...

view this post on Zulip Théo Zimmermann (Feb 26 2021 at 17:39):

Oh that's a very nice warning! I have often stumbled upon this issue in my OCaml programming.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 26 2021 at 17:43):

4.12 got better at detecting this I think, so I think I'll update the API, hopefully we need no overlays.


Last updated: Mar 28 2024 at 20:01 UTC