File: Makefile-generic

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (302 lines) | stat: -rw-r--r-- 12,652 bytes parent folder | download
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
#; ACL2 Version 3.1 -- A Computational Logic for Applicative Common Lisp
#; Copyright (C) 2006  University of Texas at Austin

#; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
#; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTES-2-0.

#; This program is free software; you can redistribute it and/or modify
#; it under the terms of the GNU General Public License as published by
#; the Free Software Foundation; either version 2 of the License, or
#; (at your option) any later version.

#; This program is distributed in the hope that it will be useful,
#; but WITHOUT ANY WARRANTY; without even the implied warranty of
#; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
#; GNU General Public License for more details.

#; You should have received a copy of the GNU General Public License
#; along with this program; if not, write to the Free Software
#; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

#; Written by:  Matt Kaufmann               and J Strother Moore
#; email:       Kaufmann@cs.utexas.edu      and Moore@cs.utexas.edu
#; Department of Computer Sciences
#; University of Texas at Austin
#; Austin, TX 78712-1188 U.S.A.

#; Adapted from makefiles for IHS and data-structures library, which were
#; created by Bishop Brock.

#; NOTE:  Target "all" causes a recursive invocation of make with ACL2 set to
#; its current value.  These recursive invocations of make thus have ACL2 set
#; on the command line, which overrides any values of ACL2 set in those files.
#; This should not cause any problems unless you try to do something fancy; see
#; the comment for example just above target .exercises.cert in
#; books/case-studies/ivy/ivy-v2/ivy-sources/Makefile from the ACL2
#; distribution.

# Success can be determined by checking for the absence of the following string
# in the log;  "**CERTIFICATION FAILED**".

# We could probably arrange for the make process to stop as soon as
# certification fails, if there is a need.  If we do that, we should also
# arrange that the -k (or --keep_going) flag, as specified by the GNU make
# manual, avoids such stopping.

#################### Editable variables ####################

# The default command below prints runtime statistics for the certification.
# We normally inhibit most output during certification to speed up the proofs.
# Edit as necessary.

# The setting of ACL2 immediately below reflects an assumption about where this
# Makefile will be executed, namely, directly under books/.  This assumption
# can of course be overridden by specifying ACL2 on the command line, for
# example: make ACL2=/home/smith/saved_acl2.  Be sure to do this override on
# the command line rather than by editing the line below, because that edit
# will probably not suffice for overriding the assignment of ACL2 that is made
# in some books (namely, those not just one level past books/).

ACL2 ?= ../../saved_acl2

# Fix problem with sh on some Linux systems:
ifeq ($(OSTYPE),linux)
	SHELL = bash
endif
ifeq ($(OSTYPE),linux-gnu)
	SHELL = bash
endif

# Inhibit all output except the summary (which can be useful for tracking down problems).
# Set this to "" if you do want the output.

INHIBIT = (assign inhibit-output-lst (list (quote prove) (quote proof-tree) (quote warning) (quote observation) (quote event) (quote expansion)))

# Support for make dependencies:  should be a list of book names without
# the .lisp suffix.  Can be overridden on the command line or in a file
# that includes this file.

BOOKS = $(patsubst %.lisp, %, $(wildcard *.lisp))

#################### END of editable variables ####################

# We should really check that following is not empty.  It is the same as
# books, but with .cert suffixes.  This variable should not be overridden;
# it is computed as needed from BOOKS.

BOOKS_CERT   = $(patsubst %, %.cert, $(BOOKS))
BOOKS_FASL   = $(patsubst %, %.fasl, $(BOOKS))
BOOKS_FAS   = $(patsubst %, %.fas, $(BOOKS))
BOOKS_SPARCF = $(patsubst %, %.sparcf, $(BOOKS))
BOOKS_UFSL = $(patsubst %, %.ufsl, $(BOOKS))
BOOKS_DFSL = $(patsubst %, %.dfsl, $(BOOKS))
BOOKS_D64FSL = $(patsubst %, %.d64fsl, $(BOOKS))
BOOKS_X86F = $(patsubst %, %.x86f, $(BOOKS))
BOOKS_O      = $(patsubst %, %.o, $(BOOKS))

#  This tells make to expect `suffix rules' for these file suffixes.

.SUFFIXES: .cert .lisp

#  This rule tells how to get <book>.cert from <book>.lisp, either by running
#  ACL2 on the <book>.acl2 file (if it exists) or using the default command
#  to certify at ground zero.  Note that some Lisps execute (LP) upon startup
#  and some do not, and some (e.g., OpenMCL) might not even start in the ACL2
#  package, which can cause a problem if .acl2 files in our regressions suite
#  execute (LP) instead of (ACL2::LP).  We deal with these issues below.

.lisp.cert:
	@echo "Making `pwd`/$*.cert on `date`"
	@rm -f $*.cert
	@echo '(acl2::value :q)' > workxxx.$(*F)
	@echo '(in-package "ACL2")' >> workxxx.$(*F)
	@echo '(acl2::lp)' >> workxxx.$(*F)
	@echo '$(INHIBIT)' >> workxxx.$(*F)
	@if [ -f $*.acl2 ] ; \
	then \
	  cat $*.acl2 >> workxxx.$(*F) ; \
	elif [ -f cert.acl2 ] ; \
	then \
	  cat cert.acl2 >> workxxx.$(*F) ; \
	  echo '(certify-book "$*" ? $(COMPILE_FLG))' >> workxxx.$(*F) ; \
	else \
	  echo '(certify-book! "$*" 0 $(COMPILE_FLG))' >> workxxx.$(*F) ; \
	fi
	@echo '(acl2::value :q)' >> workxxx.$(*F) ; \
	echo '(acl2::exit-lisp)' >> workxxx.$(*F) ; \
	$(ACL2) < workxxx.$(*F) > $*.out
	@rm -f workxxx.$(*F)
	@((test -f $<) && (ls -al $*.cert)) || ($(MAKE) -s --no-print-directory FAILED FAILED_BOOK=`pwd`/$*.lisp)
# The following code can replace the line just above.  However, it is a bit
# complicated by our having seen sh on Sun/Solaris 5.9 fail to recognize -nt,
# which is this code uses csh instead of sh if possible.  At any rate, the test
# on file dates seems unnecessary since we remove the .cert file immediately
# upon entering this target.
#	@if [ `which csh` ] ; then \
#	csh -c "((test -f $< -a ! $< -nt $@ ) && (ls -al $*.cert))" || ($(MAKE) -s --no-print-directory FAILED FAILED_BOOK=`pwd`/$*.lisp) ; \
#	else \
#	((test -f $< -a ! $< -nt $@ ) && (ls -al $*.cert)) || ($(MAKE) -s --no-print-directory FAILED FAILED_BOOK=`pwd`/$*.lisp) ; \
#	fi

#  This rule certifies every book in BOOKS.  If the dependencies are set up
#  correctly then the order of the books in BOOKS won't matter.

all:
	echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f Makefile $(BOOKS_CERT) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

# The following rules are useful when books have been certified in one lisp,
# but we would also like their compiled files to exist in the other lisp.

FAILED:
	@echo "**CERTIFICATION FAILED** for $(FAILED_BOOK)" ; exit 1

.PHONY: FAILED

fasl:
	echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f Makefile $(BOOKS_FASL) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.fasl: %.cert
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.fasl,%,$(@))" :load-compiled-file :comp))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

fas:
	echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f Makefile $(BOOKS_FAS) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

# For CLISP, apparently only the first echoed form is evaluated.  So do not give multiple forms.
%.fas: %.cert
	echo '(ld `((include-book "$(patsubst %.fas,%,$(@))" :load-compiled-file :comp)))' | $(ACL2)

sparcf:
	echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f Makefile $(BOOKS_SPARCF) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.sparcf: %.cert
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.sparcf,%,$(@))" :load-compiled-file :comp))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

ufsl:
	echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f Makefile $(BOOKS_UFSL) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.ufsl: %.cert
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.ufsl,%,$(@))" :load-compiled-file :comp))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

x86f:
	echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f Makefile $(BOOKS_X86F) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.x86f: %.cert
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.x86f,%,$(@))" :load-compiled-file :comp))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

dfsl:
	echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f Makefile $(BOOKS_DFSL) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.dfsl: %.cert
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.dfsl,%,$(@))" :load-compiled-file :comp))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

d64fsl:
	echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f Makefile $(BOOKS_D64FSL) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.d64fsl: %.cert
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.d64fsl,%,$(@))" :load-compiled-file :comp))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

o:
	echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f Makefile $(BOOKS_O) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.o: %.cert
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.o,%,$(@))" :load-compiled-file :comp))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

# The dependencies rule prints make dependency commands to the screen.  The basic
# strategy is to look for include-book commands, and to prefix appropriately
# "$(ACL2_SYSTEM_BOOKS)" when :dir :system is specified.  Thus, if :dir :system is
# specified then a common Makefile header in a books directory could be as
# follows (just strip off the leading "# " on each line).

# ----------------------------------------------------------------------
# # The following variable should represent the ACL2 source directory.
# # It is the only variable in this Makefile that may need to be edited.
# ACL2_SRC = ../../../../../..

# ACL2_SYSTEM_BOOKS = $(ACL2_SRC)/books
# include $(ACL2_SYSTEM_BOOKS)/Makefile-generic
# ACL2 = $(ACL2_SRC)/saved_acl2
# ----------------------------------------------------------------------

# Here are variables that represent egrep commands for finding include-book
# forms, as well as sed commands for modifying those include-book forms to
# generate dependency lines.

# Grep commands to rule out :dir :system:
ACL2_NON_DIR            = egrep -i -v ':dir[ \t]*:system'

# Grep commands for include-book and ld forms withOUT :dir :system:
ACL2_EGREP_CMD          = egrep -i '^[^;]*include-book[ \t]*\".*\"' $$book.lisp | $(ACL2_NON_DIR)
ACL2_EGREP_CMD_ACL2     = $(subst book.lisp,book.acl2,$(ACL2_EGREP_CMD))
ACL2_EGREP_CMD_CERT     = $(subst $$book.lisp,cert.acl2,$(ACL2_EGREP_CMD))
ACL2_EGREP_CMD_ACL2_LD  = egrep -i '^[^;]*\(ld[ \t]*\".*\"' $$book.acl2 | $(ACL2_NON_DIR)
ACL2_EGREP_CMD_CERT_LD  = egrep -i '^[^;]*\(ld[ \t]*\".*\"' cert.acl2 | $(ACL2_NON_DIR)

# Grep commands for include-book and ld forms WITH :dir :system (need a file argument):
ACL2_EGREP_CMD_DIR      = egrep -i '^[^;]*include-book[ \t]*\".*\"[ \t]*:dir[ \t]*:system'
ACL2_EGREP_CMD_DIR_LD   = egrep -i '^[^;]*\(ld[ \t]*\".*\"[ \t]*:dir[ \t]*:system'

# Sed commands for transforming above egrep results into a dependency line:
ACL2_SED_CMD            = sed "s/[^\"]*\"/$$book.cert: /" | sed 's/".*/.cert/'
ACL2_SED_CMD_LD         = sed "s/[^\"]*\"/$$book.cert: /" | sed 's/".*//'
ACL2_SED_CMD_DIR        = $(subst book.cert: ,book.cert: $$\(ACL2_SYSTEM_BOOKS)\/,$(ACL2_SED_CMD))
ACL2_SED_CMD_DIR_LD     = $(subst book.cert: ,book.cert: $$\(ACL2_SYSTEM_BOOKS)\/,$(ACL2_SED_CMD_LD))

# To comment out a line:
ACL2_SED_CMD_COMMENT    = sed "s/^/\# /"

# See comments above.
dependencies: 
	@for book in $(BOOKS) ; \
	do \
	echo "" ;  echo "$$book.cert: $$book.lisp" ; \
	$(ACL2_EGREP_CMD) | $(ACL2_SED_CMD) ;\
	$(ACL2_EGREP_CMD_DIR) $$book.lisp | $(ACL2_SED_CMD_DIR) | $(ACL2_SED_CMD_COMMENT) ;\
	if [ -f $$book.acl2 ]; then \
	echo "$$book.cert: $$book.acl2" ; \
	$(ACL2_EGREP_CMD_ACL2) | $(ACL2_SED_CMD) ;\
	$(ACL2_EGREP_CMD_ACL2_LD) | $(ACL2_SED_CMD_LD) ;\
	$(ACL2_EGREP_CMD_DIR) $$book.acl2 | $(ACL2_SED_CMD_DIR) | $(ACL2_SED_CMD_COMMENT) ;\
	$(ACL2_EGREP_CMD_DIR_LD) $$book.acl2 | $(ACL2_SED_CMD_DIR_LD) | $(ACL2_SED_CMD_COMMENT) ;\
	elif [ -f cert.acl2 ]; then \
	echo "$$book.cert: cert.acl2" ; \
	$(ACL2_EGREP_CMD_CERT) | $(ACL2_SED_CMD) ;\
	$(ACL2_EGREP_CMD_CERT_LD) | $(ACL2_SED_CMD_LD) ;\
	$(ACL2_EGREP_CMD_DIR) cert.acl2 | $(ACL2_SED_CMD_DIR) | $(ACL2_SED_CMD_COMMENT) ;\
	$(ACL2_EGREP_CMD_DIR_LD) cert.acl2 | $(ACL2_SED_CMD_DIR_LD) | $(ACL2_SED_CMD_COMMENT) ;\
	fi ; \
	done

clean:
	rm -f *.cert
	rm -f *.h
	rm -f *.c
	rm -f *.o
	rm -f *.sbin
	rm -f *.lbin
	rm -f *.fasl
	rm -f *.ufsl
	rm -f *.pfsl
	rm -f *.dfsl
	rm -f *.d64fsl
	rm -f *.bin
	rm -f *.sparcf
	rm -f *.axpf
	rm -f *.x86f
	rm -f *.ppcf
	rm -f *.fas
	rm -f *.lib
	rm -f *.out
	rm -f *.date
	rm -f *.log
	rm -f TMP*.*
	rm -f *@expansion.lsp
	rm -f workxxx*