-
Notifications
You must be signed in to change notification settings - Fork 106
/
Copy pathGNUmakefile
993 lines (891 loc) · 38.7 KB
/
GNUmakefile
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
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
# ACL2 Version 8.6 -- A Computational Logic for Applicative Common Lisp
# Copyright (C) 2025, Regents of the University of Texas
# 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 LICENSE file distributed with ACL2.
# 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
# LICENSE for more details.
# Written by: Matt Kaufmann and J Strother Moore
# email: Kaufmann@cs.utexas.edu and Moore@cs.utexas.edu
# Department of Computer Science
# University of Texas at Austin
# Austin, TX 78712 U.S.A.
# Example invocations for users:
# make ; Same as make all
# make all ; Same as make large, but also makes TAGS-acl2-doc if
# ; TAGS_ACL2_DOC is non-empty and not SKIP. Most output
# ; goes to file make.log (customizable with
# ; ACL2_MAKE_LOG), including output from both large and
# ; TAGS-acl2-doc.
# make large ; Build ${PREFIXsaved_acl2} from scratch. Most output
# ; goes to file make.log (customizable with
# ; ACL2_MAKE_LOG).
# make TAGS-acl2-doc ; Build tags-table for books (used by acl2-doc browser)
# make clean ; Remove all generated files in top-level directory and doc/
# make clean-all ; Same as above
# make distclean ; Same as above
# make clean-lite ; Same as clean-all, except do not delete *saved_acl2*
# ; or doc.lisp.backup
# make update ; Same as make large, except that if the desired
# ; executable is up-to-date with respect to the
# ; ACL2 sources, then do nothing. See warning
# ; next to `update' target, below.
# make LISP=cl PREFIX=allegro-
# make TAGS ; Create tags table, handy for viewing sources with emacs.
# make TAGS! ; Same as TAGS, except forces a rebuild of TAGS.
# make regression
# ; Certify most community books.
# make regression ACL2=xxx
# ; Same as make regression, but use xxx as ACL2, which
# ; should either be an absolute filename or a command on
# ; one's path.
# make regression ACL2_CUSTOMIZATION=xxx
# ; Same as make regression, but use xxx as the
# ; ACL2 customization file (see :DOC acl2-customization).
# ; In particular, this is useful for certifying
# ; the books in the regression suite using
# ; waterfall parallelism (requires the
# ; experimental extension ACL2(p) of ACL2); see
# ; file acl2-customization-files/README.
# make regression-everything
# ; Same as make regression-everything in books/Makefile;
# ; certifies more than the regression target.
# make clean-books ; Remove certificate files, object files, log files,
# ; debris, ..., created by `make basic',
# ; `make regression', etc.
###############################################################################
# NOTE: Perhaps only implementors should read below.
# Example invocations for implementors:
# NOTE: Make completely recompiles, initializes and saves.
# make full ; A complete recompilation whether needed or not.
8000
# make full init ; Completely recompile, initialize and save.
# make full-meter init ; Completely recompile with meters, init and save.
# make init ; Just build full-size ${PREFIXsaved_acl2}.
# make check-sum ; Call only after ACL2 is completely compiled.
# make full LISP=lucid PREFIX=lucid- ; makes acl2 in Lucid
# make full LISP=cl PREFIX=allegro- ; makes acl2 in allegro
# make full LISP=lispworks PREFIX=lispworks- ; makes acl2 in lispworks
# make copy-distribution DIR=/stage/ftp/pub/moore/acl2/v2-9/acl2-sources
# ; copies all of acl2 plus books, doc, etc., to the named
# ; directory, as for compiling on another architecture or
# ; moving to the ftp site.
# ; Precondition:
# ; The named directory must not already exist; if it
# ; does, a harmless error is caused.
# make DOC ; Build xdoc manual and rebuild source file doc.lisp
# make clean-doc ; Remove files created by make DOC
# make proofs ; Assuming sources are compiled, initialize without skipping
# ; proofs during pass 2. Does not save an image. Uses same
# ; flags used to build full-size image.
# Metering: If the currently compiled version is unmetered and you
# wish it metered, the fastest thing to do is to (push :acl2-metering
# *features*) and then yank in and recompile just those definitions
# that mention acl2-metering. However, if you would like to install
# metering as part of a system-wide recompilation, use the full-meter
# option below. If you want to get rid of the metering in the
# compiled code, do make full.
###############################################################################
# Avoid loading the ACL2 customization file. This is already done by
# the books build system; however we need this for "make DOC" and
# perhaps other targets.
export ACL2_CUSTOMIZATION ?= NONE
# Log file for builds
export ACL2_MAKE_LOG ?= make.log
# Avoid escape characters in regression log:
export CERT_PL_NO_COLOR ?= t
# Always make it possible to gather timing statistics after a regression.
export TIME_CERT = yes
LISP = ccl
DIR = /tmp
# The following is intended to provide the current working directory
# on Cygwin/Windows.
ifneq (,$(findstring CYGWIN, $(shell uname)))
ACL2_WD := $(shell cygpath -m `pwd`)
else
ACL2_WD := $(shell pwd)
endif
# The build of saved_acl2 may succeed even if the directory name has
# spaces, but book certification will almost surely fail, so we
# disallow such a build. Comment out the three lines below if you
# want to take your chances nonetheless!
ifneq (,$(word 2, $(ACL2_WD)))
$(error Illegal ACL2 build directory (contains a space): $(ACL2_WD)/)
endif
# The variable ACL2_REAL should be defined for the non-standard
# version and not for the standard version. Non-standard ACL2 images
# will include the suffix "r", for example saved_acl2r rather than
# saved_acl2. Variables ACL2_PAR, ACL2_DEVEL, and ACL2_WAG (for
# feature write-arithmetic-goals) are similar (with suffixes p, d, and
# w, resp., rather than r), but for versions that respectively are
# parallel or (for implementors only) have features :acl2-devel or
# :write-arithmetic-goals, for special builds pertaining to
# guard-verified functions or writing out arithmetic lemma data to
# ~/write-arithmetic-goals.lisp.
# DO NOT EDIT ACL2_SUFFIX! Edit the above-mentioned four variables instead.
ACL2_SUFFIX :=
ifdef ACL2_PAR
ACL2_SUFFIX := $(ACL2_SUFFIX)p
endif
ifdef ACL2_WAG
ACL2_SUFFIX := $(ACL2_SUFFIX)w
endif
ifdef ACL2_DEVEL
ACL2_SUFFIX := $(ACL2_SUFFIX)d
endif
ifdef ACL2_REAL
ACL2_SUFFIX := $(ACL2_SUFFIX)r
endif
# The user may define PREFIX; otherwise it is implicitly the empty string.
PREFIX :=
PREFIXsaved_acl2 := ${PREFIX}saved_acl2${ACL2_SUFFIX}
PREFIXosaved_acl2 := ${PREFIX}osaved_acl2${ACL2_SUFFIX}
ACL2 ?= $(ACL2_WD)/${PREFIXsaved_acl2}
# One may define ACL2_SAFETY and/or (only useful for CCL) ACL2_STACK_ACCESS
# to provide a safety or :stack-access setting. We recommend
# ACL2_SAFETY = 3
# for careful error checking. This can cause significant slowdown and for
# some Lisp implementations, the regression might not even complete. For
# CCL we have had success with safety 3.
# NOTE: The use of ACL2_STACK_ACCESS relies on recognition by CCL of the
# :stack-access keyword for optimize expressions, hence will only have
# effect for CCL versions starting with 16678.
ACL2_SAFETY =
ACL2_STACK_ACCESS =
# It can be useful to set the space to other than its default (in
# other than CMUCL) of 0. In particular, we have seen improved
# floating-point performance with SBCL.
ACL2_SPACE =
# Set ACL2_COMPILER_DISABLED, say with ACL2_COMPILER_DISABLED=t, to
# build the image with (SET-COMPILER-ENABLED NIL STATE), thus
# disabling use of the compiler for certify-book and include-book; see
# :DOC compilation. This is generally not necessary, but for the use
# of some books employing raw Lisp code it could, on rare occasion, be
# useful; and for SBCL and CCL (as of this writing, May 2010),
# reasonably harmless other than to lose a bit of speed when including
# books with many complex defun forms.
ACL2_COMPILER_DISABLED =
# See *acl2-egc-on* for an explanation of the following variable.
ACL2_EGC_ON =
# The following supplies a value for *acl2-exit-lisp-hook*, which
# should be a symbol in the "COMMON-LISP-USER" package. For example,
# for CCL consider:
# make ACL2_EXIT_LISP_HOOK='acl2-exit-lisp-ccl-report'.
ACL2_EXIT_LISP_HOOK =
# The following is not advertised. It allows more symbol allocation
# when ACL2 package is created; if specified, its value should be a
# number to supply for the :size argument of defpackage. For example,
# 3000000 has been found a useful such value for a use of the HONS
# version of ACL2 built on CCL on a 64-bit machine.
ACL2_SIZE =
# The following causes the calls of make that use it to continue past
# errors. Delete -k if you want to stop at first error and return
# non-zero exit status in that case; or, instead of editing the line
# below, supply ACL2_IGNORE='' on the make command line. Formerly we
# used -i; if you prefer that, use ACL2_IGNORE=-i on the command line.
# Note however that the GNU make manual
# (http://www.gnu.org/software/make/manual/make.html, May 2013) says
# that -i is "obsolete".
ACL2_IGNORE ?= -k
# The order of the files below is unimportant.
# NOTE: We deliberately exclude doc.lisp, which does not contribute to
# proclaiming or TAGS.
sources := axioms.lisp memoize.lisp hons.lisp\
boot-strap-pass-2-a.lisp boot-strap-pass-2-b.lisp\
basis-a.lisp basis-b.lisp parallel.lisp translate.lisp\
type-set-a.lisp linear-a.lisp\
type-set-b.lisp linear-b.lisp\
non-linear.lisp tau.lisp\
rewrite.lisp simplify.lisp bdd.lisp\
other-processes.lisp induct.lisp prove.lisp\
proof-builder-a.lisp history-management.lisp defuns.lisp\
defthm.lisp other-events.lisp ld.lisp proof-builder-b.lisp\
proof-builder-pkg.lisp float-a.lisp float-b.lisp float-raw.lisp\
apply-raw.lisp interface-raw.lisp\
serialize.lisp serialize-raw.lisp\
defpkgs.lisp\
apply-prim.lisp apply-constraints.lisp apply.lisp
sources := $(sources) hons-raw.lisp memoize-raw.lisp
ifdef ACL2_PAR
sources := $(sources) multi-threading-raw.lisp parallel-raw.lisp futures-raw.lisp
endif
# No change to sources for ACL2_DEVEL or ACL2_WAG
sources_extra := GNUmakefile acl2-characters doc.lisp \
acl2.lisp acl2-check.lisp acl2-fns.lisp acl2-init.lisp \
akcl-acl2-trace.lisp allegro-acl2-trace.lisp openmcl-acl2-trace.lisp
ACL2_DEPS := $(sources) $(sources_extra)
ACL2_SAVED ?= custom-saved_acl2${ACL2_SUFFIX}
ACL2_SAVED_ARGS ?= "Saved with additions from $(ACL2_CUSTOMIZATION)"
# Top (default) target:
.PHONY: all
all: large
ifneq ($(TAGS_ACL2_DOC),)
ifneq ($(TAGS_ACL2_DOC),SKIP)
ifeq ($(ACL2_MAKE_LOG),NONE)
@$(MAKE) TAGS-acl2-doc
else
@echo -n Making TAGS-acl2-doc...
@$(MAKE) TAGS-acl2-doc >> "$(ACL2_MAKE_LOG)" 2>&1 || (echo "\nERROR: See $(ACL2_MAKE_LOG)." ; exit 1)
@echo " done."
endif
endif
endif
# We run target update_books_build_info when ACL2 is built, to update
# certain files in books/build/, in particular
# books/build/Makefile-features and books/build/*.certdep files. Note
# that we do this every time ACL2 is built, not merely when the
# sources have changed, because variables ACL2_HOST_LISP and
# ACL2_COMP_EXT are written to books/build/Makefile-features. (Of
# course, one might use cert.pl on a saved_acl2 previously built in
# the same directory on a different host Lisp. But this approach is
# probably much better than nothing, and the target
# update_books_build_info is only relevant for using cert.pl, not
# make, as books/GNUmakefile rebuilds books/build/Makefile-features
# every time it is invoked.)
.PHONY: update_books_build_info
update_books_build_info:
@if [ ! -d books/build ] ; then \
echo "ERROR: Directory, books/build/ does not exist." ;\
exit 1 ;\
fi
@export ACL2=$(ACL2) ; export STARTJOB=$(SHELL) ; cd books/build ; (./features.sh 2>&1) > features.out
# The following target is intended only for when $(ACL2_MAKE_LOG) is
# not NONE.
.PHONY: set-up-log
set-up-log:
@if [ -f "$(ACL2_MAKE_LOG)".bak ] ; then \
rm -f "$(ACL2_MAKE_LOG)".bak ; \
fi
@if [ -f "$(ACL2_MAKE_LOG)" ] ; then \
cp -p "$(ACL2_MAKE_LOG)" "$(ACL2_MAKE_LOG)".bak ; \
fi
@echo "Preparing to build ${PREFIXsaved_acl2} (log file $(ACL2_MAKE_LOG))."
@if [ -f "$(ACL2_MAKE_LOG)" ] && [ "`(tail -1 "$(ACL2_MAKE_LOG)" 2>&1)`" = "Preparing to build ${PREFIXsaved_acl2} (log file $(ACL2_MAKE_LOG))." ]; then \
echo "" ;\
>&2 echo '** ABORTING: Shell output has been redirected to the file' $(ACL2_MAKE_LOG) . ;\
>&2 echo ' But this is illegal, because this "make" invocation' ;\
>&2 echo ' is already directing its output to that same file.' ;\
>&2 echo ' To change where this "make" invocation directs its output,' ;\
>&2 echo ' you may set "make" variable ACL2_MAKE_LOG to that desired' ;\
>&2 echo ' filename, but you are advised to consider simply avoiding' ;\
>&2 echo ' the redirection of shell output to $(ACL2_MAKE_LOG).' ;\
exit 1 ;\
fi
# Build tags table for acl2-doc, with ACL2 topics first.
TAGS-acl2-doc: $(ACL2_DEPS)
rm -f TAGS-acl2-doc
etags -o TAGS-acl2-doc -- *.lisp
find books -name '*.lisp' -print | (time xargs etags -o TAGS-acl2-doc --append --)
# The targets acl2r and acl2r.lisp were originally created to support
# ACL2(r) builds. It has more uses than that now.
.PHONY: acl2r
acl2r:
@rm -f acl2r.lisp
@$(MAKE) --no-print-directory acl2r.lisp
acl2r.lisp:
# The various "startup" code below can be loaded as a first step in
# building ACL2. The first is actually always done in modern ACL2 builds.
@echo "" > $@
@if [ "$(ACL2_COMPILER_DISABLED)" != "" ] ; then \
echo '(DEFPARAMETER *ACL2-COMPILER-ENABLED* NIL)' >> $@ ;\
fi
@if [ "$(ACL2_EGC_ON)" != "" ] ; then \
echo '(DEFPARAMETER *ACL2-EGC-ON* $(ACL2_EGC_ON))' >> $@ ;\
fi
# The next startup is something for developers only. It is useful
# from time to time to check the arrangement that certain source
# functions come up as guard-verified. See :DOC
# verify-guards-for-system-functions.
@if [ "$(ACL2_DEVEL)" != "" ] ; then \
echo '(or (member :acl2-devel *features*) (push :acl2-devel *features*))' >> $@ ;\
fi
# WARNING: The next two startups are for building ACL2(p) and ACL2(r),
# respectively.
@if [ "$(ACL2_PAR)" != "" ] ; then \
echo '(or (member :acl2-par *features*) (push :acl2-par *features*))' >> $@ ;\
fi
@if [ "$(ACL2_REAL)" != "" ] ; then \
echo '(or (member :non-standard-analysis *features*) (push :non-standard-analysis *features*))' >> $@ ;\
fi
# WARNING: The startups below should be used with care. Don't use
# them unless you know what you are doing! They are not officially
# supported.
@if [ "$(ACL2_WAG)" != "" ] ; then \
mv -f ~/write-arithmetic-goals.lisp.old ; \
mv -f ~/write-arithmetic-goals.lisp ~/write-arithmetic-goals.lisp.old ; \
echo '(or (member :write-arithmetic-goals *features*) (push :write-arithmetic-goals *features*))' >> $@ ;\
fi
@if [ "$(ACL2_SAFETY)" != "" ] ; then \
echo "(defparameter *acl2-safety* $(ACL2_SAFETY))" >> $@ ;\
fi
@if [ "$(ACL2_SPACE)" != "" ] ; then \
echo "(defparameter *acl2-space* $(ACL2_SPACE))" >> $@ ;\
fi
@if [ "$(ACL2_STACK_ACCESS)" != "" ] ; then \
echo "(defparameter *acl2-stack-access* $(ACL2_STACK_ACCESS))" >> $@ ;\
fi
@if [ "$(ACL2_SIZE)" != "" ] ; then \
echo '(or (find-package "ACL2") (#+(and gcl (not ansi-cl)) defpackage:defpackage #-(and gcl (not ansi-cl)) defpackage "ACL2" (:size $(ACL2_SIZE)) (:use)))' >> $@ ;\
fi
@if [ "$(ACL2_EXIT_LISP_HOOK)" != "" ] ; then \
echo '(DEFPARAMETER *ACL2-EXIT-LISP-HOOK* (QUOTE $(ACL2_EXIT_LISP_HOOK)))' >> $@ ;\
fi
# WARNING: The startup below should be used with even more care than
# those warned about above, since it allows you to put anything you
# like into acl2r.lisp, whether reasonable or not! Example:
# make ACL2_STARTUP_EXTRA='(push :acl2-save-unnormalized-bodies *features*)'
@if [ "$(ACL2_STARTUP_EXTRA)" != "" ] ; then \
echo '$(ACL2_STARTUP_EXTRA)' >> $@ ;\
fi
.PHONY: chmod_image
chmod_image:
if [ -f ${PREFIXsaved_acl2} ]; then \
chmod 775 ${PREFIXsaved_acl2} ;\
fi
.PHONY: do_saved
# Note: We removed line "chmod g+s saved" before the second chmod below, as it
# was causing errors in at least one environment, and instead did final chmod
# to 666 instead of 664 in case files in saved/ wind up in an unexpected group.
do_saved:
rm -fr saved
mkdir saved
chmod 775 saved
cp *.lisp acl2-characters GNUmakefile saved/
chmod 666 saved/*
# Keep the use of :COMPILED/:COMPILE-SKIPPED below in sync with ACL2
# source function note-compile-ok.
.PHONY: check_compile_ok
check_compile_ok:
@if [ ! -f acl2-status.txt ] ; then \
echo 'Compile FAILED: file acl2-status.txt is missing.' ; \
exit 1 ; \
fi
@if [ `cat acl2-status.txt` != :COMPILED ] && [ `cat acl2-status.txt` != :COMPILE-SKIPPED ] ; then \
echo 'Compile FAILED: acl2-status.txt should contain :COMPILED or (for some Lisps) :COMPILE-SKIPPED.' ; \
exit 1 ; \
fi
# Keep the use of :INITIALIZED below in sync with ACL2 source function
# initialize-acl2.
.PHONY: check_init_ok
check_init_ok:
@if [ ! -f acl2-status.txt ] ; then \
echo 'Initialization FAILED: file acl2-status.txt is missing.' ; \
exit 1 ; \
fi
@if [ `cat acl2-status.txt` != :INITIALIZED ] ; then \
echo 'Initialization FAILED: acl2-status.txt should contain :INITIALIZED.' ; \
exit 1 ; \
fi
@echo "Initialization SUCCEEDED."
# The following target should only be used when the compiled files are
# ready to use and, if needed, so is acl2-proclaims.lisp.
.PHONY: compile-ok
compile-ok:
date
rm -f workxxx
echo '(load "init.lisp")' > workxxx
echo '(acl2::note-compile-ok)' >> workxxx
echo '(acl2::exit-lisp)' >> workxxx
${LISP} < workxxx
rm -f workxxx
.PHONY: check-sum
check-sum:
date
rm -f workxxx
echo '(load "init.lisp") (acl2)' > workxxx
echo '(acl2::make-check-sum-file)' >> workxxx
echo '(acl2::exit-lisp)' >> workxxx
${LISP} < workxxx
rm -f workxxx
.PHONY: full
full: TAGS
$(MAKE) compile
rm -f acl2-proclaims.lisp
# The following two forms should do nothing, and quickly, if
# *do-proclaims* is nil.
$(MAKE) acl2-proclaims.lisp
$(MAKE) compile USE_ACL2_PROCLAIMS=t
.PHONY: compile
compile:
rm -f workxxx
echo '(load "init.lisp")' > workxxx
echo '(acl2::compile-acl2 $(USE_ACL2_PROCLAIMS))' >> workxxx
echo '(acl2::exit-lisp)' >> workxxx
${LISP} < workxxx
@$(MAKE) check_compile_ok
.PHONY: copy-distribution
copy-distribution: acl2r.lisp
# WARNING: Execute this from an ACL2 source directory.
# You must manually rm -r ${DIR} before this or it will fail without doing
# any damage.
# Note that below, /projects/acl2/ is not used, because this directory must
# match what lisp returns from truename.
rm -f workxxx
rm -f workyyy
echo '(load "init.lisp")' > workxxx
echo '(acl2::copy-distribution "workyyy" "${CURDIR}" "${DIR}")' >> workxxx
echo '(acl2::exit-lisp)' >> workxxx
${LISP} < workxxx
chmod 777 workyyy
./workyyy
rm -f workxxx
rm -f workyyy
# You can replace the block of code below if etags doesn't exist on your system, by
# removing "#" on the two lines just below and commenting out the block below
# them. However, since Lisp function make-tags deals with this issue, such a
# change is probably not necessary.
#TAGS:
# @echo 'Skipping building of a tags table.'
# We build acl2r.lisp so that we build ACL2(r) or ACL2(p), for example.
TAGS: $(ACL2_DEPS)
$(MAKE) acl2r
rm -f TAGS
rm -f workxxx
echo '(load "init.lisp")' > workxxx
echo '(acl2::make-tags)' >> workxxx
echo '(acl2::exit-lisp)' >> workxxx
${LISP} < workxxx
rm -f workxxx
if [ -f TAGS ] ; then chmod 644 TAGS ; fi
# THE FOLLOWING TARGET IS DEPRECATED, since TAGS now depends on $(ACL2_DEPS).
# The following remakes TAGS even if TAGS is up to date. This target can be
# useful when building a parallel version after a normal version, or
# vice-versa.
.PHONY: TAGS!
TAGS!: acl2r
rm -f TAGS
$(MAKE) TAGS
.PHONY: move-to-old
move-to-old:
if [ -f ${PREFIXsaved_acl2} ] && [ -f ${PREFIXsaved_acl2}.${LISPEXT} ]; then \
echo "Moving " ${PREFIXsaved_acl2}.${LISPEXT} " to ${PREFIXosaved_acl2}.${LISPEXT}"; \
mv -f ${PREFIXsaved_acl2}.${LISPEXT} ${PREFIXosaved_acl2}.${LISPEXT}; \
cat ${PREFIXsaved_acl2} | sed -e 's/saved_acl2${ACL2_SUFFIX}.${LISPEXT}$$/osaved_acl2${ACL2_SUFFIX}.${LISPEXT}/' > ${PREFIXosaved_acl2} ;\
chmod 775 ${PREFIXosaved_acl2} ;\
rm -f ${PREFIXsaved_acl2} ; fi
.PHONY: move-new
move-new:
if [ -f nsaved_acl2.${LISPEXT} ]; then \
mv -f nsaved_acl2.${LISPEXT} ${PREFIXsaved_acl2}.${LISPEXT} ; fi
# See the Essay on Proclaiming in source file acl2-fns.lisp.
acl2-proclaims.lisp: ${sources}
rm -f acl2-proclaims.lisp
rm -f workxxx
rm -f worklispext
echo '(load "init.lisp")' > workxxx
echo '(in-package "ACL2")' >> workxxx
echo '(generate-acl2-proclaims)' >> workxxx
echo '(exit-lisp)' >> workxxx
${LISP} < workxxx
[ -f acl2-proclaims.lisp ]
.PHONY: init
init: acl2-proclaims.lisp
# Note: If you believe that compilation is up-to-date, do
# make compile-ok init
# rather than
# make init.
rm -f workxxx
rm -f worklispext
echo -n "" >> ${PREFIXosaved_acl2}
rm -f ${PREFIXosaved_acl2}
echo '(load "init.lisp")' > workxxx
echo '(in-package "ACL2")' >> workxxx
echo '(save-acl2 (quote (initialize-acl2 (quote include-book))) "${PREFIXsaved_acl2}")' >> workxxx
echo '(exit-lisp)' >> workxxx
${LISP} < workxxx
@$(MAKE) check_init_ok
# Move to old.
if [ -f worklispext ]; then $(MAKE) move-to-old LISPEXT=`cat worklispext` ;\
elif [ -f ${PREFIXsaved_acl2} ]; then \
mv -f ${PREFIXsaved_acl2} ${PREFIXosaved_acl2} ;\
else \
touch ${PREFIXsaved_acl2} ;\
mv -f ${PREFIXsaved_acl2} ${PREFIXosaved_acl2} ;\
fi
# End of move to old.
# Move new into position.
mv -f nsaved_acl2 ${PREFIXsaved_acl2}
# For Allegro 5.0 and later and cmulisp, only:
if [ -f worklispext ]; then $(MAKE) move-new LISPEXT=`cat worklispext` ; fi
# End of move new into position.
rm -f worklispext
rm -f workxxx
$(MAKE) do_saved
rm -f workxxx
$(MAKE) chmod_image
@echo "Successfully built $(ACL2_WD)/${PREFIXsaved_acl2}."
# The following "proofs" target assumes that files for the specified LISP have
# been compiled. We use :load-acl2-proclaims nil so that we don't
# have to worry about perhaps having wiped out acl2-proclaims.lisp
# since the time we compiled for the given Lisp.
.PHONY: proofs
proofs: compile-ok
rm -f workxxx
echo '(load "init.lisp")' > workxxx
echo '(acl2::load-acl2 :load-acl2-proclaims nil)' >> workxxx
echo '(acl2::initialize-acl2 nil)' >> workxxx
echo '(acl2::exit-lisp)' >> workxxx
${LISP} < workxxx
@$(MAKE) check_init_ok
rm -f workxxx
.PHONY: DOC acl2-manual check-acl2-exports check-books
check-books:
@if [ ! -d books ] ; then \
echo "ERROR: The system books directory, books/, does not exist." ;\
exit 1 ;\
fi
@echo ACL2_WD is $(ACL2_WD)
@echo ACL2 is $(ACL2)
@uname -a
# The next target, DOC, is the target that should generally be used
# for rebuilding the ACL2 User's Manual.
# WARNING: Sub-targets below have their own warnings!
# WARNING: We suggest that you supply ACL2=, e.g., make DOC
# ACL2=/u/acl2/saved_acl2. Otherwise parts of the build might use
# copies of ACL2 that surprise you. (It seems awkward to pass
# ACL2 through recursive calls of make so we leave this to the
# user.)
# WARNING: even though this target may rebuild doc.lisp, that will not
# update the documentation for the :DOC command at the terminal, of
# course; for that, you'll need to rebuild ACL2.
DOC: acl2-manual STATS check-books
cd books ; rm -f system/doc/render-doc.cert system/doc/rendered-doc.lsp
rm -f doc/home-page.html
$(MAKE) update-doc.lisp doc/home-page.html
check-acl2-exports: check-books
cd books ; rm -f misc/check-acl2-exports.cert ; $(MAKE) ACL2=$(ACL2) misc/check-acl2-exports.cert
# We remove doc/HTML before rebuilding it, in order to make sure that
# it is up to date. We could do that removal in doc/create-doc
# instead, but this way create-doc provides an interface that makes
# sense for most users, where the sources for the HTML/ files will not
# be changing. Still, we expect that doc/HTML is the main way people
# will update the home page
# WARNING: This target might be up to date even if the manual is out
# of date with respect to books/system/doc/acl2-doc.lisp. Consider
# using the DOC target instead.
doc/home-page.html: doc/home-page.lisp
cd doc ; rm -rf HTML ; ./create-doc 2>&1 create-doc.out
# The following will implicitly use ACL2=acl2 unless ACL2 is set.
# Note that books/system/doc/acl2-manual.lisp ends in a call of
# xdoc::save that populates doc/manual/ (not under books/).
acl2-manual: check-books
rm -rf doc/manual books/system/doc/acl2-manual.cert
cd books ; $(MAKE) USE_QUICKLISP=1 system/doc/acl2-manual.cert
rm -rf doc/manual/download/*
# WARNING: The dependency list just below isn't complete, since it
# doesn't consider what _those_ files depend on.
# WARNING: even though this target may rebuild doc.lisp, that will not
# update the documentation for the :DOC command at the terminal, of
# course; for that, you'll need to rebuild ACL2.
# NOTE: We copy books/system/doc/rendered-doc.lsp without -p so that
# doc.lisp will be newer than books/system/doc/acl2-doc.lisp, and
# hence doc.lisp won't later be rebuilt needlessly.
.PHONY: update-doc.lisp
update-doc.lisp: books/system/doc/acl2-doc.lisp books/system/doc/rendered-doc.lsp
@diff doc.lisp books/system/doc/rendered-doc.lsp 2>&1 > /dev/null ; \
if [ $$? != 0 ] ; then \
mv -f doc.lisp doc.lisp.backup ; \
cp books/system/doc/rendered-doc.lsp doc.lisp ; \
echo "NOTE: doc.lisp has changed." ; \
echo " If you use :DOC at the terminal, then" ; \
echo " you might wish to rebuild your ACL2 executable." ; \
else \
echo "Note: doc.lisp is up-to-date." ; \
fi
# Note: The following target uses $(PREFIXsaved_acl2) -- but we don't
# care much about whether it's up-to-date in any sense, so we don't
# make the next target depend on $(PREFIXsaved_acl2). This hasn't
# been super carefully thought out, so could change.
books/system/doc/rendered-doc.lsp: check-books
rm -f books/system/doc/rendered-doc.lsp
cd books ; (export ACL2_XDOC_TAGS=FANCY ; $(MAKE) USE_QUICKLISP=1 system/doc/render-doc.cert ACL2=$(ACL2))
.PHONY: STATS
# See the Essay on Computing Code Size in the ACL2 source code.
STATS:
@ACL2=$(ACL2) ;\
export ACL2 ;\
ACL2_SOURCES="$(sources)" ;\
export ACL2_SOURCES ;\
doc/create-acl2-code-size
.PHONY: clean-lite
clean-lite:
# Unlike clean-all, this does not remove executables or corresponding scripts
# (since there could be many executables that one prefers not to delete),
# except for *osaved_acl2* files.
rm -f *.o *#* *.c *.h *.data gazonk.* workxxx* workyyy* *.lib \
*.fasl *.fas *.sparcf *.ufsl *.64ufasl *.ufasl *.dfsl *.dxl \
*.d64fsl *.dx64fsl *.lx64fsl \
*.lx32fsl *.x86f *.sse2f
10000
*.o *.fn \
TAGS TAGS-acl2-doc acl2-status.txt acl2r.lisp acl2-proclaims.lisp \
.acl2rc *osaved_acl2* *.log devel-check.out TMP*
rm -rf saved
rm -f doc/*.o doc/*#* doc/*.c doc/*.h doc/*.data doc/gazonk.* \
doc/workxxx doc/workyyy doc/*.lib \
doc/*.fasl doc/*.fas doc/*.sparcf doc/*.ufsl doc/*.64ufasl doc/*.ufasl doc/*.dfsl \
doc/*.dxl doc/*.d64fsl doc/*.dx64fsl doc/*.lx64fsl \
doc/*.lx32fsl doc/*.x86f doc/*.sse2f doc/*.o doc/*.fn \
doc/*.cert doc/*.port doc/*.out \
doc/*.log doc/TMP*
rm -rf doc/TEX doc/HTML doc/EMACS
.PHONY: clean-all clean
clean clean-all: clean-lite
rm -f *saved_acl2* doc.lisp.backup
# Inspired by https://www.gnu.org/prep/standards/html_node/Standard-Targets.html:
.PHONY: distclean
distclean: clean-all
# The .NOTPARALLEL target avoids our doing any build process in
# parallel. Uses of makefiles in other directories, even if invoked
# from this makefile, can still take advantage of -j (as per the GNU
# make documentation).
.NOTPARALLEL:
# Warning: Be careful about adding quotes on "echo" commands below.
# Those don't seem to work well with the "-n" option in a Makefile on
# at least one Mac.
.PHONY: large
large: acl2r
ifeq ($(ACL2_MAKE_LOG),NONE)
$(MAKE) full init
else
@$(MAKE) --no-print-directory set-up-log
@echo -n Compiling ...
@echo "-*- Mode: auto-revert -*-" > "$(ACL2_MAKE_LOG)"
@rm -f acl2-status.txt
@$(MAKE) full >> "$(ACL2_MAKE_LOG)" 2>&1 || (echo "\nERROR: See $(ACL2_MAKE_LOG)." ; exit 1)
# The "incomplete" case below shouldn't happen (unless maybe upon aborting).
@acl2_compile_status="`cat acl2-status.txt`" ;\
if [ "$$acl2_compile_status" = :COMPILED ] ; then \
echo " done." ;\
elif [ "$$acl2_compile_status" = :COMPILE-SKIPPED ] ; then \
echo " not performed for this host Lisp." ;\
else \
echo " incomplete." ;\
exit 1 ;\
fi
@echo -n Bootstrapping, then saving executable \(may take a few minutes\) ...
@$(MAKE) init >> "$(ACL2_MAKE_LOG)" 2>&1 || (echo "\n**ERROR**: See $(ACL2_MAKE_LOG)." ; exit 1)
@echo " done."
@echo "Successfully built $(ACL2_WD)/${PREFIXsaved_acl2}."
@echo "Updating books/build/."
@if [ -d books/build ] ; then \
$(MAKE) --no-print-directory update_books_build_info ;\
fi
endif
# The following target should be used with care, since it fails to
# rebuild the desired executable when it already exists and is more
# recent than the sources. For example, if you change Lisp
# implementations without changing PREFIX, perhaps even only changing
# the version of your Lisp, then use "make large", not "make update".
.PHONY: update
update: $(PREFIXsaved_acl2)
# Note: Below, the lines below "large" probably aren't needed, since
# these variables can only be set on the command line. But we'll
# leave them in place for now.
$(PREFIXsaved_acl2): $(ACL2_DEPS)
@$(MAKE) large \
PREFIX=$(PREFIX) \
LISP=$(LISP) \
ACL2_SAFETY=$(ACL2_SAFETY) \
ACL2_SPACE=$(ACL2_SPACE) \
ACL2_STACK_ACCESS=$(ACL2_STACK_ACCESS) \
ACL2_COMPILER_DISABLED=$(ACL2_COMPILER_DISABLED) \
ACL2_EGC_ON=$(ACL2_EGC_ON) \
ACL2_EXIT_LISP_HOOK=$(ACL2_EXIT_LISP_HOOK) \
ACL2_SIZE=$(ACL2_SIZE) \
ACL2_IGNORE=$(ACL2_IGNORE) \
TAGS_ACL2_DOC=$(TAGS_ACL2_DOC)
.PHONY: large-acl2r
large-acl2r:
@$(MAKE) -s large ACL2_REAL=r
.PHONY: large-acl2d
large-acl2d:
@$(MAKE) -s large ACL2_DEVEL=d
.PHONY: large-acl2p
large-acl2p:
@$(MAKE) -s large ACL2_PAR=p
.PHONY: save-exec
# Note: As per GitHub Issue #1422, $(ACL2_SAVED) is rebuilt unconditionally.
save-exec:
@if [ "$(ACL2_CUSTOMIZATION)" = "" ] || \
[ "$(ACL2_CUSTOMIZATION)" = "NONE" ] ; then \
echo "Error: ACL2_CUSTOMIZATION must be set for target $(@)." ;\
exit 1 ;\
fi
@if [ ! -f "$(ACL2_CUSTOMIZATION)" ] ; then \
echo "Error: ACL2_CUSTOMIZATION = $(ACL2_CUSTOMIZATION), but" ;\
echo " that file does not exist." ;\
exit 1 ;\
fi
@$(MAKE) update
@rm -f workxxx
@echo "Preparing to save $(ACL2_SAVED) using ACL2_CUSTOMIZATION = $(ACL2_CUSTOMIZATION) ..."
@echo '(value :q) (save-exec "$(ACL2_SAVED)" $(ACL2_SAVED_ARGS))' > workxxx
@./$(PREFIXsaved_acl2) < workxxx > $(ACL2_SAVED).out
@echo "... done (see $(ACL2_SAVED).out for log)."
@rm -f workxxx
# Since ACL2_WAG is for implementors only, we don't bother making a
# target for it. Instead one just uses ACL2_WAG=w on the "make"
# command line.
# NOTE: None of the book certification targets use PREFIX. They use
# "acl2" by default, but the ACL2 executable can be specified on the command
# line with ACL2=<some_acl2_executable>.
# Success can generally be determined by checking for the absence of ** in the
# log.
# Certify books that are not up-to-date, even those less likely to be
# included in other books. Success can generally be determined by
# checking for the absence of ** in the log, or by looking at the Unix
# exit status.
.PHONY: regression
regression: check-books
cd books ; $(MAKE) $(ACL2_IGNORE) regression ACL2=$(ACL2)
.PHONY: regression-everything
regression-everything: check-books
cd books ; $(MAKE) $(ACL2_IGNORE) regression-everything ACL2=$(ACL2)
# Do regression tests from scratch.
# Success can generally be determined by checking for the absence of ** in the
# log.
.PHONY: regression-fresh
regression-fresh: clean-books
$(MAKE) $(ACL2_IGNORE) ACL2=$(ACL2) regression
.PHONY: regression-everything-fresh
regression-everything-fresh: clean-books
$(MAKE) $(ACL2_IGNORE) ACL2=$(ACL2) regression-everything
# The following allows for a relatively short test, in response to a request
# from GCL maintainer Camm Maguire. The legacy name is
# certify-books-short; the preferred name now is basic.
.PHONY: basic certify-books-short
basic: check-books
uname -a
cd books ; $(MAKE) $(ACL2_IGNORE) ACL2=$(ACL2) basic
certify-books-short: basic
# The following target assumes that we are using an image built with
# ACL2_DEVEL set, and then have certified the books mentioned in
# *system-verify-guards-alist*, currently system/top, for example as
# follows. (This has taken about 2 minutes on a 2015 MacBook Pro.)
# # Perhaps start with make clean-books. Then, where the -j
# # argument is optional:
# cd books
# ./build/cert.pl -j 8 --acl2 `pwd`/../saved_acl2d system/top.cert
.PHONY: devel-check
devel-check:
@echo "(chk-new-verified-guards)" > workxxx.devel-check
@$(ACL2) < workxxx.devel-check > devel-check.out
@if [ "`fgrep CHK-NEW-VERIFIED-GUARDS-SUCCESS devel-check.out`" ] ; then \
rm -f workxxx.devel-check devel-check.out ;\
echo 'SUCCESS for chk-new-verified-guards' ;\
break ;\
else \
echo '**FAILED** for chk-new-verified-guards;' ;\
echo ' output log follows:' ;\
cat devel-check.out ;\
rm -f workxxx.devel-check ;\
exit 1 ;\
fi
@echo "(check-system-events)" > workxxx.devel-check
@$(ACL2) < workxxx.devel-check > devel-check.out
@if [ "`fgrep CHECK-SYSTEM-EVENTS-SUCCESS devel-check.out`" ] ; \
then \
rm -f workxxx.devel-check devel-check.out ;\
echo 'SUCCESS for check-system-events' ;\
else \
echo '**FAILED** for check-new-system-events;' ;\
echo ' output log follows:' ;\
cat devel-check.out ;\
rm -f workxxx.devel-check ;\
exit 1 ;\
fi
@echo 'SUCCESS for devel-check'
# Note that clean-doc does NOT delete source file doc.lisp,
# because it's important that there is always a doc.lisp present when
# building ACL2. If we want to refresh doc.lisp, we can do so
# without running the clean-doc target.
.PHONY: clean-doc
clean-doc: check-books
cd books/system/doc ; ../../build/clean.pl
rm -rf doc/manual
rm -f books/system/doc/rendered-doc.lsp
.PHONY: clean-books
clean-books: check-books
cd books ; $(MAKE) $(ACL2_IGNORE) ACL2=$(ACL2) moreclean
# This following should be executed inside the acl2-sources directory.
# You probably need to be the owner of all files in order for the chmod
# commands to work, but perhaps not.
# Keep tar in sync with tar-workshops.
.PHONY: tar
tar:
rm -f acl2.tar.Z acl2.tar.gz acl2.tar
rm -f SUM
# Historical comment (may be updated some day...):
# We want the extracted tar files to have permission for everyone to write,
# so that when they use -p with tar they get that permission.
# But we don't want the tar file itself to have that permission. We may as
# well protect all the other files too from writing by CLI people other than
# those in the acl2 group, even though these files aren't the ones transferred
# to the ftp server. Those come from the tar file, and we will extract them
# without the -p option so that the ftp files will not be world-writable.
cd .. ; chmod -R g+r acl2-sources ; chmod -R o+r acl2-sources ; tar cvf /tmp/acl2.tar acl2-sources ; chmod -R o-w acl2-sources
mv /tmp/acl2.tar .
gzip acl2.tar
md5sum acl2.tar.gz > acl2-tar-gz-md5sum
# Keep tar-workshops in sync with tar.
# This target should be executed in the acl2-sources directory.
.PHONY: tar-workshops
tar-workshops: check-books
cd books ; rm -f workshops.tar.Z workshops.tar.gz workshops.tar workshops-tar-gz-md5sum
cd books ; chmod -R g+r workshops ; chmod -R o+r workshops ; tar cvf /tmp/workshops.tar workshops ; chmod -R o-w workshops
mv /tmp/workshops.tar books/
cd books ; gzip workshops.tar
cd books ; (md5sum workshops.tar.gz > workshops-tar-gz-md5sum)
.PHONY: mini-proveall
mini-proveall:
@rm -rf mini-proveall.out
@echo '(value :q) (lp) (mini-proveall)' | ./${PREFIXsaved_acl2} > mini-proveall.out
@(grep '^ "Mini-proveall completed successfully."' mini-proveall.out > /dev/null) || \
(echo 'Mini-proveall failed!' ; ls -l ./${PREFIXsaved_acl2}; cat mini-proveall.out ; exit 1)
@echo 'Mini-proveall passed.'
# Target for making an Allegro CL application acl2.exe in a new "bin/" subdirectory.
# NOTE: An Allegro CL dynamic runtime license is needed in order for this to work.
# Also, a file our-develenv.cl is needed in this (the ACL2 sources) directory. As
# explained in file build-allegro-exe.cl:
# [File our-develenv.cl] is obtained from a path such as
# <path-to-allegro>/AllegroCL-7.0/acl70/develenv.cl, then commenting out those
# not allowed in runtime images, as suggested in the above file.
ACL2_BIN_DIR = bin
.PHONY: allegro-app
allegro-app: our-develenv.cl
@if [ -L ${PREFIXsaved_acl2} ]; then \
echo "Note: removing link ${PREFIXsaved_acl2}"; \
rm -f ${PREFIXsaved_acl2}; \
elif [ -f ${PREFIXsaved_acl2} ]; then \
echo "ERROR: Please move or remove ${PREFIXsaved_acl2} first."; \
exit 1; \
fi
@if [ -d "${ACL2_BIN_DIR}" ]; then \
echo "ERROR: Please remove the ${ACL2_BIN_DIR}/ subdirectory."; \
exit 1; \
fi
$(MAKE) full
rm -f workxxx
echo '(generate-application "acl2.exe" "${ACL2_BIN_DIR}/" (quote ("build-allegro-exe.cl")) :runtime :dynamic :include-compiler t) (exit)' > workxxx
${LISP} < workxxx
rm -f workxxx
@echo "Creating link from ${PREFIXsaved_acl2} to ${ACL2_BIN_DIR}/acl2.exe ."
ln -s ${ACL2_BIN_DIR}/acl2.exe ${PREFIXsaved_acl2}
# Support for target allegro-app:
our-develenv.cl:
@echo "ERROR:"
@echo " Please create file our-develenv.cl. This may be obtained by"
@echo " copying a file <path-to-allegro>/AllegroCL-7.0/acl70/develenv.cl,"
@echo " and then commenting out those forms not allowed in runtime"
@echo " images, as suggested in the that file."
exit 1
# Developer target only. WARNING: Be sure to run "make regression"
# first! We could add a dependency on regression, but maybe there
# will be some case in which we know part of the regression fails but
# we want to run this anyhow and it would get in the way to have a
# regression failure (though I don't know how that might happen).
.PHONY: chk-include-book-worlds
chk-include-book-worlds: check-books
uname -a
cd books ; $(MAKE) $(ACL2_IGNORE) chk-include-book-worlds ACL2=$(ACL2)