Skip to content

Nix: Improve build reproducibility and fix OCaml library loading#4105

Open
remix7531 wants to merge 7 commits intoFStarLang:masterfrom
remix7531:nix-fixes
Open

Nix: Improve build reproducibility and fix OCaml library loading#4105
remix7531 wants to merge 7 commits intoFStarLang:masterfrom
remix7531:nix-fixes

Conversation

@remix7531
Copy link
Contributor

This PR improves the Nix flake for F* with proper OCaml library path handling, better formatting, and an isolated CI testing target.

Changes

Commit 1: Add CAML_LD_LIBRARY_PATH and fix diff sh call

  • Automatically discover and set CAML_LD_LIBRARY_PATH for OCaml shared libraries in devShell
  • Add num to propagatedBuildInputs (required for runtime library loading)
  • Fix diff.sh path in test.mk

Commit 2: Sort dependency lists and format

  • Alphabetically sort dependency lists for maintainability
  • Format code consistently

Commit 3: Add isolated CI build target and fix sandbox issues

  • New fstar-ci-nofsharp package for reproducible testing in pure Nix sandbox
  • Add python3, which, util-linux to build dependencies (required by tests)
  • Set DUNE_CACHE=disabled to avoid permission errors in sandboxed builds
  • Export CAML_LD_LIBRARY_PATH with auto-discovered OCaml shared library paths
  • Excludes F# support (requires EOL .NET 6, incompatible with nixpkgs .NET 8)
  • Runs: make 2, test, stage3-diff, test-2-bare, stage2-unit-tests

Testing

Test the isolated CI build with:

nix build .#fstar-ci-nofsharp --option sandbox true --option pure-eval true -L

@remix7531
Copy link
Contributor Author

Working on PR 4080, I encountered some issues with the Nix environment:

  1. The flake was not completely sandboxed/independent from the host system
  2. Shared libraries from the num package were not correctly exposed via CAML_LD_LIBRARY_PATH

This draft PR addresses these issues and adds a fstar-ci-nofsharp target for isolated CI testing in a pure sandbox.

@gebner @Nadrieril What do you think of the current approach? A few questions:

  • Should we use checkPhase instead of a separate CI package target?
  • Should we bump the F# dependency to .NET 8 (requires updating global.json)? The current .NET 6 requirement is EOL.

I'd like to hear your thoughts before restructuring the commits and finalizing this PR.

@remix7531
Copy link
Contributor Author

I will undo the formatting.

@Nadrieril
Copy link
Contributor

Overall looks pretty good to me! I don't mind the formatting commit, I too have autoformat enabled ^^ Can't comment on the F# version, I know nothing about that; the nix looks good if we can avoid the IFD.

Create ocamlLibraryPath using symlinkJoin to avoid IFD and export it
in the dev shell for OCaml shared libraries access.

Addresses review feedback from @Nadrieril.
- Expand sourceByRegex to include test directories
- Pass ocamlLibraryPath for checkPhase
- Add check build with tests enabled
@remix7531 remix7531 marked this pull request as ready for review February 16, 2026 17:01
@remix7531 remix7531 requested a review from Nadrieril February 16, 2026 17:01
Copy link
Contributor

@Nadrieril Nadrieril left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Much better, LGTM now! I don't have merge rights fyi

@remix7531
Copy link
Contributor Author

@gebner Requesting additional review on this PR. I do not have permission to request reviewers directly. Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants