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
|
; The easiest way to generate a portable absolute path is to use OCaml
; itself to print it
(executable
(name ocaml_pwd)
(modules ocaml_pwd))
(rule
(targets libpath.inc)
(action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted ../../install/%{context_name}/lib/coq/ ))))
(rule
(targets bin.inc)
(action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted -trailing-slash ../../install/%{context_name}/bin/ ))))
(rule
(targets summary.log)
(deps
; File that should be promoted.
misc/universes/all_stdlib.v
; Dependencies of the legacy makefile
../Makefile.common
../config/Makefile
; Stuff for the compat script test
../dev/header.ml
../dev/tools/update-compat.py
../doc/stdlib/index-list.html.template
; For the misc/printers.sh test
../dev/incdir_dune
../dev/base_include
../dev/inc_ltac_dune
../dev/include_printers
../dev/include
../dev/top_printers.ml
../dev/vm_printers.ml
; For the changelog test
../config/coq_config.py
(source_tree doc/changelog)
(package coq-core)
(package coq-stdlib)
; For fake_ide
(package coqide-server)
(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} BIN=%{read:bin.inc} COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))
|
