building timing reports with dune

dune

@@ -129,3 +129,35 @@
   (file file_to_bench))
  (action
   (run echo "Starting bench. This may take a while.")))
+
+; Timing report
+
+(rule
+ (alias timing-html-hint)
+ (deps (universe) %{bin:lua})
+ (action
+  (run echo "Generating timing report. This may take a while.")))
+
+(rule
+ (alias timing-html)
+ (target
+  (dir timing-html))
+ (deps
+  (alias timing-html-hint)
+  etc/generate_coqproject.sh
+  etc/time2html
+  Makefile
+  Makefile.coq.local
+  Makefile.coq.local-early
+  (sandbox always)
+  (sandbox preserve_file_kind)
+  (glob_files_rec ./theories/*.v)
+  (glob_files_rec ./contrib/*.v)
+  (glob_files_rec ./test/*.v))
+ (action
+  (setenv
+   GENERATE_COQPROJECT_FOR_DUNE
+   true
+   (progn
+    (ignore-outputs
+     (run %{bin:make} timing-html))))))

dune-project

@@ -6,6 +6,8 @@
 
 (generate_opam_files true)
 
+(using directory-targets 0.1)
+
 (source
  (github HoTT/HoTT))
 

etc/generate_coqproject.sh

@@ -37,9 +37,9 @@ COQPROJECT_HEADER=\
 if [ "$GENERATE_COQPROJECT_FOR_DUNE" == "true" ]; then
   COQPROJECT_HEADER="$COQPROJECT_HEADER
 # Dune compatibility
--R _build/default/theories HoTT
--Q _build/default/contrib HoTT.Contrib
--Q _build/default/test HoTT.Tests
+-R $PWD/theories HoTT
+-Q $PWD/contrib HoTT.Contrib
+-Q $PWD/test HoTT.Tests
 "
 fi