1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
; 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.")))
|
