1826
|
1 |
###############################################
|
|
2 |
# Title: Tools/8bit/Makefile
|
|
3 |
# ID: $Id$
|
|
4 |
# Author: Franz Regensburger
|
|
5 |
# Copyright 1996 TU Muenchen
|
|
6 |
#
|
|
7 |
# Master Makefile for Isabelle 8bit package
|
|
8 |
# ATTENTION: this is a GNU-MAKE Makefile
|
|
9 |
#
|
|
10 |
# Franz Regensburger <regensbu@informatik.tu-muenchen.de>, 8.3.95
|
|
11 |
# last changed:
|
|
12 |
# 21.3.95
|
|
13 |
# 02.09.95 added latex2e support
|
|
14 |
# 07.02.96 added BASH variable and changed reference to amssym
|
|
15 |
# in amssymb for latex2.09
|
|
16 |
# 23.05.96 modifications by David von Oheimb
|
|
17 |
#
|
|
18 |
###############################################
|
|
19 |
|
|
20 |
# operate silently
|
|
21 |
MAKEFLAGS='s'
|
|
22 |
|
|
23 |
###############################################
|
|
24 |
# general configuration
|
|
25 |
###############################################
|
|
26 |
|
|
27 |
# path and name of bash shell
|
|
28 |
# should be /bin/bash on every reasonable system
|
|
29 |
#
|
|
30 |
#BASH=/bin/bash
|
|
31 |
BASH=/bin/bash
|
|
32 |
|
|
33 |
# Perl path and name for interpreter
|
|
34 |
# should be a perl 4.x
|
|
35 |
#PERL=/usr/bin/perl
|
|
36 |
PERL=/usr/local/dist/DIR/perl4/bin/perl
|
|
37 |
|
|
38 |
# use LaTeX2e instead of LaTeX 2.09
|
|
39 |
# this flag is currently only sensible for perl script gen-isadoc
|
|
40 |
# set to empty string for LaTeX 2.09
|
|
41 |
USE2E='-2e'
|
|
42 |
|
|
43 |
# name of GNU make utility: `make' on linux box; `gmake' on solaris
|
|
44 |
#GMAKE=make
|
|
45 |
GMAKE=gmake
|
|
46 |
|
|
47 |
#keycode for Super_L 26 on SUN, 64 on Linux box
|
|
48 |
#SUPER_L=64
|
|
49 |
SUPER_L=26
|
|
50 |
|
|
51 |
#keycode for Hyper_R 20 on SUN, 113 on Linux box
|
|
52 |
#HYPER_R=113
|
|
53 |
HYPER_R=20
|
|
54 |
|
1907
|
55 |
CONFIGFILES = config/Makefile config/key-table.inp config/conv-tables.inp
|
1826
|
56 |
|
1856
|
57 |
#path stem to isabelle source, used by patcher
|
2392
|
58 |
STEM = /usr/wiss/oheimb/isabelle/
|
1856
|
59 |
|
1826
|
60 |
###############################################
|
|
61 |
# configuration for configuration files in ./config
|
|
62 |
###############################################
|
|
63 |
|
|
64 |
CONV_SOURCE_DIR="$(ISABELLE8BIT)/c-sources/isa2latex"
|
|
65 |
|
|
66 |
###############################################
|
|
67 |
# configuration for GNU emacs
|
|
68 |
###############################################
|
|
69 |
|
|
70 |
# Name of your GNU emacs executable
|
|
71 |
GNU_ENAME=emacs
|
|
72 |
|
|
73 |
#users init file ($HOME is added). This file is loaded after
|
|
74 |
#the init file isa_gnu_emacs.emacs
|
|
75 |
GNU_INIT=.emacs_gnu_isa
|
|
76 |
|
|
77 |
###############################################
|
|
78 |
# configuration for xemacs
|
|
79 |
###############################################
|
|
80 |
|
|
81 |
# Name of your xemacs executable
|
|
82 |
|
|
83 |
XEMACS_ENAME=xemacs
|
|
84 |
|
|
85 |
#users init file ($HOME is added). This file is loaded after
|
|
86 |
#the init file isa_xemacs.emacs
|
|
87 |
|
|
88 |
XEMACS_INIT=.emacs_xemacs_isa
|
|
89 |
|
|
90 |
###############################################
|
|
91 |
# END of Configuration Section
|
|
92 |
###############################################
|
|
93 |
|
|
94 |
|
|
95 |
###############################################
|
|
96 |
# user targets
|
|
97 |
###############################################
|
|
98 |
|
|
99 |
# ----------------------------------------------------
|
|
100 |
|
|
101 |
# first target. Used if no target is given by the user
|
|
102 |
#usage:
|
|
103 |
# echo "type 'make install' to install everything"
|
|
104 |
# echo "type 'make clean' to cleanup"
|
|
105 |
|
|
106 |
# ----------------------------------------------------
|
|
107 |
|
1907
|
108 |
all: $(CONFIGFILES)\
|
1826
|
109 |
bin/gen-isa2latex bin/gen-isaterm bin/gen-isavim bin/gen-isaaxe\
|
|
110 |
bin/gen-isa_gnu_emacs bin/gen-isa_xemacs bin/gen-isadoc\
|
|
111 |
configuration a2isa bin/isa2latex bin/a2isa\
|
|
112 |
bin/isa_gnu_emacs bin/isa_xemacs bin/isavim bin/isaaxe\
|
|
113 |
bin/isaterm bin/isa_xmosaic bin/isapal bin/codetable bin/patcher\
|
|
114 |
fonts/install keyboard/install\
|
1856
|
115 |
isa-patches/HOL/add-HOL.cfg isa-patches/HOL/clean-HOL.cfg\
|
|
116 |
isa-patches/HOL/extract-HOL.cfg\
|
|
117 |
isa-patches/HOLCF/add-HOLCF.cfg isa-patches/HOLCF/clean-HOLCF.cfg\
|
|
118 |
isa-patches/HOLCF/extract-HOLCF.cfg\
|
|
119 |
manual\
|
1826
|
120 |
|
|
121 |
# ----------------------------------------------------
|
|
122 |
|
|
123 |
clean:
|
1856
|
124 |
cd bin; rm -f a2isa codetable gen-* isa* patcher
|
1826
|
125 |
cd c-sources/a2isa; $(GMAKE) clean
|
|
126 |
cd c-sources/isa2latex; $(GMAKE) clean
|
1856
|
127 |
cd doc; $(GMAKE) clean
|
1826
|
128 |
|
|
129 |
###############################################
|
|
130 |
# internal targets
|
|
131 |
###############################################
|
|
132 |
|
|
133 |
####### configuration files and the Makefile
|
|
134 |
|
1907
|
135 |
$(CONFIGFILES): Makefile
|
1826
|
136 |
@echo "configuring the configuration files"
|
|
137 |
@cd config;\
|
|
138 |
$(PERL) -pi \
|
|
139 |
-e "s#^USE2E\s*=.*#USE2E= $(USE2E)#g;" \
|
1907
|
140 |
-e "s#^GMAKE\s*=.*#GMAKE= $(GMAKE)#g;" \
|
1826
|
141 |
Makefile
|
|
142 |
@cd config;\
|
|
143 |
$(PERL) -pi \
|
|
144 |
-e "s#^BIN_DIR\s*\".*#BIN_DIR \"$(CONV_BIN_DIR)\"#g;" \
|
|
145 |
key-table.inp
|
|
146 |
@cd config;\
|
|
147 |
$(PERL) -pi \
|
|
148 |
-e "s#^CONV_SOURCE_DIR\s*\".*#CONV_SOURCE_DIR \"$(CONV_SOURCE_DIR)\"#g;" \
|
|
149 |
conv-tables.inp
|
|
150 |
|
|
151 |
####### Generators
|
|
152 |
|
|
153 |
# ----------------------------------------------------
|
|
154 |
|
|
155 |
bin/gen-isa2latex: Makefile #perl/generators/gen-isa2latex.pl
|
|
156 |
@echo "configuring gen-isa2latex"
|
|
157 |
@cd perl/generators;\
|
|
158 |
$(PERL) -pi \
|
1907
|
159 |
-e "s#GMAKE\s*=.*#GMAKE= \"$(GMAKE)\";#g;" \
|
1826
|
160 |
-e "s&^#!.*&#!$(PERL)&g;" \
|
|
161 |
gen-isa2latex.pl
|
|
162 |
@rm -f bin/gen-isa2latex;\
|
|
163 |
ln -s ../perl/generators/gen-isa2latex.pl bin/gen-isa2latex
|
|
164 |
|
|
165 |
# ----------------------------------------------------
|
|
166 |
|
|
167 |
bin/gen-isaterm: Makefile #perl/generators/gen-isaterm.pl
|
|
168 |
@echo "configuring gen-isaterm"
|
|
169 |
@cd perl/generators;\
|
|
170 |
$(PERL) -pi \
|
|
171 |
-e "s&^#!.*&#!$(PERL)&g;" \
|
|
172 |
gen-isaterm.pl
|
|
173 |
@rm -f bin/gen-isaterm;\
|
|
174 |
ln -s ../perl/generators/gen-isaterm.pl bin/gen-isaterm
|
|
175 |
|
|
176 |
# ----------------------------------------------------
|
|
177 |
|
|
178 |
bin/gen-isavim: Makefile #perl/generators/gen-isavim.pl
|
|
179 |
@echo "configuring gen-isavim"
|
|
180 |
@cd perl/generators;\
|
|
181 |
$(PERL) -pi \
|
|
182 |
-e "s&^#!.*&#!$(PERL)&g;" \
|
|
183 |
gen-isavim.pl
|
|
184 |
@rm -f bin/gen-isavim;\
|
|
185 |
ln -s ../perl/generators/gen-isavim.pl bin/gen-isavim
|
|
186 |
|
|
187 |
# ----------------------------------------------------
|
|
188 |
|
|
189 |
bin/gen-isaaxe: Makefile #perl/generators/gen-isaaxe.pl
|
|
190 |
@echo "configuring gen-isaaxe"
|
|
191 |
@cd perl/generators;\
|
|
192 |
$(PERL) -pi \
|
|
193 |
-e "s&^#!.*&#!$(PERL)&g;" \
|
|
194 |
gen-isaaxe.pl
|
|
195 |
@rm -f bin/gen-isaaxe;\
|
|
196 |
ln -s ../perl/generators/gen-isaaxe.pl bin/gen-isaaxe
|
|
197 |
|
|
198 |
# ----------------------------------------------------
|
|
199 |
|
|
200 |
bin/gen-isa_gnu_emacs: Makefile #perl/generators/gen-isa_gnu_emacs.pl
|
|
201 |
@echo "configuring gen-isa_gnu_emacs"
|
|
202 |
@cd perl/generators;\
|
|
203 |
$(PERL) -pi \
|
|
204 |
-e "s&^#!.*&#!$(PERL)&g;" \
|
|
205 |
gen-isa_gnu_emacs.pl
|
|
206 |
@rm -f bin/gen-isa_gnu_emacs;\
|
|
207 |
ln -s ../perl/generators/gen-isa_gnu_emacs.pl bin/gen-isa_gnu_emacs
|
|
208 |
|
|
209 |
# ----------------------------------------------------
|
|
210 |
|
|
211 |
bin/gen-isa_xemacs: Makefile #perl/generators/gen-isa_xemacs.pl
|
|
212 |
@echo "configuring gen-isa_xemacs"
|
|
213 |
@cd perl/generators;\
|
|
214 |
$(PERL) -pi \
|
|
215 |
-e "s&^#!.*&#!$(PERL)&g;" \
|
|
216 |
gen-isa_xemacs.pl
|
|
217 |
@rm -f bin/gen-isa_xemacs;\
|
|
218 |
ln -s ../perl/generators/gen-isa_xemacs.pl bin/gen-isa_xemacs
|
|
219 |
|
|
220 |
# ----------------------------------------------------
|
|
221 |
|
|
222 |
bin/gen-isadoc: Makefile #perl/generators/gen-isadoc.pl
|
|
223 |
@echo "configuring gen-isadoc"
|
|
224 |
@cd perl/generators;\
|
|
225 |
$(PERL) -pi \
|
|
226 |
-e "s&^#!.*&#!$(PERL)&g;" \
|
|
227 |
gen-isadoc.pl
|
|
228 |
@rm -f bin/gen-isadoc;\
|
|
229 |
ln -s ../perl/generators/gen-isadoc.pl bin/gen-isadoc
|
|
230 |
|
|
231 |
|
|
232 |
####### Converter
|
|
233 |
|
|
234 |
# ----------------------------------------------------
|
|
235 |
|
|
236 |
#isa2latex, editor support, font documentation:
|
|
237 |
configuration:
|
|
238 |
@cd config; $(GMAKE)
|
|
239 |
|
|
240 |
a2isa:
|
|
241 |
@cd c-sources/a2isa; $(GMAKE); $(GMAKE) clean
|
|
242 |
|
|
243 |
bin/isa2latex: c-sources/isa2latex/isa2latex
|
|
244 |
@echo "installing isa2latex"
|
|
245 |
@rm -f bin/isa2latex;\
|
1988
|
246 |
ln -s ../c-sources/isa2latex/isa2latex bin/isa2latex
|
1826
|
247 |
|
|
248 |
bin/a2isa: c-sources/a2isa/a2isa
|
|
249 |
@echo "installing a2isa"
|
|
250 |
@rm -f bin/a2isa;\
|
|
251 |
ln -s ../c-sources/a2isa/a2isa bin/a2isa
|
|
252 |
|
|
253 |
####### Editors
|
|
254 |
|
|
255 |
# ----------------------------------------------------
|
|
256 |
|
|
257 |
bin/isa_gnu_emacs: Makefile #gnu_emacs/isa_gnu_emacs
|
|
258 |
@echo "installing GNU emacs"
|
|
259 |
@cd gnu_emacs;\
|
|
260 |
$(PERL) -pi \
|
|
261 |
-e "s&^#!.*&#!$(BASH)&g;" \
|
|
262 |
-e "s#^ENAME\s*=.*#ENAME=$(GNU_ENAME)#g;"\
|
|
263 |
-e "s#^INIT\s*=.*#INIT=$(GNU_INIT)#g;" \
|
|
264 |
isa_gnu_emacs
|
|
265 |
@rm -f bin/isa_gnu_emacs;\
|
|
266 |
ln -s ../gnu_emacs/isa_gnu_emacs bin/isa_gnu_emacs
|
|
267 |
|
|
268 |
# ----------------------------------------------------
|
|
269 |
|
|
270 |
bin/isa_xemacs: Makefile #xemacs/isa_xemacs
|
|
271 |
@echo "installing xemacs"
|
|
272 |
@@cd xemacs;\
|
|
273 |
$(PERL) -pi\
|
|
274 |
-e "s&^#!.*&#!$(BASH)&g;" \
|
|
275 |
-e "s#^ENAME\s*=.*#ENAME=$(XEMACS_ENAME)#g;"\
|
|
276 |
-e "s#^INIT\s*=.*#INIT=$(XEMACS_INIT)#g;" \
|
|
277 |
isa_xemacs
|
|
278 |
@rm -f bin/isa_xemacs;\
|
|
279 |
ln -s ../xemacs/isa_xemacs bin/isa_xemacs
|
|
280 |
|
|
281 |
# ----------------------------------------------------
|
|
282 |
|
|
283 |
bin/isavim: Makefile #vim/isavim
|
|
284 |
@echo "installing vim"
|
|
285 |
@@cd vim;\
|
|
286 |
$(PERL) -pi\
|
|
287 |
-e "s&^#!.*&#!$(BASH)&g;" \
|
|
288 |
initvim ; \
|
|
289 |
$(PERL) -pi\
|
|
290 |
-e "s&^#!.*&#!$(BASH)&g;" \
|
|
291 |
isavim
|
|
292 |
@rm -f bin/isavim;\
|
|
293 |
ln -s ../vim/isavim bin/isavim
|
|
294 |
|
|
295 |
# ----------------------------------------------------
|
|
296 |
|
|
297 |
bin/isaaxe: Makefile #axe/isaaxe
|
|
298 |
@echo "installing axe"
|
|
299 |
@cd axe;\
|
|
300 |
$(PERL) -pi \
|
|
301 |
-e "s&^#!.*&#!$(BASH)&g;" \
|
|
302 |
isaaxe
|
|
303 |
@rm -f bin/isaaxe;\
|
|
304 |
ln -s ../axe/isaaxe bin/isaaxe
|
|
305 |
|
|
306 |
# ----------------------------------------------------
|
|
307 |
|
|
308 |
bin/isa_xmosaic: Makefile #xmosaic/isa_xmosaic
|
|
309 |
@echo "installing xmosaic"
|
|
310 |
@cd xmosaic;\
|
|
311 |
$(PERL) -pi\
|
|
312 |
-e "s&^#!.*&#!$(BASH)&g;" \
|
|
313 |
isa_xmosaic
|
|
314 |
@rm -f bin/isa_xmosaic;\
|
|
315 |
ln -s ../xmosaic/isa_xmosaic bin/isa_xmosaic
|
|
316 |
|
|
317 |
####### Terminal
|
|
318 |
|
|
319 |
# ----------------------------------------------------
|
|
320 |
|
|
321 |
bin/isaterm: Makefile #term/isaterm
|
|
322 |
@echo "installing term"
|
|
323 |
@cd term;\
|
|
324 |
$(PERL) -pi\
|
|
325 |
-e "s&^#!.*&#!$(BASH)&g;" \
|
|
326 |
initisaterm;\
|
|
327 |
$(PERL) -pi\
|
|
328 |
-e "s&^#!.*&#!$(BASH)&g;" \
|
|
329 |
isaterm
|
|
330 |
@rm -f bin/isaterm;\
|
|
331 |
ln -s ../term/isaterm bin/isaterm
|
|
332 |
|
|
333 |
####### other perl scripts
|
|
334 |
|
|
335 |
# ----------------------------------------------------
|
|
336 |
|
|
337 |
bin/isapal: Makefile #perl/isapal.pl
|
|
338 |
@echo "installing perl script isapal"
|
|
339 |
@cd perl;\
|
|
340 |
$(PERL) -pi \
|
|
341 |
-e "s&^#!.*&#!$(PERL)&g;"\
|
|
342 |
isapal.pl
|
|
343 |
@rm -f bin/isapal;\
|
|
344 |
ln -s ../perl/isapal.pl bin/isapal
|
|
345 |
|
|
346 |
bin/codetable: Makefile #perl/codetable.pl
|
|
347 |
@echo "installing perl script codetable"
|
|
348 |
@cd perl;\
|
|
349 |
$(PERL) -pi \
|
|
350 |
-e "s&^#!.*&#!$(PERL)&g;" \
|
|
351 |
codetable.pl
|
|
352 |
@rm -f bin/codetable;\
|
|
353 |
ln -s ../perl/codetable.pl bin/codetable
|
|
354 |
|
|
355 |
bin/patcher: Makefile #perl/patcher.pl
|
|
356 |
@echo "installing perl script patcher"
|
|
357 |
@cd perl;\
|
|
358 |
$(PERL) -pi \
|
|
359 |
-e "s&^#!.*&#!$(PERL)&g;" \
|
|
360 |
patcher.pl
|
|
361 |
@rm -f bin/patcher;\
|
|
362 |
ln -s ../perl/patcher.pl bin/patcher
|
|
363 |
|
|
364 |
fonts/install: Makefile
|
|
365 |
@cd fonts;\
|
|
366 |
$(PERL) -pi\
|
|
367 |
-e "s&^#!.*&#!$(BASH)&g;" \
|
|
368 |
install
|
|
369 |
|
|
370 |
keyboard/install: Makefile
|
|
371 |
@cd keyboard;\
|
|
372 |
$(PERL) -pi\
|
|
373 |
-e "s&^#!.*&#!$(BASH)&g;" \
|
|
374 |
-e "s#^SUPER_L\s*=.*#SUPER_L=$(SUPER_L)#g;"\
|
|
375 |
-e "s#^HYPER_R\s*=.*#HYPER_R=$(HYPER_R)#g;"\
|
|
376 |
install
|
|
377 |
|
1856
|
378 |
isa-patches/HOL/add-HOL.cfg: Makefile
|
|
379 |
@cd isa-patches/HOL;\
|
|
380 |
$(PERL) -pi -e "s#^STEM\s*\".*#STEM \"$(STEM)\"#g;" add-HOL.cfg
|
|
381 |
isa-patches/HOL/clean-HOL.cfg: Makefile
|
|
382 |
@cd isa-patches/HOL;\
|
|
383 |
$(PERL) -pi -e "s#^STEM\s*\".*#STEM \"$(STEM)\"#g;" clean-HOL.cfg
|
|
384 |
isa-patches/HOL/extract-HOL.cfg: Makefile
|
|
385 |
@cd isa-patches/HOL;\
|
|
386 |
$(PERL) -pi -e "s#^STEM\s*\".*#STEM \"$(STEM)\"#g;" extract-HOL.cfg
|
|
387 |
isa-patches/HOLCF/add-HOLCF.cfg: Makefile
|
|
388 |
@cd isa-patches/HOLCF;\
|
|
389 |
$(PERL) -pi -e "s#^STEM\s*\".*#STEM \"$(STEM)\"#g;" add-HOLCF.cfg
|
|
390 |
isa-patches/HOLCF/clean-HOLCF.cfg: Makefile
|
|
391 |
@cd isa-patches/HOLCF;\
|
|
392 |
$(PERL) -pi -e "s#^STEM\s*\".*#STEM \"$(STEM)\"#g;" clean-HOLCF.cfg
|
|
393 |
isa-patches/HOLCF/extract-HOLCF.cfg: Makefile
|
|
394 |
@cd isa-patches/HOLCF;\
|
|
395 |
$(PERL) -pi -e "s#^STEM\s*\".*#STEM \"$(STEM)\"#g;" extract-HOLCF.cfg
|
|
396 |
|
1826
|
397 |
# ----------------------------------------------------
|
|
398 |
|
|
399 |
manual:
|
1856
|
400 |
@cd doc; $(GMAKE) manual.dvi
|