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
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
|
#!/usr/bin/make -f
# Sample debian/rules that uses debhelper.
# GNU copyright 1997 by Joey Hess.
#
# This version is for a hypothetical package that builds an
# architecture-dependant package, as well as an architecture-independent
# package.
# Uncomment this to turn on verbose mode.
#export DH_VERBOSE=1
# This is the debhelper compatability version to use.
#export DH_COMPAT=4
# This has to be exported to make some magic below work.
export DH_OPTIONS
PN:=acl2
VR:=$(shell awk '{if (i) next;i=1;a=$$2;gsub("[()]","",a);split(a,A,"-");print A[1];}' debian/changelog)
PD:=$(PN)-$(VR)
NO_STRIP:=
# ifeq ($(DEB_BUILD_ARCH),powerpc)
# NO_STRIP:=--exclude=saved_acl2
# endif
# ACL2_HEAP_WORDS_NEEDED_FOR_CERTIFICATION:=500000000
# MAXJOBS:=$(shell gcl -batch -eval \
# "(print \
# (multiple-value-bind (a b c d) (si::heap-report) \
# (min 8 \
# (ceiling (/ (- d c) (/ a 8)) \
# ${ACL2_HEAP_WORDS_NEEDED_FOR_CERTIFICATION}))))")
NUMJOBS:=1
ifneq (,$(filter parallel=%,$(DEB_BUILD_OPTIONS)))
NUMJOBS:=$(patsubst parallel=%,%,$(filter parallel=%,$(DEB_BUILD_OPTIONS)))
endif
# NUMJOBS:=$(shell if test $(NUMJOBS) -gt ${MAXJOBS}; then echo ${MAXJOBS} ; else echo $(NUMJOBS); fi)
#books/workshops:
# mkdir $@
#init.lsp.ori:
# [ -e $@ ] || mv init.lsp $@
DLOPEN_T:=debian/dlopen.lisp #init.lsp.ori
#ifeq ($(DEB_BUILD_ARCH),ia64)
#DLOPEN?=$(DLOPEN_T)
#endif
#ifeq ($(DEB_BUILD_ARCH),alpha)
#DLOPEN?=$(DLOPEN_T)
#endif
#ifeq ($(DEB_BUILD_ARCH),mips)
#DLOPEN?=$(DLOPEN_T)
#endif
#ifeq ($(DEB_BUILD_ARCH),mipsel)
#DLOPEN?=$(DLOPEN_T)
#endif
#ifeq ($(DEB_BUILD_ARCH),hppa)
#DLOPEN?=$(DLOPEN_T)
#endif
debian/dlopen.lisp: debian/dlopen.lisp.in
cat $< | sed "s,@VR@,$(VR),g" > $@
debian/acl2-emacs.emacsen-startup: debian/acl2-emacs.emacsen-startup.in
cat $< | sed "s,@VR@,$(VR),g" > $@
#pgcl:
# echo "(progn (setq compiler::*split-files* 100000)(si::save-system \"$@\"))" | GCL_ANSI=t gcl
saved_acl2: # pgcl #debian/patches_applied $(DLOPEN_T)
# gcl -batch -eval "(bye #-native-reloc 1)" || \
# (gcl -batch -eval '(load "debian/dlopen.lisp")' && $(MAKE) do_saved)
# gcl -batch -eval "(bye #+native-reloc 1)" || $(MAKE) GCL_ANSI=t LISP=gcl
$(MAKE) GCL_ANSI=t LISP=gcl
mv *$@.gcl $@
saved_acl2.c: saved_acl2
echo "(f-put-global 'old-certification-dir \"$$(pwd)/books\" state)" \
"(f-put-global 'new-certification-dir \"/usr/share/$(PD)/books\" state)" \
":q #-native-reloc (setq si::*multiply-stacks* 4) :q (in-package :acl2) " \
"#+(or sparc sparc64)(progn (si::sgc-on nil) (fmakunbound 'si::sgc-on))" \
"(save-exec \"$@\" \"Modified to produce final certification files\")" | HOME=$$(pwd) ./$<
mv $@.gcl $@
debian/mini-proveall.out: saved_acl2
HOME=$$(pwd) $(MAKE) mini-proveall
mv $(@F) $@
books/short-test.log: saved_acl2.c
cp saved_acl2 saved_acl2.ori
HOME=$$(pwd) $(MAKE) certify-books-short
cp saved_acl2.ori saved_acl2
# tail -f --pid=$$j --retry $@ $$(find books -name "*.lisp" | sed 's,\.lisp$$,.out,1') & \
debian/test.log: saved_acl2.c
mv saved_acl2 saved_acl2.ori
cp $< saved_acl2
BUILDDIR="$$(dirname $$(pwd))" \
FINALDIR="/usr/share/$(PD)" \
HOME=$$(pwd) \
GCL_MULTIPROCESS_MEMORY_POOL=t \
$(MAKE) -j $(NUMJOBS) -l 2.95 regression-fresh 2>&1 | tee $@ & j=$$! ; \
while sleep 1800; do echo Tick; done & k=$$! ; \
wait $$j ; kill $$k
# >$@ 2>&1 & j=$$! ; \
# while sleep 1800; do echo Tick; done & k=$$! ; tail -f debian/test.log & l=$$! ; \
# wait $$j ; kill $$k $$l
# [ -f $@ ] && ! fgrep '**' $@ || (echo FULL TEST FAILS ;\
# for i in $$(find books -name "*.out"); do \
# if ! [ -e $${i%out}cert ] ; then \
# echo $$i ; \
# cat $$i ; \
# fi ; \
done)
mv saved_acl2.ori saved_acl2
[ -f $@ ] && ( ! fgrep '**' $@ || true )
# gcl -batch -eval \
# "(bye \
# #-native-reloc 0 \
# #+native-reloc \
# (let ((w (multiple-value-bind (a b c d) (si::heap-report) (/ (- d c) (/ a 8))))) \
# (format t \"certification run with ~s heap words~%\" w) \
# (if (< w ${ACL2_HEAP_WORDS_NEEDED_FOR_CERTIFICATION}) 0 1)))")
books/interface/infix/Makefile: books/interface/infix/makefile
sed -e "s,^DIR = .*,DIR = $$(pwd)/books/interface/infix,1" \
-e "s,^LISP = .*,LISP = $$(pwd)/saved_acl2,1" $< > $@
infix-stamp: books/interface/infix/Makefile saved_acl2
cd books/interface/infix && make -f Makefile compile
cd books/interface/infix && make -f Makefile example
# cd books/interface/infix && make -f Makefile events
touch $@
doc/TEX/acl2-book.ps.gz: saved_acl2
HOME=$$(pwd) $(MAKE) DOC
rm -f doc/HTML/LICENSE
find doc -empty -exec rm {} \;
build: build-arch build-indep
build-arch: build-stamp
build-indep: build-stamp
build-stamp: debian/mini-proveall.out debian/test.log infix-stamp # doc/TEX/acl2-book.ps.gz
dh_testdir
# $(MAKE)
touch build-stamp
infix_clean: books/interface/infix/Makefile
rm -f infix-stamp
cd books/interface/infix && make -f Makefile clean
rm -f books/interface/infix/Makefile
debian/dpatches: debian/patches.in
debian/rules debian/patches_unapplied
cat $< | sed -e "s,@BDIR@,$$(pwd),1" -e "s,@DDIR@,/usr/share/$(PD),1" >$@
debian/patches_applied: debian/dpatches
! [ -e debian/patches_unapplied ] || \
(patch -p1 < $< && rm -f debian/patches_unapplied)
touch $@
debian/patches_unapplied:
! [ -e debian/patches_applied ] || ! [ -e debian/dpatches ] || \
(patch -p1 -R < debian/dpatches && rm -f debian/patches_applied)
touch $@
INSTALLS:=$(addprefix debian/,$(addsuffix .install,acl2 acl2-source acl2-emacs acl2-doc acl2-books acl2-books-source acl2-books-certs acl2-infix acl2-infix-source))
LINKS:=$(addprefix debian/,$(addsuffix .links,acl2 acl2-books acl2-infix))
IFILES:=$(INSTALLS) $(shell ls -1 debian/*.examples debian/*.docs)
debian/README.Debian: debian/README.Debian.in $(IFILES)
awk '/@PLIST@/ {exit 0} {print}' $< >$@
for i in $(filter %.install,$^); do\
awk '/^debian\// {next} {sub(".final$$","",$$1);$$2="/" $$2;print $$0 " " p}' \
p=$$(basename $${i%.install}) $$i >>$@ ; done
for i in $(filter %.info,$^); do\
awk '/^debian\// {next} {print $$0 " /usr/share/info " p}' p=$$(basename $${i%.info}) $$i >>$@ ; done
for i in $(filter %.examples,$^); do\
awk '/^debian\// {next} {print $$0 " /usr/share/doc/" p "/examples " p}' \
p=$$(basename $${i%.examples}) $$i >>$@ ; done
for i in $(filter %.docs,$^); do\
awk '/^debian\// {next} {print $$0 " /usr/share/doc/" p " " p}' p=$$(basename $${i%.docs}) $$i >>$@ ; done
awk '/@PLIST@/ {i=1;next} {if (i) print}' $< >>$@
OVERRIDES:= $(shell find debian/ -name "*.lintian-overrides.in" |sed 's,\.in,,g')
clean: infix_clean #debian/patches_unapplied books/workshops
dh_testdir
dh_testroot
rm -f build-stamp
$(MAKE) clean-all
$(MAKE) clean-books
find books -name "*.final" -exec rm {} \;
rm -f saved_acl2 init_nsaved1_acl2.lsp worklispext
rm -f debian/mini-proveall.out books/short-test.log debian/test.log
# ! [ -e init.lsp.ori ] || mv init.lsp.ori init.lsp
rm -f foo.lsp nsaved_acl2
for i in data c h ; do \
for j in $$(find -name "*.$$i") ; do\
k=$$(echo $$j | sed "s,\.$$i$$,,1") ;\
! [ -e $$k.lisp ] || rm $$j ; \
done ; \
done
rm -f books/bdd/benchmarks.data acl2r.lisp tmp
rm -f debian/dpatches $(INSTALLS) $(LINKS) debian/README.Debian saved_acl2*
rm -f debian/dlopen.lisp debian/acl2-emacs.emacsen-startup
rm -f debian/acl2.sh pgcl books/Makefile-tmp books/coi/gensym/gensym.out sys-proclaim.lisp
rm -f books/coi/gensym/Makefile-deps books/coi/gensym/workxxx.gensym books/system/doc/rendered-doc.lsp
rm -rf doc/HTML-old doc/EMACS-old doc/acl2-wc.txt books/std/io/test.sao
rm -f books/centaur/bitops/bitsets-opt-raw.o books/centaur/vl/util/gc-raw.o \
books/centaur/misc/tshell-raw.o books/centaur/vl/Makefile-tmp \
books/build/Makefile-sources books/build/Makefile-certs
rm -f books/build/acl2-exports.certdep books/build/acl2-version.certdep \
books/build/first-order-like-terms-and-out-arities.certdep \
books/build/ground-zero-theory.certdep gcl_pool
rm -f $(OVERRIDES)
rm -f books/centaur/fty/tests/deftagsum-scale.cert.temp books/centaur/fty/tests/deftranssum.cert.temp
rm -f books/centaur/vl/kit/test.vlzip books/centaur/getopt/demo2 books/centaur/getopt/demo2-test.ok
dh_clean -XTAGS
debian/acl2-infix.install::
find books/interface/infix -name "*.o" | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/lib/$(PD)/%s\n",$$1,a);}' >>$@
find books/interface/infix -name "*.sty" | \
awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/texmf/tex/latex\n",$$1);}' >>$@
debian/acl2-infix-source.install::
find books/interface/infix -name "*.lisp" | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/lib/$(PD)/%s\n",$$1,a);}' >>$@
debian/acl2-emacs.install::
find books/interface/emacs -name "*.el" | awk '{printf("%s usr/share/emacs/site-lisp/$(PN)\n",$$1);}' >>$@
find emacs -name "*.el" | awk '{printf("%s usr/share/emacs/site-lisp/$(PN)\n",$$1);}' >>$@
debian/acl2.install::
echo debian/acl2.sh usr/bin >>$@
echo saved_acl2 usr/lib/$(PD) >>$@
debian/acl2-books.install::
find books -name "*.o" | grep -v interface/ | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/lib/$(PD)/%s\n",$$1,a);}' >>$@
debian/acl2-source.install::
find * -name "*.lisp" -maxdepth 0 | grep -v TMP1.lisp | awk '{printf("%s usr/share/$(PD)\n",$$1);}' >$@
find * -name "TAGS" -maxdepth 0 | awk '{printf("%s usr/share/$(PD)\n",$$1);}' >>$@
debian/acl2-books-certs.install::
find books -name "*.cert" | grep -v fix-cert/moved | grep -v system/pcert | \
awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/$(PD)/%s\n",$$1,a);}' >>$@
find books -name "*.pcert0.final" | \
awk '{a=$$1;sub(".pcert0.final",".cert",a);printf("%s usr/share/$(PD)/%s\n",$$1,a);}' >>$@
debian/acl2-books-source.install::
find books -name "*.lisp" | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/$(PD)/%s\n",$$1,a);}' >>$@
find books -name "*.acl2" | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/$(PD)/%s\n",$$1,a);}' >>$@
find books/bdd -name "bit-vector-reader.lsp" | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/$(PD)/%s\n",$$1,a);}' >>$@
debian/acl2-doc.install::
echo doc usr/share/doc/acl2-doc >$@
find books -name "README*" | \
awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
find books/textbook -name "*.txt" | \
awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
find books/textbook -name "*.html" | \
awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
find books/bdd/be/ -type f | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
find books/misc -name "simplify-defuns.txt" | \
awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
find books/interface/infix -name "README*" | \
awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
find books/interface/infix -name "*.ps" | \
awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
find books/interface/infix -name "*.dvi" | \
awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
find books/interface/emacs -name "README*" | \
awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
find books/arithmetic-2/pass1/arithmetic-axioms.txt | \
awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
debian/acl2.links::
echo usr/lib/$(PD)/saved_acl2 usr/share/$(PD)/saved_acl2 >$@
debian/acl2-books.links::
find books -name "*.o" | grep -v interface/ | awk '{printf("usr/lib/$(PD)/%s usr/share/$(PD)/%s\n",$$1,$$1);}' >>$@
debian/acl2-infix.links::
find books/interface/infix -name "*.o" | awk '{printf("usr/lib/$(PD)/%s usr/share/$(PD)/%s\n",$$1,$$1);}' >>$@
debian/acl2.sh:
echo "#!/bin/bash" >$@
echo >>$@
echo "export ACL2_SYSTEM_BOOKS=/usr/share/$(PD)/books" >>$@
echo "exec /usr/lib/$(PD)/saved_acl2 -dir /usr/share/$(PD)" >>$@
chmod 755 $@
%.lintian-overrides: %.lintian-overrides.in
cat $< | sed "s,@PD@,$(PD),g" > $@
install: DH_OPTIONS=
install: build $(INSTALLS) $(LINKS) debian/acl2.sh debian/acl2-emacs.emacsen-startup debian/README.Debian $(OVERRIDES)
dh_testdir
dh_testroot
dh_prep -XTAGS
dh_installdirs
dh_install
rm -f debian/acl2-doc/usr/share/doc/acl2-doc/doc/manual/LICENSE
rm -f debian/acl2-doc/usr/share/doc/acl2-doc/doc/.gitignore
find debian/acl2-books-source/usr/share/$(PD)/books/quicklisp/bundle/software/ -type f -name release.lisp -exec rm {} \;
-find debian/acl2-doc/usr/share/doc/acl2-doc// -type f -size 0 -exec rm {} \;
for i in $$(find debian -name "*.final"); do mv $$i $${i%.final} ; done
find debian/acl2-source -name "*.lisp" -type f -exec chmod 444 {} \;
find debian/acl2-source -name "*.acl2" -type f -exec chmod 444 {} \;
find debian/acl2-source -name "*.lsp" -type f -exec chmod 444 {} \;
find debian/acl2-books-source -name "*.lisp" -type f -exec chmod 444 {} \;
find debian/acl2-books-source -name "*.acl2" -type f -exec chmod 444 {} \;
find debian/acl2-books-source -name "*.lsp" -type f -exec chmod 444 {} \;
mv debian/acl2/usr/bin/acl2.sh debian/acl2/usr/bin/acl2
binary-indep: DH_OPTIONS:=-i
binary-indep: build install
dh_testdir
dh_testroot
dh_installdocs
dh_installexamples
dh_installmenu
dh_installemacsen
dh_installtex -p acl2-infix
dh_installcron
DH_OPTIONS= dh_installinfo -p acl2-doc #$$(find doc/EMACS -name "*.info*")
dh_installchangelogs
dh_link
dh_compress
dh_lintian
dh_fixperms
dh_installdeb
dh_gencontrol
dh_md5sums
dh_builddeb
binary-arch: DH_OPTIONS=-a
binary-arch: build install
dh_testdir
dh_testroot
dh_installdocs
dh_installexamples
dh_installmenu
dh_installemacsen
dh_installcron
dh_installman
dh_installinfo
dh_installchangelogs
dh_strip $(NO_STRIP)
dh_link
dh_compress
dh_lintian
dh_fixperms
dh_installdeb
dh_shlibdeps
dh_gencontrol
dh_md5sums
dh_builddeb
binary: binary-indep binary-arch
.PHONY: build build-arch build-indep clean binary-indep binary-arch binary install
|
