blob: 2aac55004ed0b84017f8690b7a6550d9803ce1a9 (
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
|
##
## Makefile for Proof General.
##
## Author: David Aspinall <da@dcs.ed.ac.uk>
##
## make - do "compile" and "scripts" targets
## make compile - make .elc's in a single session
## make all - make .elc's in separate sessions
## make scripts - edit paths in isabelle interface scripts,
## legotags and coqtags
##
## $Id$
##
###########################################################################
ELISP_DIRS = generic lego coq isa isar plastic demoisa hol98 phox twelf acl2
# FIXME: automate the emacs choice to be xemacs if it can be
# found, otherwise emacs.
BATCHEMACS=xemacs -batch -q -no-site-file
PWD=$(shell pwd)
BASH_SCRIPTS = isa/interface isar/interface
PERL_SCRIPTS = lego/legotags coq/coqtags
# FIXME: would rather set load path 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 so these are set just in that one
# place.
BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (concat "${PWD}/" (symbol-name d))) (quote (${ELISP_DIRS}))) load-path))' -f batch-byte-compile
EL=$(shell for f in $(ELISP_DIRS); do ls $$f/*.el; done)
ELC=$(EL:.el=.elc)
# Some parts of code were not compile safe, because of macros
# being expanded too early (e.g. proof-defshortcut, easy-menu-define)
# This should be fixed for 3.5, although careful testing is required.
BROKENELC=
.SUFFIXES: .el .elc
default: compile scripts
##
## compile : byte compile files in working directory:
## Clearout old .elc's and re-compile in a
## single Emacs process. This is faster than make all,
## but can have artefacts because of context between
## compiles.
##
compile:
@echo "*************************************************"
@echo " Byte compiling..."
@echo "*************************************************"
rm -f $(ELC)
$(BYTECOMP) $(EL)
rm -f $(BROKENELC)
@echo "*************************************************"
@echo " Finished."
@echo "*************************************************"
all: $(ELC)
.el.elc:
$(BYTECOMP) $*.el
rm -f $(BROKENELC)
##
## scripts: try to patch bash and perl scripts with correct paths
##
scripts: bashscripts perlscripts
bashscripts:
@(bash="`which bash`"; \
if [ -z "$$bash" ]; then \
echo "Could not find bash - bash paths not checked" >&2; \
exit 0; \
fi; \
for i in $(BASH_SCRIPTS); do \
sed "s|^#.*!.*/bin/bash.*$$|#!$$bash|" < $$i > .tmp \
&& cat .tmp > $$i; \
done; \
rm -f .tmp)
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 "s|^#.*!.*/bin/perl.*$$|#!$$perl|" < $$i > .tmp \
&& cat .tmp > $$i; \
done; \
rm -f .tmp)
clean:
rm -f $(ELC) *~ */*~ .\#* */.\#*
(cd doc; $(MAKE) clean)
##
## This special target lets us use targets defined
## in developer's makefile Makefile.devel conveniently,
## via make devel.<target>
##
devel.%:
make -f Makefile.devel $*
##
## Similarly for xemacs Makefile.
##
xemacs.%:
make -f Makefile.xemacs $*
|