blob: 3cfc0960e1d71dbefe9574463ff66d2bd7c543f0 (
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
|
# - set variable MLIFILES so that it can be used in custom targets to
# build documentation and dependencies for .mli files
# - remove useless ' -I . .../plugins/ ' lines so that we can read something in the compilation log
# - rename the rule for Makefile auto-regeneration, and replace it with an appropriate command
# - patch the rule for cleaning doc
# - include the .depend custom target, to take .mli dependencies into account
(
coq_makefile -no-install -opt MLIFILES = '$(MLFILES:.ml=.mli)' $(cat files.txt) -f magic.txt \
| sed 's|.*/plugins/.*||g;s|Makefile:|\.dummy:|g;s|rm -f doc|rm -rf doc|g'
cat <<EOF
# sanity checks
tests: Tests.vo
# override inadequate coq_makefile auto-regeneration
Makefile: make_makefile magic.txt files.txt
. make_makefile
# We want to keep the proofs only in the Tutorial
tutorial: Tutorial.vo Tutorial.glob
\$(COQDOC) --no-index --no-externals -html \$(COQDOCLIBS) -d html Tutorial.v
world: \$(VOFILES) doc gallinahtml tutorial
# additional dependencies for AAC (since aac_tactics.cmxs/cma are not
# around the first time we run make, coqdep issues a warning and
# ignores this dependency)
# (one can safely select one of theses dependencies according to
# coq' compilation mode--bytecode or native)
AAC.vo: aac_tactics.cmxs aac_tactics.cma
# .depend contains dependencies for .mli files
-include .depend
.SECONDARY: .depend
EOF
) > Makefile
# TOTHINK: coq_makefile est bête, [make all] compile systématiquement
# les .cmxs associés à chaque module, alors que ça ne sert à rien,
# seul aac_rewrite.cmxs compte
# problemes lorsqu'un module porte un meme nom qu'un module predefini
# (matching par exemple), prendre garde si ce probleme s'etend a la
# confusion module/nom de librairie
|
