nanofil/web/rocq/capture.nix

Cache prover execution independently of the presentation assets.

λpkgs

let

4src=

pkgs.lib.fileset.toSource

5root=

../../..

6fileset=

pkgs.runCommand"dterm-rocq-proof-states" nativeBuildInputs = pkgs.coq pkgs.coqPackages.stdlib pkgs.swi-prolog pkgs.python3;

python3 ${src}/nanofil/tests/watch.py --label "Proof capture regression" -- \

python3 ${src}/nanofil/web/rocq/tests/capture.py

mkdir -p project/extraction

cp -r ${src}/nanofil/rocq/. project/

chmod -R u+w project

python3 ${src}/nanofil/tests/watch.py --label "Rocq proof-state capture" -- \

python3 ${src}/nanofil/web/rocq/capture.py project $out