blob: 640fceb836b5135a2b3466be3e7e461413ca896c (
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
142
143
144
145
146
|
#!/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)
OCAMLABI := $(shell ocamlc -version)
CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man \
--emacslib /usr/share/emacs/site-lisp/coq --reals all --fsets all \
--browser "/usr/bin/x-www-browser %s &" \
--with-doc no
configure: configure-stamp
configure-stamp: patch-stamp
dh_testdir
# git doesn't handle empty directories, so we create them here
-mkdir bin
if [ -e /usr/bin/ocamlc.opt ]; \
then \
./configure -opt $(CONFIGUREOPTS); \
else \
./configure $(CONFIGUREOPTS); \
fi
touch configure-stamp
build: build-stamp
build-stamp: configure-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
cp tools/coqdoc/coqdoc.sty doc/stdlib/
$(MAKE) -f Makefile.stage3 doc/stdlib/html/index.html COQDOC="bin/coqdoc --coqlib_path `pwd`"
touch build-stamp
clean: unpatch
dh_testdir
dh_testroot
rm -f build-stamp configure-stamp opt-stamp install-stamp
# Contains a directory ending in .d which breaks the clean rule
# of upstream Makefile
-rm -Rf debian/coq/etc
[ ! -f config/Makefile ] || $(MAKE) clean
[ ! -f config/Makefile ] || $(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
rm -f test-suite/modules/*.vo
rm -f doc/stdlib/coqdoc.sty
dh_clean
install: install-stamp
install-stamp: build-stamp
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
if [ -e opt-stamp ]; then \
cp man/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 man/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.1
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 -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
touch install-stamp
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 -- -VF:OCamlABI="$(OCAMLABI)"
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
|
