Stream: Coq devs & plugin devs

Topic: ml or mli only?


view this post on Zulip Gaëtan Gilbert (Sep 28 2021 at 14:55):

We have some modules which are ml only even though they could be mlis (eg declarations)
We also have a few mli only modules (eg csig)

IIRC there were some problems with make and mli only, but we have only dune now

Shall we go back to mli only where possible?

view this post on Zulip Enrico Tassi (Sep 28 2021 at 14:57):

What is the advantage of a .mli without an .ml, with respect to an .ml without an .mli?

view this post on Zulip Enrico Tassi (Sep 28 2021 at 14:58):

Having both is boring, but I can't see much of a difference between the two options, other than pure .ml can declare exceptions

view this post on Zulip Emilio Jesús Gallego Arias (Sep 28 2021 at 15:02):

Just .ml used also to behave better w.r.t. to the foo_intf.ml pattern include as to avoid duplication of interfaces between .ml / .mli files. There are also differences about aliases, modules without implementation couldn't be aliased. So indeed I think we renamed to some .ml not due to make problems, but due to the old API.mlifile using module alias.

This pattern is used pervasively in some of the OCaml ecosystem.

IMHO, we should discuss a bit about the different styles and options.

view this post on Zulip Guillaume Melquiond (Sep 28 2021 at 15:05):

Enrico Tassi said:

What is the advantage of a .mli without an .ml, with respect to an .ml without an .mli?

Actually, that is a question I asked on OCaml's Discourse earlier today. If you have a .ml without .mli, OCaml complains. If you have a .mli without .ml, OCaml is happy. https://discuss.ocaml.org/t/dealing-with-warning-70-missing-mli/8542/4

view this post on Zulip Emilio Jesús Gallego Arias (Sep 28 2021 at 15:11):

The compiler is happy until you want to do something such as module F = Foo where only foo.mli exists.

The discussion in discuss.ocaml is kind of incomplete; Dune has not problem with .mli only files, the compiler has as it doesn't support the same set of features for example w.r.t. packing. So dune workarounds this limitation by automatically generating an implementation file for .mli-only modules. I can point out to the relevant issues if anyone is interested.

Personally, I find warning 70 activated by default to be a really bogus choice.

view this post on Zulip Enrico Tassi (Sep 28 2021 at 15:15):

IIRC the problem with make and .ml only files was that if you run in parallel ocaml/ocamlopt you get a race on the .cmi. But I guess dune does this right. So, what is wrong with .ml only files? (other than the warning which can be disabled globally)

view this post on Zulip Guillaume Melquiond (Sep 28 2021 at 15:27):

I just removed 1600 lines of dead code in Why3 thanks to this warning, so I am not eager to disable it.

view this post on Zulip Gaëtan Gilbert (Sep 28 2021 at 15:51):

mli without ml ensures you don't start adding vals in the module

view this post on Zulip Pierre-Marie Pédrot (Sep 28 2021 at 19:39):

@Gaëtan Gilbert I agree with your remark, ml files without a corresponding mli file are footguns begging for use. Interfaces are precisely that, they are guaranteed to only contain declarations. ml-only files are the equivalent of broken C headers where you can actually create code without realizing.

IMO this whole discussion is due to a limitation of OCaml, i.e. we should be able to consider implementation-free interfaces as if they were modules as well. Or a build system feature where mli-only files are duplicated on the fly into the corresponding ml file. Shouldn't be too hard to do?

view this post on Zulip Pierre-Marie Pédrot (Sep 28 2021 at 19:40):

(another minor defect is that it reduces greppability. I know that only mli files should matter for declarations but that's not true if you only have an ml file. This is annoying for the stuff that used to be mli-only like kernel/declarations and similar AST-defining files)

view this post on Zulip Rudi Grinberg (Nov 30 2021 at 19:12):

Or a build system feature where mli-only files are duplicated on the fly into the corresponding ml file. Shouldn't be too hard to do?

That’s exactly what dune does already :)


Last updated: Dec 05 2023 at 05:01 UTC