dune

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

; Common flags for Coq

(env
 (dev
  (coq
   (coqdoc_flags
    :standard
    --interpolate
    --utf8
    --no-externals
    --parse-comments)
   (flags -noinit -indices-matter -color on)))
 (_
  (coq
   (coqdoc_flags
    :standard
    --interpolate
    --utf8
    --no-externals
    --parse-comments)
   (flags -noinit -indices-matter))))

; Bench

; The following rule allows you to bench the running time of a file using
; "hyperfine". For this to work you must make a file called "file_to_bench"
; which contains the path to the file you want to bench (with brackets around
; it). For instance, if we wanted to bench the file
; "theories/WildCat/Products.v", we would make a file called "file_to_bench" with
; the following content:
;
; (theories/WildCat/Products.v)
;
; Afterwards you run "dune build @bench" and it will output the report.

(rule
 (alias bench)
 (deps
  (alias bench-hint)
  (universe)
  (sandbox always)
  (glob_files_rec ./*.vo)
  (:file
   (include file_to_bench)))
 (target bench_report)
 (action
  (progn
   (with-outputs-to
    %{target}
    (progn
     (copy %{file} benched_file.v)
     (run
      %{bin:hyperfine}
      "%{bin:coqc} -R %{project_root}/theories HoTT -noinit -indices-matter benched_file.v")))
   (echo "Bench finished, report at %{target}:\n\n")
   (cat %{target}))))

(rule
 (alias bench-hint)
 (deps
  (universe)
  (glob_files_rec ./*.vo)
  %{bin:hyperfine}
  (file file_to_bench))
 (action
  (run echo "Starting bench. This may take a while.")))