-
Notifications
You must be signed in to change notification settings - Fork 88
/
Makefile
309 lines (259 loc) · 10.2 KB
/
Makefile
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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
##
## Makefile for Proof General.
##
## Author: David Aspinall <[email protected]>
##
## make - do "compile" targets
## make compile - make .elc's
## make check - compile with warning flags enabled
## make scripts - edit paths to bash/perl/PGHOME in scripts
## make install - install into system directories
## make clean - return to clean source
## make tests - run the suite of regression tests
##
## Edit the EMACS setting below or call with an explicit one, like this:
##
## make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs
##
## $Id$
##
###########################################################################
# Set this according to your version of Emacs.
# NB: this is also used to set default install path names below.
EMACS=$(shell if [ -z "`which emacs`" ]; then echo "Emacs executable not found"; exit 1; else echo emacs; fi)
# We default to /usr rather than /usr/local because installs of
# desktop and doc files under /usr/local are unlikely to work with
# rest of the system. If that's no good for you, edit the paths
# individually before the install section.
# NB: DEST_PREFIX is used for final destination prefix, in case we're
# packaging into a build prefix rather than live root (e.g. in rpmbuild).
# NBB: DESTDIR provides for staged installs, for instance when building
# Debian packages, see http://www.gnu.org/prep/standards/html_node/DESTDIR.html
PREFIX=$(DESTDIR)/usr
DEST_PREFIX=$(DESTDIR)/usr
# subdirectories for provers: to be compiled and installed
PROVERS=coq easycrypt pghaskell pgocaml pgshell phox qrhl
# generic lisp code: to be compiled and installed
OTHER_ELISP=generic lib
# additional lisp code: to be compiled but not installed
ADDITIONAL_ELISP:=ci/compile-tests \
$(wildcard ci/compile-tests/[0-9][0-9][0-9]-*) \
ci/simple-tests
# directories with lisp code to be installed
ELISP_DIRS_INST=${PROVERS} ${OTHER_ELISP}
# directories with lisp code to be compiled (superset of ELISP_DIRS_INST
ELISP_DIRS_COMP=${ELISP_DIRS_INST} ${ADDITIONAL_ELISP}
# to be installed
ELISP_EXTRAS=
# to be installed
EXTRA_DIRS = images
DOC_FILES=AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README.md doc/*.pdf
DOC_EXAMPLES=pgshell/*.pgsh phox/*.phx
DOC_SUBDIRS=${DOC_EXAMPLES} */README* */CHANGES */BUGS
BATCHEMACS=${EMACS} --batch --no-site-file -q
# Scripts to edit paths to shells
PERL_SCRIPTS = coq/coqtags
# Scripts to install to bin directory
BIN_SCRIPTS = coq/coqtags
# Setting load path might be better in Elisp, but seems tricky to do
# only during compilation. Another idea: put a function in proof-site
# to output the compile-time load path and ELISP_DIRS_COMP so these are set
# just in that one place.
ERROR_ON_WARN = nil
BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. ${ELISP_DIRS_COMP}))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn $(ERROR_ON_WARN)))' -f batch-byte-compile
EL=$(shell for f in $(ELISP_DIRS_COMP); do ls $$f/*.el; done)
ELC=$(EL:.el=.elc)
.SUFFIXES: .el .elc
default: all
FORCE:
##
## compile : byte compile all lisp files
##
## Compiling can show up errors in the code, but be wary of fixing obsoletion
## or argument call warnings unless they're valid for all supported Emacsen.
##
## The compile target displays errors as warnings only for compatibility
## with newer Emacs versions (see ticket #458).
##
compile: $(EL)
@echo "****************************************************************"
@echo " Byte compiling... "
@echo "****************************************************************"
$(MAKE) elc
@echo "****************************************************************"
@echo " Finished."
@echo "****************************************************************"
##
## check : make sure compilation doesn't emit warnings
##
## The check target aborts compilation on any byte-compiler warning.
## Compile with this target once before commiting your changes to
## the repository.
## FIXME: Compilation currently emits many warnings :-(
##
check: $(EL)
@echo "****************************************************************"
@echo " Byte compiling... "
@echo "****************************************************************"
$(MAKE) ERROR_ON_WARN=t elc
@echo "****************************************************************"
@echo " Finished."
@echo "****************************************************************"
##
## tests : run a selection of regression tests
##
.PHONY: tests
tests:
ci/test.sh
##
## dist-tests : run all regression tests
##
.PHONY: dist-tests
dist-tests: tests check-doc-magic
+$(MAKE) -C ci/simple-tests all
+$(MAKE) -C ci/compile-tests test
+$(MAKE) -C ci/test-indent
##
## check-doc-magic : check *.texi are up-to-date w.r.t. docstrings
##
.PHONY: check-doc-magic
check-doc-magic:
+$(MAKE) -C doc magic
git diff --exit-code -- doc
##
## Make an individual .elc. Building separately means we need to be
## careful to add proper requires in source files and prevent
## evaluating/optimising top-level forms too early. Using a separate
## emacs process for each file is slower but avoids any chance of
## accidently polluting the compilation environment, it also should
## work with make -j n.
##
.el.elc:
$(BYTECOMP) $*.el
elc: $(ELC)
##
## Default targets
##
all: compile
##
## Remove generated targets
##
clean: cleanscripts
rm -f $(ELC) .\#* */.\#* */.autotest.log */.profile.log
(cd doc; $(MAKE) clean)
distclean: clean
##
## Install files
##
DESKTOP_PREFIX=${PREFIX}
# Set Elisp directories according to paths used in Red Hat RPMs
# (which may or may not be official Emacs policy). We generate
# a pg-init.el file which loads the appropriate proof-site.el.
ELISPP=share/${EMACS}/site-lisp/ProofGeneral
ELISP_START=${PREFIX}/share/${EMACS}/site-lisp/site-start.d
ELISP=${PREFIX}/${ELISPP}
DEST_ELISP=${DEST_PREFIX}/${ELISPP}
BINDIR=${PREFIX}/bin
DESKTOP=${PREFIX}/share
DOCDIR=${PREFIX}/share/doc/ProofGeneral
MANDIR=${PREFIX}/share/man/man1
INFODIR=${PREFIX}/share/info
install: install-desktop install-elisp install-bin install-init
install-desktop:
mkdir -p ${DESKTOP}/icons/hicolor/16x16/apps
cp etc/desktop/icons/16x16/proofgeneral.png ${DESKTOP}/icons/hicolor/16x16/apps
mkdir -p ${DESKTOP}/icons/hicolor/32x32/apps
cp etc/desktop/icons/32x32/proofgeneral.png ${DESKTOP}/icons/hicolor/32x32/apps
mkdir -p ${DESKTOP}/icons/hicolor/48x48/apps
cp etc/desktop/icons/48x48/proofgeneral.png ${DESKTOP}/icons/hicolor/48x48/apps
mkdir -p ${DESKTOP}/icons/hicolor/64x64/apps
cp etc/desktop/icons/64x64/proofgeneral.png ${DESKTOP}/icons/hicolor/64x64/apps
mkdir -p ${DESKTOP}/icons/hicolor/128x128/apps
cp etc/desktop/icons/128x128/proofgeneral.png ${DESKTOP}/icons/hicolor/128x128/apps
mkdir -p ${DESKTOP}/applications
cp etc/desktop/proofgeneral.desktop ${DESKTOP}/applications
mkdir -p ${DESKTOP}/mime-info
cp etc/desktop/mime-info/proofgeneral.mime ${DESKTOP}/mime-info
cp etc/desktop/mime-info/proofgeneral.keys ${DESKTOP}/mime-info
# backwards compatibility with old linuxes
mkdir -p ${DESKTOP}/application-registry
cp etc/desktop/application-registry/proofgeneral.applications ${DESKTOP}/application-registry
# NB: .el files are not strictly necessary, but we package/install them
# for the time being to help with debugging, or for users to recompile.
install-elisp: install-el install-elc
# NB: "elisp" directory actually includes the extra subdirs in EXTRA_DIRS,
# i.e. images. FIXME: we could put these elsewhere, but
# then we would need to adjust paths in proof-site.el.
# FIMXE 3: Michaël Cadilhac pointed out that 'cp -p' when used with
# sudo to install will give users ownership instead of root.
# Should use install program or fix ownerships afterwards here.
install-el:
mkdir -p ${ELISP}
for f in ${ELISP_DIRS_INST} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done
for f in ${ELISP_DIRS_INST}; do cp -pf $$f/*.el ${ELISP}/$$f; done
for f in ${EXTRA_DIRS}; do cp -prf $$f/* ${ELISP}/$$f; done
for f in ${ELISP_EXTRAS}; do cp -pf $$f ${ELISP}/$$f; done
install-elc: compile
mkdir -p ${ELISP}
for f in ${ELISP_DIRS_INST} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done
for f in ${ELISP_DIRS_INST}; do cp -pf $$f/*.elc ${ELISP}/$$f; done
for f in ${ELISP_EXTRAS}; do cp -pf $$f ${ELISP}/$$f; done
install-init:
mkdir -p ${ELISP_START}
echo ';;; pg-init.el --- setup for Proof General' > ${ELISP_START}/pg-init.el
echo "(setq load-path (append load-path '(\"${DEST_ELISP}/generic\")))" >> ${ELISP_START}/pg-init.el
echo "(require 'proof-site)" >> ${ELISP_START}/pg-init.el
install-bin: scripts
mkdir -p ${BINDIR}
cp -pf ${BIN_SCRIPTS} ${BINDIR}
install-doc: doc.info doc.pdf
mkdir -p ${MANDIR}
cp -pf doc/proofgeneral.1 ${MANDIR}
mkdir -p ${INFODIR}
cp -pf doc/*.info ${INFODIR}
/sbin/install-info ${INFODIR}/ProofGeneral.info* ${INFODIR}/dir
/sbin/install-info ${INFODIR}/PG-adapting.info* ${INFODIR}/dir
mkdir -p ${DOCDIR}
for f in ${DOC_FILES}; do cp -pf $$f ${DOCDIR}; done
for f in ${DOC_EXAMPLES}; do mkdir -p ${DOCDIR}/`dirname $$f`; cp -pf $$f ${DOCDIR}/$$f; done
doc: FORCE
(cd doc; $(MAKE) EMACS=$(EMACS) $*)
doc.%: FORCE
(cd doc; $(MAKE) EMACS=$(EMACS) $*)
##
## scripts: try to patch bash and perl scripts with correct paths
##
.PHONY: scripts
scripts: bashscripts perlscripts
.PHONY: bashscripts
bashscripts:
(bash="`which bash`"; \
if [ -z "$$bash" ]; then \
echo "Could not find bash - bash paths not checked" >&2; \
exit 0; \
fi)
.PHONY: perlscripts
perlscripts:
(perl="`which perl`"; \
if [ -z "$$perl" ]; then \
echo "Could not find perl - perl paths not checked" >&2; \
exit 0; \
fi; \
for i in $(PERL_SCRIPTS); do \
sed -i.orig "s|^#.*!.*/bin/perl.*$$|#!$$perl|" $$i; \
done)
# Set PGHOME path in scripts back to default location.
.PHONY: cleanscripts
cleanscripts:
(for i in $(PERL_SCRIPTS); do \
if [ -f $$i.rm ] ; then \
rm -f $$i.rm; \
fi; \
if [ -f $$i.orig ] ; then \
mv -f $$i.orig $$i; \
fi; \
done)
##
## Include developer's makefile if it exists here.
##
-include Makefile.devel