blob: f22d2c4847a6e44b5bb21044152e37877c257b03 (
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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
|
#!/usr/bin/make -f
# debian/rules for coq
# Uncomment this to turn on verbose mode.
#export DH_VERBOSE=1
# This has to be exported to make some magic below work.
export DH_OPTIONS
# We want to use dpatch
include /usr/share/dpatch/dpatch.make
COQPREF := $(CURDIR)/debian/tmp
ADDPREF := COQINSTALLPREFIX=$(COQPREF)
CONFIGUREOPTS := --prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq --reals all --fsets all
configure: configure-stamp
configure-stamp:
dh_testdir
if [ -e /usr/bin/ocamlc.opt ]; \
then \
./configure -opt $(CONFIGUREOPTS); \
else \
./configure $(CONFIGUREOPTS); \
fi
touch configure-stamp
build: patch-stamp configure-stamp build-stamp
build-stamp:
dh_testdir
if grep -q BEST=opt config/Makefile; \
then \
($(MAKE) check \
&& touch opt-stamp) \
|| (echo WARNING: NATIVE CODE COMPILATION FAILED \
&& echo Trying to build coq in bytecode instead \
&& $(MAKE) archclean clean \
&& sed -i -e 's/best = "opt"/best = "byte"/' config/coq_config.ml \
&& $(MAKE) BEST=byte HASCOQIDE=byte check \
&& echo NATIVE CODE COMPILATION FAILED \
&& echo Coq was built in bytecode instead); \
else \
$(MAKE) BEST=byte HASCOQIDE=byte check; \
fi
if [ -e opt-stamp ]; then \
$(MAKE) BEST=opt glob.dump; \
else \
$(MAKE) BEST=byte HASCOQIDE=byte glob.dump; \
fi
cp tools/coqdoc/coqdoc.sty doc/stdlib/
$(MAKE) -C doc stdlib/html/index.html
touch build-stamp
clean: unpatch
dh_testdir
dh_testroot
rm -f build-stamp configure-stamp opt-stamp
-$(MAKE) clean
-$(MAKE) archclean
rm -f bin/*
rm -f tools/coqdoc/*.cm[oi]
rm -f config/coq_config.ml config/Makefile test-suite/check.log
rm -f dev/ocamldebug-v7
rm -f ide/undo.mli glob.dump
dh_clean
install: build
dh_testdir
dh_testroot
dh_clean -k
dh_installdirs
if [ -e opt-stamp ]; then \
$(MAKE) $(ADDPREF) install; \
else \
$(MAKE) BEST=byte HASCOQIDE=byte $(ADDPREF) install; \
fi
-for i in $(COQPREF)/usr/bin/*.opt; do \
echo "Stripping: $$i"; \
strip -R .note -R .comment $$i; \
done
if [ -e opt-stamp ]; then \
strip -R .note -R .comment $ $(COQPREF)/usr/bin/coqc; \
strip -R .note -R .comment $(COQPREF)/usr/bin/coqmktop; \
fi
cp debian/coq.xpm debian/coq/usr/share/pixmaps/coq.xpm
cp debian/coq.xpm debian/coqide/usr/share/pixmaps/coqide.xpm
cp debian/coqide.desktop debian/coqide/usr/share/applications
cp ide/index_urls.txt debian/coqide/usr/lib/coq/ide/index_urls.txt
if [ -e opt-stamp ]; then \
cp debian/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.opt.1; \
cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.opt.1; \
fi
cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.1
cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.byte.1
cp debian/coqc.1 debian/coq/usr/share/man/man1/coqc.1
cp debian/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.1
cp debian/coq_makefile.1 debian/coq/usr/share/man/man1/coq_makefile.1
cp debian/coqmktop.1 debian/coq/usr/share/man/man1/coqmktop.1
cp debian/coqtop.1 debian/coq/usr/share/man/man1/coqtop.1
cp -r doc/stdlib/html debian/coq-libs/usr/share/doc/coq-libs/
cd debian/coq-libs/usr/share/doc/coq; ln -s ../coq-libs/html stdlib
# These are installed as docs
rm -f $(COQPREF)/usr/lib/coq/ide/utf8.v $(COQPREF)/usr/lib/coq/ide/FAQ
dh_install --sourcedir=$(COQPREF) --list-missing
binary-common:
dh_testdir
dh_testroot
dh_installdocs
dh_installmenu
dh_installemacsen
dh_installman
dh_installchangelogs CHANGES
dh_installtex
dh_desktop
dh_link
dh_compress
dh_fixperms
dh_installdeb
dh_shlibdeps
dh_gencontrol
dh_md5sums
dh_builddeb
binary-indep: build install
$(MAKE) -f debian/rules DH_OPTIONS=-i binary-common
binary-arch: build install
$(MAKE) -f debian/rules DH_OPTIONS=-a binary-common
binary: binary-indep binary-arch
.PHONY: build clean binary-indep binary-arch binary-common binary install configure
|
