Something went wrong. Try again.
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031; Print Assumptions over the audited names, which is a claim about the; built theories rather than about any one file, so it hangs off an alias; and is never part of @default. The .vo files are named as deps so that; dune builds them first and reruns the audit when they change.
(rule (alias axioms) (deps check-axioms.sh (glob_files %{workspace_root}/theories/*.vo)) (action (setenv PAC_THEORIES %{workspace_root}/theories (run bash %{dep:check-axioms.sh}))))
; Sandboxed so that the script walks only the sources, not the build; artefacts dune leaves beside them.
(rule (alias runtest) (deps (glob_files %{workspace_root}/theories/*.v) (source_tree %{workspace_root}/lib) (source_tree %{workspace_root}/bin) (source_tree %{workspace_root}/eval) (source_tree %{workspace_root}/test) (sandbox always)) (action (run python3 %{dep:check-citations.py} %{workspace_root})))