fstar.2025.12.15

[mtzguido]

Just a new F* release. For this release, we are switching the source tarball to be a "source package" containing the OCaml-extracted sources of F*, avoiding the need to bootstrap the compiler when installing via OPAM.

[jmid]

Thanks!

There's a dune lower bound that needs adjusting.

On 5.4 workflows I see
https://opam.ci.ocaml.org/github/ocaml/opam-repository/commit/749b51f6618d0d7a7f48b66e781d6ecf017bc24a/variant/compilers,5.4,fstar.2025.12.15

#=== ERROR while compiling fstar.2025.12.15 ===================================#
# context              2.5.0 | linux/x86_64 | ocaml-base-compiler.5.4.0 | pinned(https://github.com/FStarLang/FStar/releases/download/v2025.12.15/fstar-v2025.12.15-src.tar.gz)
# path                 ~/.opam/5.4/.opam-switch/build/fstar.2025.12.15
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j 71 ADMIT=1
# exit-code            2
# env-file             ~/.opam/log/fstar-7-c5d6a8.env
# output-file          ~/.opam/log/fstar-7-c5d6a8.out
### output ###
#    DUNE BUILD      
#    INSTALL LIB SRC  
# (cd _build/.sandbox/4aeafa9c2bf1296a1addfb86cfd16bf3/default && /home/opam/.opam/5.4/bin/menhir fstar-guts/FStarC_Parser_Parse.mly --base fstar-guts/FStarC_Parser_Parse --infer-write-query fstar-guts/FStarC_Parser_Parse__mock.ml.mock)
# File "fstar-guts/FStarC_Parser_Parse.mly", line 129, characters 60-70:
# Warning: the token LBRACK_BAR is unused.
# File "fstar-guts/FStarC_Parser_Parse.mly", line 323, characters 0-15:
# Warning: symbol decoratableDecl is unreachable from any of the start symbol(s).
# File "fstar-guts/FStarC_Parser_Parse.mly", line 306, characters 0-16:
# Warning: symbol noDecorationDecl is unreachable from any of the start symbol(s).
# (cd _build/default && /home/opam/.opam/5.4/bin/ocamlc.opt -w @[email protected]@31..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -w -A -g -I fstar-guts/.fstarcompiler.objs/byte -I /home/opam/.opam/5.4/lib/batteries -I /home/opam/.opam/5.4/lib/batteries/unthreaded -I /home/opam/.opam/5.4/lib/camlp-streams -I /home/opam/.opam/5.4/lib/gen -I /home/opam/.opam/5.4/lib/menhirLib -I /home/opam/.opam/5.4/lib/mtime -I /home/opam/.opam/5.4/lib/mtime/clock -I /home/opam/.opam/5.4/lib/num -I /home/opam/.opam/5.4/lib/ocaml-compiler-libs/common -I /home/opam/.opam/5.4/lib/ocaml-compiler-libs/shadow -I /home/opam/.opam/5.4/lib/ocaml/compiler-libs -I /home/opam/.opam/5.4/lib/ocaml/dynlink -I /home/opam/.opam/5.4/lib/ocaml/str -I /home/opam/.opam/5.4/lib/ocaml/threads -I /home/opam/.opam/5.4/lib/ocaml/unix -I /home/opam/.opam/5.4/lib/pprint -I /home/opam/.opam/5.4/lib/ppx_derivers -I /home/opam/.opam/5.4/lib/ppx_deriving/runtime -I /home/opam/.opam/5.4/lib/ppx_deriving_yojson/runtime -I /home/opam/.opam/5.4/lib/ppxlib -I /home/opam/.opam/5.4/lib/ppxlib/ast -I /home/opam/.opam/5.4/lib/ppxlib/astlib -I /home/opam/.opam/5.4/lib/ppxlib/print_diff -I /home/opam/.opam/5.4/lib/ppxlib/stdppx -I /home/opam/.opam/5.4/lib/ppxlib/traverse_builtins -I /home/opam/.opam/5.4/lib/process -I /home/opam/.opam/5.4/lib/sedlex -I /home/opam/.opam/5.4/lib/seq -I /home/opam/.opam/5.4/lib/sexplib0 -I /home/opam/.opam/5.4/lib/stdint -I /home/opam/.opam/5.4/lib/stdlib-shims -I /home/opam/.opam/5.4/lib/yojson -I /home/opam/.opam/5.4/lib/zarith -no-alias-deps -opaque -open Fstarcompiler -o fstar-guts/.fstarcompiler.objs/byte/fstarcompiler__FStarC_Extraction_ML_PrintML.cmo -c -impl fstar-guts/ml/FStarC_Extraction_ML_PrintML.pp.ml)
# File "fstar-guts/ml/FStarC_Extraction_ML_PrintML.ml", line 80, characters 23-41:
# 80 |          | [] ->  Ldot(Lident path_abbrev, sym) |> mk_sym_lident
#                             ^^^^^^^^^^^^^^^^^^
# Error: This expression should not be a constructor, the expected type is
#        Longident.t with_loc
# (cd _build/.sandbox/10793fc7477cad35d11cfe3e6c544878/default && /home/opam/.opam/5.4/bin/menhir fstar-guts/FStarC_Parser_Parse.mly --base fstar-guts/FStarC_Parser_Parse --infer-read-reply fstar-guts/FStarC_Parser_Parse__mock.mli.inferred)
# Warning: 20 states have shift/reduce conflicts.
# Warning: 302 shift/reduce conflicts were arbitrarily resolved.
# Warning: 226 end-of-stream conflicts were arbitrarily resolved.
# make: *** [Makefile:34: build] Error 1

which would be good to address. It is likely caused by 5.4 AST changes.