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
|
; The easiest way to generate a portable absolute path is to use OCaml
; itself to print it
(executable
(name ocaml_pwd)
(modules ocaml_pwd))
(env
(dev (flags :standard -w -70)))
(rule
(targets test_suite_config.inc)
(action (with-stdout-to %{targets} (run tools/coq_config_to_make.exe %{bin:coqc}))))
(rule
(targets summary.log)
(deps
; File that should be promoted.
misc/universes/all_stdlib.v
; Configure for test-suite
test_suite_config.inc
; when TIMED is set, used to print the timing table
../tools/make-one-time-file.py
../tools/TimeFileMaker.py
; For the changelog test
../config/coq_config.py
(source_tree doc/changelog)
(package rocq-runtime)
(package coq-core)
(package rocq-core)
(package coqide-server) ; For fake_ide
(package rocq-devtools) ; For bench-render
(source_tree .))
; Finer-grained dependencies would look like this and be generated
; by coqdep; that would allow tests to be run incrementally.
; ../tools/CoqMakefile.in
; ../theories/Init/Prelude.vo
; %{bin:coqc}
; %{bin:coq_makefile}
; %{bin:fake_ide}
(action
(progn
(bash "make -j %{env:NJOBS=2} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))
|
