FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Bump OCaml version to 4.14 #3397

Closed gebner closed 2 months ago

gebner commented 2 months ago

I just tried installing F* on a new machine and opam installed --deps-only . failed with this error:

# [...]
# (cd _build/default && /home/gebner/.opam/default/bin/ocamlc.opt -w -40 -w -3-32-50-52 -g -bin-annot -I src/.batteries_unthreaded.objs/byte -I /home/gebner/.opam/default/lib/camlp-streams -I /home/gebner/.opam/default/lib/num -intf-suffix .ml -no-alias-deps -o src/.batteries_unthreaded.objs/byte/batGc.cmo -c -impl src/batGc.pp.ml)
# File "src/batGc.pp.ml", line 1:
# Error: The implementation src/batGc.pp.ml
#        does not match the interface src/.batteries_unthreaded.objs/byte/batGc.cmi:
#        The value `get_minor_free' is required but not provided
#        File "src/batGc.mli", line 278, characters 0-61: Expected declaration
# (cd _build/default && /home/gebner/.opam/default/bin/ocamlopt.opt -w -40 -w -3-32-50-52 -g -I src/.batteries_unthreaded.objs/byte -I src/.batteries_unthreaded.objs/native -I /home/gebner/.opam/default/lib/camlp-streams -I /home/gebner/.opam/default/lib/num -intf-suffix .ml -no-alias-deps -o src/.batteries_unthreaded.objs/native/batGc.cmx -c -impl src/batGc.pp.ml)
# File "src/batGc.pp.ml", line 1:
# Error: The implementation src/batGc.pp.ml
#        does not match the interface src/.batteries_unthreaded.objs/byte/batGc.cmi:
#        The value `get_minor_free' is required but not provided
#        File "src/batGc.mli", line 278, characters 0-61: Expected declaration

From what I can tell, recent versions of batteries no longer build with old OCaml versions. It seems easiest to just bump OCaml to the latest version, which this PR does.

This requires an update of the fstar_ci container image, so this PR fails CI for now.