fstar: build with dune

[pnmadelaine]

Description of changes

Build F* with Dune, reflecting changes to the F* build process from a few months ago.
This splits the build into three derivations, one for the F* binary, one for the library and one for the complete package.

Should fix #275866

cc @W95Psp who helped rework the F* flake, does this look good to you?

Things done

• Built on platform(s)
  • x86_64-linux
  • aarch64-linux
  • x86_64-darwin
  • aarch64-darwin
• For non-Linux: Is sandboxing enabled in nix.conf? (See Nix manual)
  • sandbox = relaxed
  • sandbox = true
• Tested, as applicable:
  • NixOS test(s) (look inside nixos/tests)
  • and/or package tests
  • or, for functions and "core" functionality, tests in lib/tests or pkgs/test
  • made sure NixOS tests are linked to the relevant packages
• Tested compilation of all packages that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review rev HEAD". Note: all changes have to be committed, also see nixpkgs-review usage
• Tested basic functionality of all binary files (usually in ./result/bin/)
• 24.05 Release Notes (or backporting 23.05 and 23.11 Release notes)
  • (Package updates) Added a release notes entry if the change is major or breaking
  • (Module updates) Added a release notes entry if the change is significant
  • (Module addition) Added a release notes entry if adding a new NixOS module
• Fits CONTRIBUTING.md.

---

Add a 👍 reaction to pull requests you find important.

[someplaceguy]

@pnmadelaine Thanks for fixing this!

I've just tried this PR and F* builds correctly for me and seems to work fine.

However, I am running into one issue. I have a tiny F* program which gets extracted to OCaml and builds fine when using PR #275889 but fails to build with this PR unless I apply the following patch to my program's default.nix:

diff --git a/default.nix b/default.nix
index 7a8e9c7..49b7c49 100644
--- a/default.nix
+++ b/default.nix
@@ -25,6 +25,18 @@ stdenv.mkDerivation {

   nativeBuildInputs = with ocamlPackages; [ findlib fstar ocaml ocamlbuild tup z3_4_8_5 ];

+  buildInputs = with ocamlPackages; [
+    batteries
+    menhirLib
+    pprint
+    process
+    ppx_deriving
+    ppx_deriving_yojson
+    sedlex
+    stdint
+    zarith
+  ];
+
   installPhase = ''
     mkdir -p $out/bin

The issue is that fstar.lib requires those libraries (but my program doesn't, or at least, not directly).

This is normally fixed by moving these libraries in the fstarDune derivation from buildInputs to propagatedBuildInputs so that downstream derivations don't have to declare these dependencies manually.

However, since in this case the fstarDune derivation is not the actual derivation that gets exported to all-packages.nix, it might be slightly more awkward. I think it would require not only moving those libraries to propagatedBuildInputs in fstarDune, but it would also require adding fstarDune to the buildInputs of the main fstar derivation as well, I think...

[pnmadelaine]

@someplaceguy thanks for testing this!
I don't think adding fstarDune as a propagated build input is a good idea, since it would expose two F* binaries.
Instead I propagated fstarDune.buildInputs directly.
It does not feel too awkard to me, what do you think?

[pnmadelaine]

Just noticed some things in fstarDune.buildInputs are not necessary to propagate.
I am just going to do the same split you did in your PR if that's okay!

[someplaceguy]

It does not feel too awkard to me, what do you think?

I agree it's not too awkward. I just tried your latest changes (including the don't propagate everything commit) and it seems to work perfectly.

Many thanks! 🎉