Ship fstar.lib as source in binary packages, and add fstar.exe --install_lib[_with_deps] to install it

[tahina-pro]

Motivation

F* binary packages (e.g. the nightly tarballs) bundle a standalone native
fstar.exe. Until now they also shipped the F* OCaml findlib packages
(fstar.compiler, fstar.pluginlib, and a compiled fstar.lib) that were
produced alongside that binary. Those compiled packages only work for a user
whose OCaml compiler and dependency versions exactly match the ones used to
build the package — which is essentially never true for the recipient of a
binary package. As a result, downstream consumers that need fstar.lib to
compile F*-extracted OCaml code (e.g. EverParse, and any project using
fstar.exe --ocamlopt/--ocamlenv) could not reliably build against a binary
package.

This PR makes binary packages ship fstar.lib as OCaml sources + a dune
project, and adds a new F* command-line mode, --install_lib
(and --install_lib_with_deps), that builds and installs that fstar.lib
into the user's own opam switch against their own toolchain. The end result is
a single, install-method-independent recipe for building OCaml apps against
F*:

fstar.exe --install_lib_with_deps      # build & install fstar.lib (+ its deps)
fstar.exe --ocamlopt ...               # compile extracted OCaml against it

This recipe is now uniform whether F* was obtained via a source build,
make install, opam install, or a binary package.

What changed

Packaging: binary packages ship fstar.lib as source

• Binary packages ship no precompiled OCaml packages. .scripts/bin-install.sh
  (run only on the binary-package path) strips compiler/, pluginlib/, META
  and dune-package from the package, and re-ships fstar.lib as OCaml sources
  plus a self-contained dune project (mk/fstar-lib-src/{dune,dune-project,README.md}).
  A regular make install / opam install fstar.opam is unaffected and keeps
  installing the compiled fstar.lib via dune install (the (public_name fstar.lib) stanzas in stage{1,2,3}/dune/libapp/dune are retained).
• Stripping META from the bundled lib dir also fixes findlib resolution of
  the user-built fstar.lib: --ocamlopt/--ocamlenv prepend <exec>/../lib
  to OCAMLPATH; with no META there, ocamlfind falls through to the user's
  switch (where --install_lib installed a proper fstar.lib) instead of being
  shadowed by the package's own stale META.
• make package (stage3) fix: stage3 reuses stage2's ulib extraction rather
  than re-extracting, so a new ULIB_ML variable (defaulting to
  $(BROOT)/ulib.ml, overridden to stage2/ulib.ml for package-3) encodes that
  invariant and avoids a cp: cannot stat '.../stage3/ulib.ml' failure.

New command: fstar.exe --install_lib

Builds and installs fstar.lib into the current OCaml/opam environment from the
shipped sources. Behaviour:

• If fstar.lib already resolves via findlib, it is a clean no-op
  ("already installed; nothing to do").
• If the findlib package fstar exists but fstar.lib does not, it errors out,
  rather than overwriting that package's META and dropping its other
  sub-packages.
• Otherwise it drives dune directly (dune build/dune install --root <lib_root>/lib, no shell, no --prefix so it installs into the active
  switch) to build and install fstar.lib.

Implementation notes:

• Detection uses the findlib library linked into fstar.exe
  (FStarC.Util.findlib_package_exists → Findlib.init/package_directory),
  not an ocamlfind subprocess, so it works on native (non-Cygwin) Windows.
  findlib is added to the fstar-guts dune (libraries ...) and to
  fstar.opam's and the nix derivation's dependencies.
• The install step likewise spawns dune directly (no bash install.sh), again
  for native-Windows support.
• The detection guard extends OCAMLPATH with the bundled lib dir
  (<exec>/../lib) exactly as --ocamlenv does, so it uniformly detects a
  compiled fstar.lib shipped next to fstar.exe (source build / make install) as well as one in the opam switch (opam install). This is why the
  command is a no-op for non-binary installs.

New command: fstar.exe --install_lib_with_deps

Same as --install_lib, but first installs fstar.lib's OCaml dependencies
(and ocamlfind itself) via opam install --deps-only on a fstar-lib.opam
shipped in the package. opam is driven directly (no shell) for native Windows.
fstar-lib.opam carries build: [ "false" ] so a direct opam install ./fstar-lib.opam fails on purpose — it is a dependency carrier, not an
installable package — while --deps-only (which skips the build step) still
installs the deps. The pre-flight findlib check is hardened to treat a missing
findlib.conf (which makes Findlib.init raise Failure) as "not resolvable",
so it proceeds to install findlib rather than crashing.

Tests / CI

• make test asserts --install_lib_with_deps is a no-op for a source
  build across test-1/2/3 (guards the bundled-lib detection / OCAMLPATH
  extension). It needs no OCaml toolchain since findlib is linked into
  fstar.exe.
• build-opam.yml: after opam install ., build the sample apps
  (tests/simple_hello, tests/dune_hello, tests/extraction) against the
  switch's fstar.lib.
• nightly-ci.yml: a new binary-install-lib job that, starting from only
  the binary package, runs --install_lib_with_deps to build+install
  fstar.lib from source into a fresh switch and builds the same sample apps
  against it — exercising the uniform app-build workflow end to end.

Documentation

• --help text for both options, and mk/fstar-lib-src/README.md, document the
  workflow and the ocamlfind/findlib/dune (and, for --install_lib_with_deps,
  opam) requirements — noting that --install_lib_with_deps installs
  ocamlfind/dune for you, whereas plain --install_lib assumes they are
  already present.

Files touched

 .github/workflows/build-opam.yml      # build sample apps against opam-installed fstar.lib
 .github/workflows/nightly-ci.yml      # binary-install-lib job (build fstar.lib from package)
 .nix/fstar.nix                        # declare findlib build dependency
 .scripts/bin-install.sh               # strip compiled OCaml pkgs; re-ship fstar.lib sources
 .scripts/install-fstar-lib-src.sh     # copy fstar.lib sources + dune project into package
 Makefile                              # ULIB_ML var; pass ulib.ml dir to bin-install.sh
 fstar.opam                            # depend on ocamlfind
 mk/fstar-lib-src/{README.md,dune,dune-project,fstar-lib.opam}  # shipped dune project + deps
 mk/stage.mk, stage3/Makefile          # source-shipping moved to binary-package path only
 src/basic/FStarC.Options.{fst,fsti}   # register --install_lib[_with_deps] + help
 src/basic/FStarC.Util.fsti, src/ml/FStarC_Util.ml  # findlib_package_exists
 src/fstar/FStarC.Main.fst             # dispatch the new terminal modes
 src/fstar/FStarC.OCaml.{fst,fsti}     # install_lib / install_lib_with_deps logic
 stage{1,2,3}/dune/fstar-guts/dune     # link findlib
 stage{1,2,3}/dune/libapp/dune         # keep (public_name fstar.lib) for make/opam install
 stage3/{Makefile,dune/...}            # ULIB_ML override; stage3-reuses-stage2 wiring

Compatibility

• make install and opam install fstar.opam are unchanged: they still install
  a compiled fstar.lib, and --install_lib[_with_deps] is a no-op there.
• Only the binary-package path changes shape (sources instead of compiled
  OCaml packages); the new commands rebuild fstar.lib from those sources.
• The new findlib dependency is statically linked into fstar.exe
  (buildInputs, not propagatedBuildInputs, in nix), needing no runtime
  stublibs.

[tahina-pro]

New nightly-ci tasks succeed (ocaml client tests with opam install and the binary package) : https://github.com/tahina-pro/FStar/actions/runs/26916542314

[gebner]

I am a bit torn on the --install_lib option. We typically don't (require F* packages to) modify the opam switch, so you can use the same switch for many F* builds.

Can we point dune to the fstar.lib ML source directory? (That is, 3dgen's dune file would build fstar.lib from source.)

[tahina-pro]

I have an EverParse PR into its fstar2 branch, project-everest/everparse#292, to build EverParse with a F* binary package. There, the fstarpkg.Dockerfile tests that feature, and it succeeds on my side with the binary package obtained from https://github.com/tahina-pro/FStar/actions/runs/26922219139

[tahina-pro]

Can we point dune to the fstar.lib ML source directory? (That is, 3dgen's dune file would build fstar.lib from source.)

Alas, I am not sure this solution works for cascading F* applications: if an user develops a F* application meant to be an ocaml package, and if another user develops an F* application that uses that ocaml package, fstar.lib will be compiled and linked twice, which may be a problem.

Another problematic scenario: what if an OCaml program depends on two libraries that both depend on fstar.lib.

[tahina-pro]

Gabriel:

I am a bit torn on the --install_lib option. We typically don't (require F* packages to) modify the opam switch, so you can use the same switch for many F* builds.

I acknowledge I am not sure about use cases for --install_lib.

However, for --install_lib_with_deps, which also installs dependencies in the user's switch, the main purpose of this option is to make the build of F* applications uniform, regardless of how the user installs F*:

• if they install F* with opam install fstar.opam, this step installs fstar.lib and its dependencies, and --install_lib_with_deps is a noop;
• if they build F* from sources, they will have installed the fstar.lib dependencies beforehand because F* also depends on them, and then the F* source build builds fstar.opam, so --install_lib_with_deps is a noop
• if they use a binary package, --install_lib_with_deps installs fstar.lib and its dependencies.

Notably, the process with --install_lib_with_deps is uniform in its treatment of dependencies of fstar.lib : especially, if a user uses F* with a binary package, they do not need to look into any detail about such dependencies.

In light of the problematic scenarios in my previous comment, a possible alternative to your proposal would be to make --install_lib build fstar.lib but not install it into the switch. This would ensure --install_lib does not change the user's switch, as you are proposing. But then, should --install_lib_with_deps behave in a hybrid way, by also building fstar.lib without installing it, while still installing its dependencies into the user's switch?

[gebner]

My proposal.

1. --ocamlenv is only used for plugins, and only works with local F* installations.

2. Applications that intend to be buildable with binary releases use a new --install_lib dest_dir option and manually set up OCAMLPATH to include that directory.

[tahina-pro]

Thanks Gabriel for your proposal!

1. --ocamlenv is only used for plugins, and only works with local F* installations.

By local F* installations, I presume you mean both F* built from source and F* installed with opam install fstar.opam, as opposed to F* binary packages. I consider opam to be a clean way to build F* plugins, since opam guarantees that the fstar.exe executable and the fstar.compilerlib and fstar.pluginlib libraries are always in sync. I hope we can keep this setup for F* plugins with your proposal. Is my understanding correct?

2. Applications that intend to be buildable with binary releases use a new --install_lib dest_dir option and manually set up OCAMLPATH to include that directory.

Here, you are proposing that applications must explicitly choose the place where to install fstar.lib, because we should not automatically install it into either the F* binary package (which you deem read-only) or the current user's opam switch (which you want to keep clean, except maybe for the fstar.lib dependencies), and that F* should not care about where fstar.lib is installed. Is my understanding correct?

Other than that, I presume the check on fstar.lib and fstar not already installed will stay. This is necessary to maintain uniformity in the opam install fstar.opam case. If so, then I buy your proposal, and it will be easy for me to adapt EverParse accordingly.

@mtzguido , @nikswamy, what do you think?