; 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})))