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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 29 Nov 2010 23:52:39 +0100
Subject: [PATCH] Fix Makefile generation
* add "#!" header to make_makefile
* add "-R . AACTactics" option to coq_makefile, and adapt theory.ml
* add custom rule for aac_tactics.cmxa
* fix Makefile rule
* fix build on bytecode/non-natdynlink architectures
* workaround Coq bug #2444
Signed-off-by: Stephane Glondu <steph@glondu.net>
---
magic.txt | 1 +
make_makefile | 22 ++++++++++++++++++----
theory.ml | 2 +-
3 files changed, 20 insertions(+), 5 deletions(-)
diff --git a/magic.txt b/magic.txt
index d0272c3..1b17df7 100644
--- a/magic.txt
+++ b/magic.txt
@@ -1,4 +1,5 @@
-custom "mkdir -p doc; $(CAMLBIN)ocamldoc -html -rectypes -d doc -m A $(ZDEBUG) $(ZFLAGS) $^ && touch doc" "$(MLIFILES)" doc
-custom "$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -linkall -o aac_tactics.cmxs $(CMXFILES)" "$(CMXFILES)" aac_tactics.cmxs
-custom "$(CAMLLINK) -g -a -o aac_tactics.cma $(CMOFILES)" "$(CMOFILES)" aac_tactics.cma
+-custom "$(CAMLOPTLINK) -g -a -o aac_tactics.cmxa $(CMXFILES)" "$(CMXFILES)" aac_tactics.cmxa
-custom "$(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $^ > .depend" "$(MLIFILES)" .depend
diff --git a/make_makefile b/make_makefile
index 3cfc096..44b47f1 100755
--- a/make_makefile
+++ b/make_makefile
@@ -1,3 +1,4 @@
+#!/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
@@ -5,9 +6,22 @@
# - patch the rule for cleaning doc
# - include the .depend custom target, to take .mli dependencies into account
+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 -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'
+coq_makefile -R . AACTactics -no-install -$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
# sanity checks
@@ -15,7 +29,7 @@ tests: Tests.vo
# override inadequate coq_makefile auto-regeneration
Makefile: make_makefile magic.txt files.txt
- . make_makefile
+ ./make_makefile
# We want to keep the proofs only in the Tutorial
tutorial: Tutorial.vo Tutorial.glob
@@ -28,7 +42,7 @@ world: \$(VOFILES) doc gallinahtml tutorial
# 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
+AAC.vo: $CMXA $CMXS aac_tactics.cma
# .depend contains dependencies for .mli files
diff --git a/theory.ml b/theory.ml
index 45a76f1..f2041da 100644
--- a/theory.ml
+++ b/theory.ml
@@ -16,7 +16,7 @@
open Term
-let ac_theory_path = ["AAC"]
+let ac_theory_path = ["AACTactics"; "AAC"]
module Sigma = struct
let sigma = lazy (Coq.init_constant ac_theory_path "sigma")
--
|
