single file benchmarks

We add some dune rules to benchmark the compilation of single .v files.
It works by writing (theories/file/to/bench.v) in a file called
`file_to_bench` and running `dune build @bench`. This uses a program
called `hyperfine` which must be available for this to work. After the
bench is run it outputs a bench report.

Typical output:

```
[ali@allosaurus:~/HoTT]$ dune build @bench
Starting bench. This may take a while.
Bench finished, report at bench_report:

Benchmark 1: /nix/store/v97xkrdzqhwrz8305w05vfix32y5qifa-coq-8.19.1/bin/coqc -R ./theories HoTT -noinit -indices-matter benched_file.v
  Time (mean ± σ):      6.421 s ±  0.024 s    [User: 6.202 s, System: 0.195 s]
  Range (min … max):    6.364 s …  6.461 s    10 runs
```

Signed-off-by: Ali Caglayan <[email protected]>

<!-- ps-id: 9ddbc823-231a-471c-9eb2-ec07405c0998 -->

Author: Alizter

.gitignore

@@ -110,3 +110,6 @@ _CoqProject
 
 # ignore nix profiles
 nix/profiles/
+
+# Ignore the file to bench
+file_to_bench

dune

@@ -62,3 +62,48 @@
    (glob_files_rec contrib/*.v)))
  (action
   (run etc/emacs/run-etags.sh %{vfile})))
+
+; 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.")))