[ocaml] Version bump for 8.16 ?

[ejgallego]

Hi folks,

there was some discussion about bumping the supported version of OCaml for 8.15 [IMHO 8.14 is out of the question]

I am opening this issue to centralize discussion.

There are several options here, the way I can see it:

• stay at 4.05: pros: stability, cons: nothing that is a blocker IMO , so we could stay
• go to 4.07: pros: Stdlib module, some issues solved, better Stdlib, , cons still a bit old
• 4.08: pros: monadic syntax, even more improvements for stdlib; cons bug in VM setting parameters [fixed in > 4.11.2], slowdown significant slowdown with ocaml 4.08.1 #11652 (fixed in >=8.12)
• 4.10: cons ocamldebug became very slow ocaml/ocaml#9606 slow ocamldebug (also 4.11, 4.12)
• 4.11: pros: good baseline for the next 3-4 years; many bugfixes and improvements, a couple of regressions cons too new?
• 4.12: cons: Fatal error: debugger does not support channel locks ocaml/ocaml#10517 ocamldebug doesn't work (also 4.13)

Regarding distro support, stable distros should ship with 4.11 for the 8.15 timeline, IIANM.

[ejgallego]

Please write / edit with yout own pros/cons

cc @Zimmi48

[JasonGross]

• cons bug in VM setting parameters [fixed in > 4.11.2]

What's this about? Note that even Debian sid and Ubuntu impish only ship 4.11.1, so I don't think you'll be seeing a fix for this in stable distros for a while.

[ejgallego]

What's this about?

That's ocaml/ocaml#9326 , and indeed it landed in the 4.11 branch in 4.11.2, but the patch is fairly small so debian could also path 4.11 by themselves.

[JasonGross]

Perhaps Coq should emit a warning if it was compiled by a bad version of OCaml without OCAMLRUNPARAM setting the GC settings, and coq_makefile should set OCAMLRUNPARAM in these cases?

[ejgallego]

Overkill IMHO, users should be careful enough to use the recommended setup.

[ppedrot]

There were some performance issues with the OCaml compilation between > 4.07 and < 4.11 IIRC. They would lead to coq-native being unusable. Last time we discussed the matter I think that there was a weak consensus that we should jump directly from 4.07 to 4.11 when we need to specify the minimal version of Coq.

Since I believe 4.11 is way too recent, it means we have to stick to at least 4.07 for quite a time. In which case, since 4.07 doesn't really provide any benefit compared to 4.05 (does it?), there is not much incentive to bump the minimal version to 4.07.

[JasonGross]

Overkill IMHO, users should be careful enough to use the recommended setup.

If you want to go this route, you should update "Other installation methods" https://coq.inria.fr/download to say that we explicitly disrecommend installing Coq or even building Coq from the system OCaml on all Ubuntu versions newer than bionic/18.04 and on all Debian versions newer than buster, due to performance issues, perhaps linking the relevant OCaml/Coq issue. Moreover, dune 2.5 requires either ocaml >=4.07 & <4.12 or else ocamlfind-secondary and hence ocaml-secondary-compiler which only exists for 4.08.1. I'm not aware of any Ubuntu/Debian packaging of ocaml-secondary-compiler which means that building Coq for Ubuntu/Debian packaging requires at least 4.07. But 4.07 is not packaged on Debian nor Ubuntu, so this means that Coq cannot be built in a recommended way with any system packages. I'd like my packages of various Coq versions to keep being useful on CI. (Perhaps the thing to do is to have my packages patch CoqMakefile.in with the GC setting?)

[JasonGross]

I think at least it would be reasonable to add a warning at

coq/sysinit/coqinit.ml

Lines 41 to 45 in f5743b1

	(* OCAMLRUNPARAM environment variable is not set.
	* In this case, we put in place our preferred configuration.
	*)
	set_gc_policy ();
	if Coq_config.caml_version_nums >= [4;10;0] then set_gc_best_fit () else ()

that will emit a warning with a suggested string setting of OCAMLRUNPARAM if the version is mismatched. I don't suppose it's possible to check that the record setting changed only the specified fields without depending on the complete list of fields? (Can we use polymorphic equality to test that the Gc state after set equals the record we tried to set it to?)

[SkySkimmer]

ocamldebug is dead slow in 4.10 / 4.11, and breaks on threads in 4.12 / 4.13 (ocaml/ocaml#10517)
So the latest we can bump to is 4.09 imo

[ejgallego]

10517 is supposed to be fixed in OCaml's trunk, is the case that they are slow too?

You recall the bug number for the slow ocamldebug stuff? [was it due to plugins?]

I think bump to 4.08 would be the most reasonable, on the other hand I don't still see a reason to bump the OCaml version beyond that.

[SkySkimmer]

Trunk is not a released version
The slowness was ocaml/ocaml#9606 IIRC

[ejgallego]

If the trunk fix works it'd be reasonable to backport it, at least to 4.13.2

[Zimmi48]

I think bump to 4.08 would be the most reasonable, on the other hand I don't still see a reason to bump the OCaml version beyond that.

It seems to me that bumping the minimal required version of OCaml to 4.08 is not reasonable until we have a solution to the linkall problem #12067 (since the only simple workaround that we can give users is to use OCaml 4.07). See a recent instance of this here: ejgallego/coq-serapi#260.

[ejgallego]

Indeed, that's a tricky one; note that merely suggesting people to use 4.07 is unfortunately not a solution, but just a workaround, if users do hit a double-link situation it is likely that some kind of corruption could happen even if OCaml doesn't complain about it.

[gares]

The double link problem seems the most severe one to me.

The solution seems to use something like findlib to actually load code (and its dependency) and assume all (ocaml) dependencies are available as .cmxs (which is the case if they are compiled with dune, IIRC).
@ejgallego you pointed out that dune provides an high level API for plugins. Is it still based on findlib behind the scenes?

[gares]

Also, it says

WARNING: This feature remains experimental and is subject to breaking changes without warning. It must be explicitly enabled in the dune-project file with (using dune_site 0.1)

Do you know what are the plans for this feature?

[ejgallego]

@gares discussion is mainly at #12067 , also see #14019 , however that ran into some problems due to findlib.dynload needing the META file to be generated earlier than what it's done in the current Coq build.

In general I'd say that the status of plugins in OCaml is pretty precarious, mainly due to the need to use -linkall [see https://github.com/ocaml/dune/issues/4957 ] , but maybe we can live with that.

@bobot sites feature looks pretty promising too, but it uses binary rewriting on install so that may be a no-go for us unfortunately :( :( That could be fixed.

But both systems are based on the same idea, which I have used with success in other projects, so if someone would put a bit of time to try any of the approaches, we could make things work for Coq IMHO.

[bobot]

Could you elaborate about the binary rewriting is a no-go?

[ejgallego]

Could you elaborate about the binary rewriting is a no-go?

We don't want to run dune install to get a usable Coq.

[ejgallego]

Moreover, it kinda breaks the expectation that the binary that is produced by the compilation is the final binary. This is IMO a reasonable expectation and breaking it would create many headaches I feel.

[bobot]

Moreover, it kinda breaks the expectation that the binary that is produced by the compilation is the final binary.

My point of view is that what is in _build is the realm of Dune. Files are finalized only when they are put outside _build. It simplify reasoning (more abstraction, clearer API) and lessen headache.

We don't want to run dune install to get a usable Coq.

dune exec -- coq would work and is the recommended use. Promoting the binary works but less recommended (some edge cases remains). Is there a problem with dune exec -- coq?

[SkySkimmer]

dune exec only works if started in the right directory

[ejgallego]

Unfortunately Coq and Coq development remains too complex to simplify things so much; there are many many developer workflows that rely on low-level access. Also binary rewriting is ugly, and I don't see why it is needed here instead of simpler solution [like having a meta file next to the binary]

So using the sites plugin as it is now, would imply that I'd have to fight a battle with half of the Coq developers, a battle I'm not willing to fight when coqc stops working for half of them.

Maybe in the future when have a more polished workflow.

[ejgallego]

To be clear here, the problem is that everyone in this project has a model that "install" means "copy" ; this is actually reasonable. Breaking that means re-educating dozens of people, not an easy task, specially when the justifications for the breakage are not very strong.

I already had enough sufferance with a much simpler task, trying to achieve an hygienic build :S

[ppedrot]

Unearthing this issue since the findlib patch has fixed the link problem. We should keep a table in the top post with the pro and cons of the potential versions (e.g. the issue with #11652 is drowned in the discussion).

[ejgallego]

@ppedrot you got some particular wish for a version bump?

Myself I'm OK for now with 4.05 , I don't really need anything from above right now.

[gares]

I don't see 4.09 up there? are there any cons? I'm using it and I've no problems.

[SkySkimmer]

Same as 08, it's a bit slower

[SkySkimmer]

The table may be more readable as

cons:

• 4.08 <= _ < 4.12: bug in VM setting parameters (not sure what this refers to)
• 4.08 <= _ < 4.12: slowdown significant slowdown with ocaml 4.08.1 #11652
• 4.10 <= _ < 4.13: ocamldebug became very slow ocaml/ocaml#9606 slow ocamldebug
• 4.12 <= _ < 4.14: Fatal error: debugger does not support channel locks ocaml/ocaml#10517 ocamldebug doesn't work

[gares]

what about applying this fix locally to Coq for the slowdown: noppa/flow@81e8447

[gares]

FTR the slowdown is cause byt a bug in Gc.set which can be worked around in the application, so the second problem is not blocking IMO.

[ppedrot]

We could even roll up our own C implementation of Gc.set, since we've already shipping C code in Coq.

[ejgallego]

The fix indeed seems worth applying.

[ppedrot]

Note that bumping to 4.08 would allow removing the Format API that is deprecated in latest 4.x OCaml versions and removed in the current 5.0 branch.

[ejgallego]

Yup 4.08 seems like the next natural step, maybe for 8.17 tho

[SkySkimmer]

see also #15399

[ppedrot]

We should have discussed this yesterday :/ I think that bumping to 4.08 makes sense. Did we include our own local patch for the GC issue already?

[ejgallego]

We should have discussed this yesterday :/ I think that bumping to 4.08 makes sense. Did we include our own local patch for the GC issue already?

Actually I am not sure, but indeed, if the platform can be upped to 4.12 for example that shouldn't matter anymore.

[Zimmi48]

The Platform should be updated to 4.13 in 2022.03 actually (now that Elpi is compatible).

[Zimmi48]

4.09 has not been considered in the OP, but it could also make sense (released in Sept 2019, minimal OCaml version required for lablgtk 3.1.2, does not have the ocamldebug issues starting at 4.10).

[ejgallego]

Looking at repology we could also go to 4.11.0

Main reason to stay at 4.08 is that Ubuntu LTS is stuck at 4.08 indeed.

[Zimmi48]

Main reason to stay at 4.08 is that Ubuntu LTS is stuck at 4.08 indeed.

Actually, the next LTS will be 22.04, which will be released before Coq 8.16 and which contains OCaml 4.13.1.

[ejgallego]

Yes I saw that, but maybe that's a bit too close? I don't mind either way.

[ppedrot]

FTR, we decided to bump to 4.08 for Coq 8.16, but before actually enforcing this we need to fix the GC issue using the aforementioned patch.

[gares]

if this is funal you should also update ci

[Zimmi48]

@ppedrot Interesting that you recall 4.08 while the notes seemed to suggest 4.09: https://github.com/coq/coq/wiki/Coq-Call-2022-04-06. But what is clear from the discussion is that you, as the RM, should decide.

Just reminding that if we bump to 4.08 and not to 4.09, we will still have to ask for a new lablgtk version that would be compatible with 4.08 in order to merge #15399.

Note that the main reason for wanting to stay on 4.08 was the version in the latest Ubuntu LTS, but Ubuntu 22.04 was just released and ships with 4.13.1.

[ppedrot]

Oh, right, I misremembered. The one difference between 4.08 and 4.09 was the support of the new lablgtk release, and that was enough to tip the balance. Indeed, the above post should read 4.09 then.

[ppedrot]

I've also realized in the meantime that with this bump we will be able to use the -linscan option for the native compiler. It was introduced in 4.06.

[herbelin]

What are the recommended versions for developers? E.g. ocamldebug 4.11.2 seems (still) slow.

[Alizter]

4.14 works fine now, I don't know about ocamldebug though. Our new min is 4.09.

[Zimmi48]

4.09 was supposed to be the last working version with ocamldebug, but recent OCaml versions are supposed to work as well.

[herbelin]

Sorry, I messed up the test. 4.11.2 ocamldebug is ok. Thanks for the recommendations.