search

EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
318 stars 49 forks source link

EasyCrypt fails to build with Dune 3.7.0 + Merlin #350

Closed alleystoughton closed 1 year ago

alleystoughton commented 1 year ago

EC builds normally after the standard sequences of opam commands, including

opam pin alt-ergo 2.4.2

Interestingly, before installing alt-ergo we were at 5.0.0, but after we downgrade to 4.14.1. dune is at 3.7.0.

After

opam install merlin

EasyCrypt no longer builds

File "src/ecUtils.ml", line 633, characters 22-36:
633 |     if s == aout then BatString.copy aout else s
                            ^^^^^^^^^^^^^^
Error: Unbound value BatString.copy
make: *** [build] Error 1

and opam list shows (in particular the compiler is bumped back to 5.0.0):

alt-ergo              2.4.2       pinned to version 2.4.2
alt-ergo-lib          2.4.2       The Alt-Ergo SMT prover library
alt-ergo-parsers      2.4.2       The Alt-Ergo SMT prover parser library
base-bigarray         base
base-domains          base
base-nnp              base        Naked pointers prohibited in the OCaml heap
base-threads          base
base-unix             base
batteries             3.6.0       A community-maintained standard library extens
camlp-streams         5.0.1       The Stream and Genlex libraries for use with C
camlzip               1.11        Accessing compressed files in ZIP, GZIP and JA
cmdliner              1.1.1       Declarative definition of command line interfa
conf-autoconf         0.1         Virtual package relying on autoconf installati
conf-gmp              4           Virtual package relying on a GMP lib system in
conf-libpcre          1           Virtual package relying on a libpcre system in
conf-pkg-config       2           Check if pkg-config is installed and create an
conf-which            1           Virtual package relying on which
conf-zlib             1           Virtual package relying on zlib
cppo                  1.6.9       Code preprocessor like cpp for OCaml
csexp                 1.5.1       Parsing and printing of S-expressions in Canon
dot-merlin-reader     4.6         Reads config files for merlin
dune                  3.7.0       Fast, portable, and opinionated build system
dune-build-info       3.7.0       Embed build information inside executable
dune-configurator     3.7.0       Helper library for gathering system configurat
dune-private-libs     3.7.0       Private libraries of Dune
dune-site             3.7.0       Embed locations information inside executable 
dyn                   3.7.0       Dynamic type
menhir                20220210    An LR(1) parser generator
menhirLib             20220210    Runtime support library for parsers generated 
menhirSdk             20220210    Compile-time library for auxiliary tools relat
merlin                4.8-500     Editor helper, provides completion, typing and
merlin-lib            4.8-500     Merlin's libraries
num                   1.4         The legacy Num library for arbitrary-precision
ocaml                 5.0.0       The OCaml compiler (virtual package)
ocaml-base-compiler   5.0.0       Official release 5.0.0
ocaml-config          3           OCaml Switch Configuration
ocaml-inifiles        1.2         An ini file parser
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special 
ocamlbuild            0.14.2      OCamlbuild is a build system with builtin rule
ocamlfind             1.9.6       A library manager for OCaml
ocplib-simplex        0.4         A library implementing a simplex algorithm, in
ordering              3.7.0       Element ordering
pcre                  7.5.0       Bindings to the Perl Compatibility Regular Exp
pp                    1.1.2       Pretty-printing library
psmt2-frontend        0.4.0       The psmt2-frontend project
seq                   base        Compatibility package for OCaml's standard ite
stdlib-shims          0.3.0       Backport some of the new stdlib features to ol
stdune                3.7.0       Dune's unstable standard library
why3                  1.6.0       Why3 environment for deductive program verific
yojson                2.0.2       Yojson is an optimized parsing and printing li
zarith                1.12        Implements arithmetic and logical operations o
chdoc commented 1 year ago

Can you post the full list of operations that the opam install merlin triggers? (upgrades, downgrades, dependencies,...)

alleystoughton commented 1 year ago 
$ opam install merlin
The following actions will be performed:
  ↗ upgrade   ocaml-base-compiler 4.14.1 to 5.0.0 [required by ocaml]
  ↗ upgrade   ocaml-config        2 to 3          [required by ocaml]
  ↗ upgrade   ocaml               4.14.1 to 5.0.0 [required by merlin]
  ∗ install   base-domains        base
  ↻ recompile seq                 base            [uses ocaml]
  ↻ recompile ocamlfind           1.9.6           [uses ocaml]
  ↻ recompile ocamlbuild          0.14.2          [uses ocaml]
  ↻ recompile dune                3.7.0           [uses ocaml]
  ↻ recompile cmdliner            1.1.1           [uses ocaml]
  ∗ install   base-nnp            base
  ↻ recompile zarith              1.12            [uses ocaml]
  ↻ recompile num                 1.4             [uses ocaml]
  ↻ recompile camlzip             1.11            [uses ocaml]
  ↻ recompile stdlib-shims        0.3.0           [uses ocaml]
  ↻ recompile pp                  1.1.2           [uses ocaml]
  ↻ recompile ordering            3.7.0           [uses ocaml]
  ↻ recompile menhirSdk           20220210        [uses ocaml]
  ↻ recompile menhirLib           20220210        [uses ocaml]
  ↻ recompile dune-build-info     3.7.0           [uses ocaml]
  ↻ recompile csexp               1.5.1           [uses ocaml]
  ↻ recompile cppo                1.6.9           [uses ocaml]
  ↻ recompile camlp-streams       5.0.1           [uses ocaml]
  ↻ recompile ocplib-simplex      0.4             [uses ocaml]
  ↻ recompile dyn                 3.7.0           [uses ocaml]
  ↻ recompile menhir              20220210        [uses ocaml]
  ∗ install   merlin-lib          4.8-500         [required by merlin]
  ↻ recompile dune-configurator   3.7.0           [uses ocaml]
  ↻ recompile yojson              2.0.2           [uses ocaml]
  ↻ recompile batteries           3.6.0           [uses ocaml]
  ↻ recompile stdune              3.7.0           [uses ocaml]
  ↗ upgrade   why3                1.5.1 to 1.6.0  [uses ocaml]
  ↻ recompile psmt2-frontend      0.4.0           [uses ocaml]
  ∗ install   dot-merlin-reader   4.6             [required by merlin]
  ↻ recompile pcre                7.5.0           [uses ocaml]
  ↻ recompile alt-ergo-lib        2.4.2           [uses ocaml]
  ↻ recompile dune-private-libs   3.7.0           [uses ocaml]
  ∗ install   merlin              4.8-500
  ↻ recompile ocaml-inifiles      1.2             [uses ocaml]
  ↻ recompile alt-ergo-parsers    2.4.2           [uses ocaml]
  ↻ recompile dune-site           3.7.0           [uses dune]
  ↻ recompile alt-ergo            2.4.2*          [uses ocaml]
===== ∗ 5   ↻ 32   ↗ 4 =====
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫 
⬇ retrieved batteries.3.6.0  (cached)
⬇ retrieved alt-ergo-parsers.2.4.2  (cached)
⬇ retrieved camlp-streams.5.0.1  (cached)
⬇ retrieved camlzip.1.11  (cached)
⬇ retrieved cmdliner.1.1.1  (cached)
⬇ retrieved cppo.1.6.9  (cached)
⬇ retrieved csexp.1.5.1  (cached)
⬇ retrieved alt-ergo-lib.2.4.2  (cached)
⬇ retrieved dune.3.7.0  (cached)
⬇ retrieved dot-merlin-reader.4.6  (https://opam.ocaml.org/cache)
⬇ retrieved dune-build-info.3.7.0  (cached)
⬇ retrieved dune-private-libs.3.7.0  (cached)
⬇ retrieved dune-site.3.7.0  (cached)
⬇ retrieved dyn.3.7.0  (cached)
⬇ retrieved menhir.20220210  (cached)
⬇ retrieved menhirLib.20220210  (cached)
⬇ retrieved menhirSdk.20220210  (cached)
⬇ retrieved dune-configurator.3.7.0  (cached)
⬇ retrieved num.1.4  (cached)
⬇ retrieved merlin.4.8-500  (https://opam.ocaml.org/cache)
⬇ retrieved ocaml-base-compiler.5.0.0  (cached)
⬇ retrieved ocamlbuild.0.14.2  (cached)
⬇ retrieved ocaml-inifiles.1.2  (cached)
⬇ retrieved ocplib-simplex.0.4  (cached)
⬇ retrieved ocamlfind.1.9.6  (cached)
⬇ retrieved pcre.7.5.0  (cached)
⬇ retrieved pp.1.1.2  (cached)
⬇ retrieved psmt2-frontend.0.4.0  (cached)
⬇ retrieved stdlib-shims.0.3.0  (cached)
⬇ retrieved merlin-lib.4.8-500  (https://opam.ocaml.org/cache)
⬇ retrieved ordering.3.7.0  (cached)
⬇ retrieved stdune.3.7.0  (cached)
⬇ retrieved why3.1.6.0  (https://opam.ocaml.org/cache)
⬇ retrieved zarith.1.12  (cached)
⬇ retrieved yojson.2.0.2  (cached)
⊘ removed   alt-ergo.2.4.2
⊘ removed   alt-ergo-parsers.2.4.2
⊘ removed   alt-ergo-lib.2.4.2
⊘ removed   batteries.3.6.0
⊘ removed   camlp-streams.5.0.1
⊘ removed   cmdliner.1.1.1
⊘ removed   dune-build-info.3.7.0
⊘ removed   dune-site.3.7.0
⊘ removed   dune-private-libs.3.7.0
⊘ removed   ocaml-inifiles.1.2
⊘ removed   ocamlbuild.0.14.2
⊘ removed   ocplib-simplex.0.4
⊘ removed   pcre.7.5.0
⊘ removed   dune-configurator.3.7.0
⊘ removed   psmt2-frontend.0.4.0
⊘ removed   stdlib-shims.0.3.0
⊘ removed   stdune.3.7.0
⊘ removed   csexp.1.5.1
⊘ removed   dyn.3.7.0
⊘ removed   ordering.3.7.0
⊘ removed   pp.1.1.2
⊘ removed   why3.1.5.1
⊘ removed   camlzip.1.11
⊘ removed   menhir.20220210
⊘ removed   menhirLib.20220210
⊘ removed   menhirSdk.20220210
⊘ removed   num.1.4
⊘ removed   yojson.2.0.2
⊘ removed   cppo.1.6.9
⊘ removed   dune.3.7.0
⊘ removed   seq.base
⊘ removed   zarith.1.12
⊘ removed   ocamlfind.1.9.6
⊘ removed   ocaml.4.14.1
⊘ removed   ocaml-config.2
[NOTE] While removing ocaml-base-compiler.4.14.1: not removing non-empty
       directories:
         - share

⊘ removed   ocaml-base-compiler.4.14.1
∗ installed ocaml-base-compiler.5.0.0
∗ installed ocaml-config.3
∗ installed ocaml.5.0.0
∗ installed base-domains.base
∗ installed base-nnp.base
∗ installed seq.base
∗ installed cmdliner.1.1.1
∗ installed ocamlfind.1.9.6
∗ installed camlzip.1.11
∗ installed ocamlbuild.0.14.2
∗ installed num.1.4
∗ installed zarith.1.12
∗ installed ocplib-simplex.0.4
∗ installed dune.3.7.0
∗ installed menhirSdk.20220210
∗ installed menhirLib.20220210
∗ installed csexp.1.5.1
∗ installed ordering.3.7.0
∗ installed stdlib-shims.0.3.0
∗ installed pp.1.1.2
∗ installed dune-build-info.3.7.0
∗ installed cppo.1.6.9
∗ installed camlp-streams.5.0.1
∗ installed dyn.3.7.0
∗ installed yojson.2.0.2
∗ installed dune-configurator.3.7.0
∗ installed pcre.7.5.0
∗ installed ocaml-inifiles.1.2
∗ installed stdune.3.7.0
∗ installed alt-ergo-lib.2.4.2
∗ installed merlin-lib.4.8-500
∗ installed dot-merlin-reader.4.6
∗ installed dune-private-libs.3.7.0
∗ installed merlin.4.8-500
∗ installed menhir.20220210
∗ installed psmt2-frontend.0.4.0
∗ installed dune-site.3.7.0
∗ installed alt-ergo-parsers.2.4.2
∗ installed alt-ergo.2.4.2
∗ installed batteries.3.6.0
∗ installed why3.1.6.0
Done.

<><> merlin.4.8-500 installed successfully ><><><><><><><><><><><><><><><><>  🐫 
=> merlin installed.
fdupress commented 1 year ago

Note this also upgrades why3 to 1.6, which will also cause other compilation failures further down the line. We do have a hard cap on the why3 version in the dune-project, so there's something very iffy going on.

EDIT Oh, wait. I don't think there's anything iffy going on: you are setting up a switch for compiling EC from source, so the EC dependency constraints are not registered with opam. Perhaps there's a way of pinning all dependencies to a .opam?

chdoc commented 1 year ago

IMHO, the weird thing is that you use a switch in which the OCaml compiler is not pinned. If the compiler was pinned, this would (presumably) force opam to install the correct version of merlin for the current compiler rather than the correct compiler for the most current version of merlin.

alleystoughton commented 1 year ago

I do sometimes start out by creating a switch for a particular compiler. But our instructions don't tell us to do this. I'll see if that works, using 4.14.1.

alleystoughton commented 1 year ago

OK, if I pin the compiler to 4.14.1 and pin alt-ergo to 2.4.2 then there are no weird changes when I build merlin, and I do end up with dune 3.7.0 but EC builds fine. So I guess the instructions should tell folks to do this?

chdoc commented 1 year ago

Well, if ocaml-5.x leads to build errors, then EC should specify this in its opam file. Currently, running

$> opam install --deps-only easycrypt

will probably not downgrade ocaml (and hence merlin) to a compatible version (except maybe indirectly though constraints on packages like why3, which are already upper-bounded.

chdoc commented 1 year ago

OK, if I pin the compiler to 4.14.1 and pin alt-ergo to 2.4.2 then there are no weird changes when I build merlin, and I do end up with dune 3.7.0 but EC builds fine. So I guess the instructions should tell folks to do this?

The instructions could warn people that installing further packages may break the environment established by --deps-only, so this may need to be repeated is EC fails to build. But for this, the versions specified in opam file need to be specific enough.

fdupress commented 1 year ago

We clearly need to add an upper bound on the compiler version anyway, so let's do this. BUT we might also want to consider removing incompatibility with ocaml 5, since it's here. Let's discuss this tomorrow.