As noted in the discussion here, there is no explicit documentation about what OCaml compiler version and options the Platform is using. Since the Platform is in some sense a "recommended solution" to compiling and working with Coq, I think it would be good to state this as part of Platform README for each release / package pick
It's actually explicitly documented. See e.g., here. But perhaps you mean that this information should be put forward more clearly?
so people are supposed to scan through the list of 40+ packages, and know by heart what "ocaml-option-flambda.1 (1) Set OCaml to be compiled with flambda activated" means? I don't think that's reasonable
I assume part of the motivation is https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/problem.20with.20sudo.20make.20install so we also have evidence of at least one mislead user
anyway, I realized now my reply sounded unnecessarily harsh, bottom line is that I will try to make a documentation PR when I get a moment to spare, I just think it's a good thing if we can get some OCaml recommendation out there
(as plugin maintainer OCaml version management is tough)
It is a bit tricky to document it at high level and correctly, because it depends on the Coq version (not all picks use the same version of OCaml). But one for sure could put it in the header of the auto generated readme files.
Yes, I think this would be sufficient.
Btw.: if one uses the scripts - which I guess users caring about the OCaml version do - then
opam switch is the way to check the OCaml version. The installers are not intended for people who need to care about the OCaml version.
Last updated: Jan 30 2023 at 11:03 UTC