Clean up the lock file

[Halbaroth]

The lock file contains several dependencies that are not related to the package alt-ergo-lib.opam. In particular, it contains dependencies related to the JavaScript package and they cannot be installed in a switch with OCaml 5.6.0.

This commit removes them, upgrades the locked dune version to 3.24.2 and improves the filter performed by make lock.

The findlib cannot be locked because it may contrain the OCaml version.

[bclement-ocp]

I'm not sure I understand why that is a problem — the lockfile shouldn't force installing these dependencies if they are not otherwise requested I think?

[bclement-ocp]

Apparently it does, given the test failures :/ I don't know why opam even calls this a lockfile…

[Halbaroth]

To be honest, I don't understand the lockfile feature of opam.
Note that the Make all job failed on opam install . --deps-only --with-test .

On my laptop, if I run:

opam sw create foo --empty --no-switch
opam install --switch foo . --deps-only --with-test

opam installs qcheck. But if I run the last command with --locked, opam doesn't install qcheck...

[Halbaroth]

After reading opam help lock and asking questions on Zulip, I understood few things about the command

opam install ./foo.opam --deps-only --locked

1. opam completely ignores the dependencies of the file foo.opam if there is a foo.opam.locked file. For instance,
   qcheck wasn't in the locked file, so opam install didn't install it although it was in the opam file.
2. all the installed optional dependencies of foo are added to the lock file as dependencies. For instance, run

opam switch create foo 5.4.1 --empty --no-switch
opam install --switch foo . --deps-only
opam lock --switch foo -w ./alt-ergo-lib.opam

the package js_of_ocaml is added to alt-ergo-lib.opam.locked as it is a mandatory dependency of alt-ergo-js.opam
and an optional dependency of alt-ergo.opam by transitivity.

Generating lock files from an existing switch is risky because it could incorporate undesired optional dependencies. Running

opam switch create foo 5.4.1 --empty --no-switch
opam install --switch foo . --deps-only --with-test
opam lock --switch foo ./alt-ergo.opam ./alt-ergo-lib.opam ./alt-ergo-js.opam

will produce good lock files to install all the Alt-Ergo packages in a recent switch but these lock files couldn't work with
OCaml 5.6.0 as they includes several dependencies with ppx.

The last commits introduce a new strategy to generate lock files:

1. We don't generate a lock file for alt-ergo-js package,
2. For alt-ergo and alt-ergo-lib packages, the script installs them in a fresh switch, generates lock files and removes
   all the dependencies related to the OCaml compiler itself with opam-ed.

[bclement-ocp]

I think that works. Just one concern about the generate_lock_file.sh script, I think it might accidentally remove a user's current switch if called directly.

[bclement-ocp]

This should either have a hardcoded default value or fail before setting the trap cleanup EXIT otherwise this risks removing the user's switch, no? I'm not too sure about how opam processes OPAMSWITCH.

[Halbaroth]

A default value for LOCK_SWITCH is hardcoded in the Makefile. The trap is executed at exit with the environment of the script, so OPAMSWITCH contains the value of LOCK_SWITCH. For instance, this script

#!/usr/bin/env bash
set -e
trap cleanup EXIT

function cleanup() {
  echo "$FOO"
}

export FOO="Hello, bar!"

outputs Hello, bar! although the variable is set after the trap command.

I agree that it is too complicated. I modified the script to make it safer:

• I moved the default value of LOCK_SWITCH into the bash script. Users can still override it with LOCK_SWITCH=... make lock.
• The script checks if the switch already exists and fails if it does. No switch is automatically erase.
• The script fails on unset variables.
• I renamed LOCK_SWITCH to LOCKED_SWITCH.

[bclement-ocp]

A default value for LOCK_SWITCH is hardcoded in the Makefile.

I was more concerned with someone calling the script manually without going through the Makefile (I guess it's not supported but it still shouldn't have that kind of side effects)!

I like the new approach! Two remarks:

• It should be something like : "${LOCK_SWITCH:=alt-ergo-locked}" instead of export LOCK_SWITCH="alt-ergo-locked" to actually be a default value (but a hardcoded one is fine as well) ;
• If we fail when the switch already exists it might be a slightly better user experience to remove the one we have just created I'd say?

[Halbaroth]

Oups I forgot to translate the strange Makefile syntax to the strange Bash syntax...
In the last commit, the script cleans the switch after the check.

[bclement-ocp]

Obscure shell trick number 2137:

Suggested change

	export LOCKED_SWITCH="${LOCKED_SWITCH:=alt-ergo-locked}"
	: "${LOCKED_SWITCH:=alt-ergo-locked}"

: is a no-op command in sh/bash and this sets a variable to a default value without having to repeat the name of the variable – "${LOCKED_SWITCH:=alt-ergo-locked}" already updates the value of $LOCKED_SWITCH, that's what := does.

(duplicating the variable name is OK, just sharing the knowledge)

[Halbaroth]

Actually, I know this syntax and I no longer use it because it looks obscure. I can apply this change if you want.