blob: c5fa0bb14a591c2e6188dc973b0c7e38246e73e5 (
plain)
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
|
(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
(package coq)
; For fake_ide
(package coqide-server)
(source_tree .))
; Finer-grained dependencies look like this
; ../tools/CoqMakefile.in
; ../theories/Init/Prelude.vo
; ../theories/Arith/Arith.vo
; ../theories/Arith/Compare.vo
; ../theories/PArith/PArith.vo
; ../theories/QArith/QArith.vo
; ../theories/QArith/Qcanon.vo
; ../theories/ZArith/ZArith.vo
; ../theories/ZArith/Zwf.vo
; ../theories/Sets/Ensembles.vo
; ../theories/Numbers/Natural/Peano/NPeano.vo
; ../theories/Numbers/Cyclic/Int31/Cyclic31.vo
; ../theories/FSets/FMaps.vo
; ../theories/FSets/FSets.vo
; ../theories/MSets/MSets.vo
; ../theories/Compat/Coq87.vo
; ../theories/Compat/Coq88.vo
; ../theories/Relations/Relations.vo
; ../theories/Unicode/Utf8.vo
; ../theories/Program/Program.vo
; ../theories/Classes/EquivDec.vo
; ../theories/Classes/DecidableClass.vo
; ../theories/Classes/SetoidClass.vo
; ../theories/Classes/RelationClasses.vo
; ../theories/Logic/Classical.vo
; ../theories/Logic/Hurkens.vo
; ../theories/Logic/ClassicalFacts.vo
; ../theories/Reals/Reals.vo
; ../theories/Lists/Streams.vo
; ../plugins/micromega/Lia.vo
; ../plugins/micromega/Lqa.vo
; ../plugins/micromega/Psatz.vo
; ../plugins/micromega/MExtraction.vo
; ../plugins/nsatz/Nsatz.vo
; ../plugins/omega/Omega.vo
; ../plugins/ssr/ssrbool.vo
; ../plugins/derive/Derive.vo
; ../plugins/funind/Recdef.vo
; ../plugins/extraction/Extraction.vo
; ../plugins/extraction/ExtrOcamlNatInt.vo
; coqtop
; coqtop.opt
; coqidetop.opt
; coqqueryworker.opt
; coqtacticworker.opt
; coqproofworker.opt
; coqc
; coqchk
; coqdoc
; %{bin:coq_makefile}
; %{bin:fake_ide}
(action
(progn
; XXX: we will allow to set the NJOBS variable in a future Dune
; version, either by using an env var or by letting Dune set `-j`
(run make -j 2 BIN= PRINT_LOGS=1))))
|
