; Rule for generating coq_project
; This uses (mode promote) in order to put _CoqProject in the source tree.
; This isn't actually needed for dune but is useful when working with editors.

(rule
 (target _CoqProject)
 (deps
  ./etc/generate_coqproject.sh
  (source_tree theories)
  (source_tree contrib)
  (source_tree test))
 (mode promote)
 (package coq-hott)
 (action
  (setenv
   GENERATE_COQPROJECT_FOR_DUNE
   true
   (bash ./etc/generate_coqproject.sh))))

; Rule for validation: dune build @runtest
; This will also run the tests

(rule
 (alias runtest)
 (deps
  (glob_files_rec ./*.vo))
 (action
  (run
   coqchk
   -R
   ./theories
   HoTT
   -Q
   contrib
   HoTT.Contrib
   -Q
   test
   HoTT.Tests
   %{deps}
   -o)))

; We modify the default alias to avoid test/

(alias
 (name default)
 (deps
  (alias_rec contrib/all)
  (alias_rec theories/all)
  _CoqProject))

; Tags for emacs

(rule
 (target TAGS)
 (alias emacs)
 (mode promote)
 (deps
  etc/emacs/run-etags.sh
  %{bin:etags}
  (:vfile
   (glob_files_rec theories/*.v)
   (glob_files_rec contrib/*.v)))
 (action
  (run etc/emacs/run-etags.sh %{vfile})))