OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
130 stars 33 forks source link

Do not use lock file for all OCaml versions #1195

Closed Halbaroth closed 1 month ago

Halbaroth commented 1 month ago

In the current version of our workflow, we use an opam lock file to ensure that we can reproduce builds. Unfortunately, there are different conflicts depending on the plateform and OCaml version. We use a hack to prevent opam from saving the version of OCaml's toolchain (see the target lock in our Makfile). This hack is not sufficient if we want to use the current workflow build on Windows.

This PR modifies the workflow build and the Makefile as follows:

  1. We check the reproducibility only on OCaml 4.14.1. I choose this version because we both develop on this version with Nix.
  2. We checked the Makefile on OCaml 4.14.2, which is strange because we check the installation with opam on OCaml 4.14.1. I replace 4.14.1 by 4.14.2.
  3. I remove the flag -y in the target dev-switch, deps and test-deps because we use OCAMLYES in our workflows and Makefile's users want to check dependencies before running a slow task as opam switch create or opam install.
bclement-ocp commented 1 month ago

I don't see a reason to test using 4.14.1 now that 4.14.2 is out. We can update the pinned nixpkgs if we want consistency with the nix version.

Couple questions:

Halbaroth commented 1 month ago

In the current version of this PR, the CI on OCaml 4.08 and 5.0 uses only one constraint: the version of OCaml. In my opinion, the main purpose of the lock file is to automatize bisections and most of the time, it is sufficient to do it with our dev environment. Checking our code works with older version of libraries is made by the CI of opam-repository. We can reproduce this behaviour here. Basically the CI of opam-repository checks if our package builds with a smallest solution of the constraints on its dependencies. In my opinion, it makes more sense than checking arbitrary version of libraries.

All the current conflicts can be solved by choosing precise versions of libraries. Windows' support adds an extra layer of complexity when we have to choose the library.

bclement-ocp commented 1 month ago

In the current version of this PR, the CI on OCaml 4.08 and 5.0 uses only one constraint: the version of OCaml.

But they are still using the lockfile (at least the workflow sets OPAMLOCKED), which now (I suppose — you did not include the new lockfile in the PR, which I assume is an omission) explicitly states the version of OCaml to use. I admit I am not 100% up to date on how lockfiles work but I thought that would not work.

Halbaroth commented 1 month ago

@bclement-ocp It seems I cannot ping you for this review, uhm strange. Anyway, this PR is ready for a second pass.