Update ocaml_version for coq:dev CI to run. Closes #23

[k4rtik]

No description provided.

[k4rtik]

So it seems that 8.12 image is not available with 4.12-flambda and dev is not available with 4.07-flambda. To obtain clean CI run, we should consider dropping 8.12, which is almost two years old now.

Generally, in providing these images, they provide support for "The last two compatible OCaml versions", see https://github.com/coq-community/docker-coq/wiki#supported-tags

@khieta thoughts? I am making this change to let the CI run.

[k4rtik]

If this change feels good, please feel free to merge.

[khieta]

Thanks for looking at this @k4rtik!

https://github.com/coq-community/docker-coq/wiki#supported-tags says that they'll build each version of Coq with "OCaml 4.07.1+flambda, which has been widely tested (see e.g. this post) and is compatible with each Coq since 8.7". Is that no longer accurate?

[k4rtik]

@khieta clearly not, since dev doesn't have those images anymore. It also doesn't make sense in the long-term as Coq will ultimately drop support for older OCaml versions (though currently, the minimum version is 4.05, which is unoptimized and slower). The wiki page was last updated on Dec 9, 2021.

[k4rtik]

I made a post at https://coq.discourse.group/t/install-notes-on-ocaml-versions-and-coq-configuration/713/21?u=kartik so that someone provides updated guidance on which version to use.

[khieta]

Sounds good. Can we use a different version of OCaml for 8.12 only? I'd like to still test 8.12 since our proofs should work for it.

[k4rtik]

It should be possible, but I was not able to figure it out last night. I will wait for some response to my post on Coq Discourse.

[k4rtik]

Hi @khieta what's the summary here now? I am somewhat confused after not looking at this for two weeks.

In my reading, it seems from their available images and updated OCaml version policy we might be better off using 4.13*-flambda for maximum compatibility.

[khieta]

@k4rtik I merged your original PR this morning, but found that it didn't build. I guess they switched from 4.12-flambda to 4.13-flambda. My latest PR works, but I'd like to see if I can figure out how to run different versions of OCaml for different versions of Coq. It looks like they don't guarantee that 4.13-flambda will work in the future for Coq versions < 8.16.

[k4rtik]

Oh, you were already doing it. I didn't see the PR #25

It looks like they don't guarantee that 4.13-flambda will work in the future for Coq versions < 8.16.

I don't think we can solve this problem once and for all. It will require updating versions in our yml file over time until we decide to stop maintaining (that's just the nature of maintenance).

I think we can stick to their "default" version for our CI.

OCaml 4.13.1+flambda (the "default" version for Coq ≥ 8.16)

ie, when that gets updated, we update the yml file.