nanofil/nix/crane.nix
Crane (https://github.com/bloomberg/crane), Bloomberg's extraction of Rocq to C++, for the Gallina backend (rocq/backend/crane, docs/gallina-backend.md, M6). Pinned to one commit and patched (crane-nanofil.patch, whose parts the doc lists): Crane's own tree builds against Rocq 9.0, the backend against 9.1.
Only the plugin and the four theory files the backend's extraction imports are built. $out/lib/coq/9.1/user-contrib/Crane goes on ROCQPATH and $out/lib/ocaml/site-lib on OCAMLPATH; the headers the extracted C++ includes are in $out/include.
λpkgs
let
in
pkgs.stdenv.mkDerivation
coq.coq ocamlPackages.ocaml ocamlPackages.findlib ocamlPackages.dune_3
The theory's dune stanza names ITree, ExtLib and Paco, for files that are not built here.
substituteInPlace theories/dune \
--replace-fail "(theories Stdlib ITree ExtLib Paco)" "(theories Stdlib)"
runHook preBuild
dune build -j "$NIX_BUILD_CORES" src \
theories/Extraction.vo theories/Mapping/Shared.vo theories/Mapping/Std.vo \
theories/Mapping/NatIntStd.vo theories/Mapping/AsciiChar.vo
runHook postBuild
runHook preInstall
mkdir -p $out/lib/ocaml/site-lib $out/lib/coq/9.1/user-contrib/Crane $out/include
cp -rL _build/install/default/lib/rocq-crane $out/lib/ocaml/site-lib/
(cd _build/default/theories && find . -name '*.vo' -exec cp --parents {} $out/lib/coq/9.1/user-contrib/Crane/ \;)
cp theories/cpp/*.h $out/include/
runHook postInstall
inherit coq ocamlPackages;