blob: 1cef3d313990f2738f5dcec1045836fd832b871c (
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
|
#!/bin/sh
# - 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
# - added some hackish settings of Variables, in order to be able to install the plugin in user-contrib (coq_makefile should define a "INSTALL" variables that we can modify, instead of copying 4 times the same code in install !)
set -e
if [ -f `ocamlc -where`/dynlink.cmxa ]; then
BEST=opt
CMXA=aac_tactics.cmxa
CMXS=aac_tactics.cmxs
else
BEST=byte
if which ocamlopt >/dev/null; then
CMXA=aac_tactics.cmxa
fi
fi
(
coq_makefile -R . AAC_tactics -$BEST 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;s|\.opt||g'
cat <<EOF
# override inadequate coq_makefile auto-regeneration
Makefile: make_makefile magic.txt files.txt
./make_makefile
# We want to keep the proofs in Caveats and the Tutorial
world: \$(VOFILES) doc
- mkdir -p html
\$(COQDOC) -toc -utf8 -html -g \$(COQDOCLIBS) -d html \$(VFILES)
\$(COQDOC) --no-index --no-externals -s -utf8 -html \$(COQDOCLIBS) -d html Tutorial.v
\$(COQDOC) --no-index --no-externals -s -utf8 -html \$(COQDOCLIBS) -d html Caveats.v
# 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: $CMXA $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
|
