forked from acl2/acl2
-
Notifications
You must be signed in to change notification settings - Fork 0
/
acl2.lisp
2709 lines (2251 loc) · 107 KB
/
acl2.lisp
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
994
995
996
997
998
999
1000
; ACL2 Version 8.1 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2018, 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 NOTE-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.
; Acknowledgments: Bob Boyer contributed crucially to the design and
; implementation of early versions of ACL2. Many others, largely at CLI, have
; also contributed to the design of certain features. We especially thank
; Bishop Brock and John Cowles for their contributions. See the documentation
; topic ACKNOWLEDGMENTS for more information.
; This research was supported in part at Computational Logic, Inc. by the
; Defense Advanced Research Projects Agency (DARPA), ARPA Orders #6082, 9151
; and 7406 and by the Office of Naval Research, contracts numbers
; N00014-88-C-0454, N00014-91-C-0130, and N00014-94-C-0193. The views and
; conclusions contained in this document are those of the author(s) and should
; not be interpreted as representing the official policies, either expressed or
; implied, of Computational Logic, Inc., Office of Naval Research, DARPA or the
; U.S. Government.
; This file cannot be compiled because it changes packages in the middle.
; This file, acl2.lisp, (a) builds the packages for the ACL2 system, (b)
; defines the functions for loading and compiling ACL2 and for running code
; verified using ACL2, and (c) makes a couple of checks concerning minor,
; non-CLTL, assumptions that we make about Common Lisps in which ACL2 is to
; run.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; CLTL1/CLTL2
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; For the most part, we program in a subset both of CLTL1 and CLTL2.
; However, there are a few places, notably the name of the main
; package for Lisp symbols, where this is impossible. So we use the
; read conditional #+CLTL2. If one wishes to run ACL2 under CLTL2,
; execute the following form before commencing compiling or loading:
; (push :CLTL2 *features*)
; For example, for Allegro and lispworks (respectively) we have the following.
#+(or ansi-cl draft-ansi-cl-2 lispworks clisp ccl)
(push :CLTL2 *features*)
; We use IN-PACKAGE in a way that is consistent with both CLTL1 and
; CLTL2, namely as a macro (i.e., whose argument is not evaluated) for
; switching *package* to an existing package, value ignored.
(in-package #-CLTL2 "USER" #+CLTL2 "COMMON-LISP-USER")
; Avoid warning, at least in Allegro CL, for use of this variable below. Note
; that it is set to nil using GNUmakefile when ACL2_COMPILER_DISABLED is set.
(defvar *acl2-compiler-enabled*)
; Changes Made in Support of CMU Lisp
; (0) (The following issue with Cmulisp no longer seems to be true, at least
; as of Version 19e on Linux.)
; Cmulisp doesn't support EVAL-WHEN. This meant that in the #+cmu case
; I had to put down special code to try to do what other lisps do.
; Generally, this involved just not checking for certain errors (compiling
; files that weren't supposed to be compiled) in #+cmu that were checked
; in other lisps. In one case, namely the initialization of
; current-acl2-world, it involved a little more.
; (1) cmulisp switches from *standard-input* to *terminal-io* when the input
; stream reaches eof; our other lisps all exit to the operating system.
; This means all the batch jobs we submit via make have to be arranged to
; exit from cmulisp before eof. This required changing the top-level
; makefile and the makefiles of all the community books. I generally put a
; `:q #+cmu (lisp::quit)' at the end of each workxxx.
; These could be replaced simply by `:q (acl2::exit-lisp)'.
; (2) Cmulisp checks type assertions at runtime. I found two of our assertions
; violated by actual use. In fmt-char we mistakenly claimed the string's
; length was less than 101. This was a typo -- elsewhere in the same
; function we claimed it was just a fixnum -- apparently caused by
; copying a type-declaration and failing to edit it thoroughly. (Another
; variable was correctly limited to 101.)
; In maximal-elements1, used in the selection of induction candidates,
; we claimed (by using int=) that the scores for an induction candidate
; are integers when in fact they are rationals.
; (3) Evidently, all functions in cmulisp pass the compiled-function-p test.
; If you defun foo and immediately get its symbol-function you get
; an object like #<Interpreted function ...>. If you ask whether
; this object is a compiled-function-p you get t. If you compile
; foo the symbol-function changes to an object like #<Function
; ...>, which also passes the test.
; The fact that everything in a symbol-function field looks like a compiled
; function killed us in an interesting way. Most locally, it made
; compile-uncompiled-*1*-defuns write out an empty file of functions to
; compile, because everything looked compiled already. But where that
; really got us was that we use that function to create TMP1.lisp during
; the bootstrapping. TMP1.lisp, recall, contains the mechanically
; generated executable-counterparts of logic mode functions defined in
; axioms.lisp. By not generating these we built an image in which the
; relevant functions were undefined. Because of the rugged way we invoke
; them, catching errors and producing a HIDE term if we can't eval them,
; we survived the certification of many books before we finally got to a
; proof that couldn't be done without running one of those functions.
; The proof, in the bdd community books, required evaling (nth -1 nil), which
; according to the axioms is nil but which we couldn't deduce because
; ACL2_*1*_COMMON-LISP::NTH was undefined.
; My fix was to define and use compiled-function-p! instead of the standard
; compiled-function-p. The new function has a #+/-cmu split in it. In the
; cmu case I ask
; (not (eq (type-of (symbol-function fn)) 'eval:interpreted-function))
; So I say fn is compiled if its symbol-function is not an object like
; #<Interpreted function ...>.
; (4) CMU Lisp does not allow us to "undefine" a macro-function. That is,
; one is not permitted to store a nil into the macro-function
; field because nil is not a function. We do this when we
; implement undo. We handle it by storing a dummy function
; instead, and change the notion of when a symbol is virgin to
; recognize the case that its symbol-function or macro-function is
; the dummy.
; (5) We made a few fixes and cleanups in order to avoid compiler warnings.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; SAFETY AND PROCLAIMING
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defvar *acl2-optimize-form*
`(optimize #+cltl2 (compilation-speed 0)
; The user is welcome to modify this proclaim form. For example, in CCL and
; SBCL, where the "full" target does essentially nothing other than note in
; file acl2-status.txt that the system has allegedly been compiled, the
; following procedure works.
; # Write :COMPILED to acl2-status.txt.
; make full LISP=ccl
; # Next, edit acl2r.lisp with the desired variant of *acl2-optimize-form*,
; # for example as follows.
; # (defparameter cl-user::*acl2-optimize-form*
; # '(OPTIMIZE (COMPILATION-SPEED 0) (DEBUG 0) (SPEED 0) (SPACE 0)
; # (SAFETY 3)))
; #
; # Now start CCL and evaluate:
; (load "init.lisp") ; loads acl2r.lisp
; (in-package "ACL2")
; (save-acl2 (quote (initialize-acl2 (quote include-book)
; acl2::*acl2-pass-2-files*))
; "saved_acl2")
; (exit-lisp)
; The following may allow more tail recursion elimination (from "Lisp
; Knowledgebase" at lispworks.com); might consider for Allegro CL too.
#+(or lispworks ccl) (debug 0)
#+cmu (extensions:inhibit-warnings 3)
#+sbcl (sb-ext:inhibit-warnings 3)
(speed 3)
; Consider replacing cmu on the next line with (or cmu sbcl). The SBCL manual
; says the following, but a quick test with (or cmu sbcl) yielded no smaller
; .core file size and no quicker (mini-proveall).
; The value of space mostly influences the compiler's decision whether to
; inline operations, which tend to increase the size of programs. Use the
; value 0 with caution, since it can cause the compiler to inline operations
; so indiscriminately that the net effect is to slow the program by causing
; cache misses or even swapping.
(space #+cmu 1 #-cmu 0)
; WARNING: Do not proclaim (cl-user::fixnum-safety 0) for LispWorks. Any
; fixnum-safety less than 3 expects all integers to be fixnums!
(safety
; Consider using (safety 3) if there is a problem with LispWorks. It should
; allow stack overflows to report an error, rather than simply to hang.
; Safety 1 for CCL has avoided the kernel debugger, e.g. for compiled calls
; of car on a non-nil atom. The following results for CCL show why we have
; decided to keep the safety at 0 by default and why safety 3 is not too bad.
;
; Safety 0:
; 12955.537u 542.877s 3:46:24.68 99.3% 0+0k 0+0io 0pf+0w
;
; Safety 1:
; 15343.578u 562.207s 4:27:03.67 99.2% 0+0k 0+0io 0pf+0w
; Try safety 2 or 3 to find violations with Allegro CL like the car of a
; non-nil atom. (Note: safety 3 has failed in GCL due to a stack overflow.)
; Here are some numbers with Allegro CL, 8 processors with make -j 8:
; Safety 0:
; 11262.699u 291.730s 38:23.72 501.5% 0+0k 0+0io 16pf+0w
; Safety 2:
; 15588.206u 285.249s 54:19.72 486.9% 0+0k 0+0io 0pf+0w
; Safety 3:
; 16450.508u 284.473s 57:46.03 482.8% 0+0k 0+0io 0pf+0w
; Here are GCL numbers, again with make -j 8 (and using "fast builds").
; Safety 0:
; 10013.573u 566.983s 33:33.80 525.4% 0+0k 0+0io 0pf+0w
; Safety 2:
; [Note: community book
; books/clause-processors/SULFA/books/sat-tests/test-incremental.lisp
; ran out of space, saving perhaps a minute]
; 15637.669u 511.811s 52:02.78 517.1% 0+0k 0+0io 0pf+0w
,(let ((our-safety
#-CLTL2
(if (boundp 'user::*acl2-safety*)
(symbol-value 'user::*acl2-safety*)
nil)
#+CLTL2
(if (boundp 'common-lisp-user::*acl2-safety*)
(symbol-value 'common-lisp-user::*acl2-safety*)
nil)))
(if our-safety
(progn (format t "Note: Setting SAFETY to ~s."
our-safety)
our-safety)
0))
)
#+ccl
,@(let ((our-stack-access
(if (boundp 'common-lisp-user::*acl2-stack-access*)
(symbol-value 'common-lisp-user::*acl2-stack-access*)
nil)))
(if our-stack-access
(progn (format t "Note: Setting :STACK-ACCESS to ~s."
our-stack-access)
`((:stack-access ,our-stack-access)))
nil))
))
(proclaim *acl2-optimize-form*)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; FILES
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; This is the file acl2.lisp, the first source file for ACL2. The names of the
; other ACL2 source files are listed under *acl2-files*.
; All of ACL2 is written in Common Lisp and we expect that ACL2 will run in any
; Common Lisp except for those Common Lisps which fail the tests we execute
; upon loading this file, acl2.lisp. With the exception of this and other
; initialization files, files *-raw.lisp, and those constructs after the
; #-acl2-loop-only readtime conditional, ACL2 is written in the applicative
; Common Lisp for which ACL2 is a verification system.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; READING CHARACTERS FROM FILES
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Files may be viewed as sequences of bytes. But Lisp can interpret these byte
; sequences as sequences of characters, depending on so-called character
; encodings.
; For example, through about March 2012 the default character encoding in CCL
; was ISO-8859-1, sometimes known as LATIN-1. When this changed to UTF-8 a
; failure was reported when attempting to certify community book
; books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/coe-fld.lisp,
; apparently because of the following line, where the next-to-last character is
; actually an accented `o' sometimes known as
; #\LATIN_SMALL_LETTER_O_WITH_ACUTE, having code 243. (The CLISP build fails
; if we use that character here, because at this point we have not yet made the
; adjustments to the character encoding that are done below!)
;;; Inverso de la primera operacion
; The accented `o' above is encoded as a single byte in LATIN-1 but as two
; bytes in UTF-8.
; Jared Davis then suggested that we explicitly specify ISO-8859-1, which might
; be slightly more efficient for reading files. Note that GCL (non-Ansi, circa
; 2010 but probably later) only supports ISO-8859-1 as far as we can tell. We
; follow Jared's suggestion below. It seems that character encoding for
; reading from files is controlled differently from character encoding for ACL2
; reading from the terminal. Jared also suggested setting the terminal
; encoding to ISO-8859-1 as well, and showed us how to do that in CCL. We have
; been unable to figure out how to do that in some other host Lisps, but since
; files are typically shared between users and (of course) ACL2 reading from
; the terminal is not, the encoding for the terminal seems less important than
; for files.
; Even for files, we assert there is no soundness issue, in the sense that for
; maximum trust we expect each user to certify all books from scratch in a
; single environment. But in practice, users share books (in particular,
; via the community books); so it is desirable to enforce uniform character
; encodings for files.
; The use of latin-1 could in principle cause problems for those whose default
; Emacs buffer encoding is utf-8. That's in fact the case for us at UT CS, but
; not on one of our Mac laptops as of this writing (April 2012), probably
; because environment variable LANG is en_US.UTF-8 at UT CS. But ACL2 users
; don't often save Lisp files with nonstandard characters. If they have
; occasion to do so, they can evaluate
; (setq save-buffer-coding-system 'iso-8859-1)
; in Emacs buffers before saving into files. This will happen automatically
; for users who load file emacs/emacs-acl2.el into their emacs sessions.
; At any rate, it seems best to standardize file encodings and leave it to
; individuals to cope with editing issues.
; Without further ado, we set the default encoding for files. Below, we make
; some attempt to do so for the terminal. We wrap all this into a function,
; because we have found that for sbcl, upon restart we lose the effect of the
; assignment below. It seems safest then to do these same assignments at
; startup; see the call of the following function in acl2-default-restart.
(defun acl2-set-character-encoding ()
; We set the character encoding (see discussion above).
#+allegro
; Alternatively, we could set the locale on the command line using -locale C:
; see http://www.franz.com/support/documentation/6.1/doc/iacl.htm#locales-1
; Note that (setq *default-external-format* :ISO-8859-1) is obsolete:
; http://www.franz.com/support/documentation/6.1/doc/iacl.htm#older-ef-compatibility-2
(setq *locale* (find-locale "C"))
#+ccl
(setq ccl:*default-file-character-encoding* :iso-8859-1)
; #+clisp
; Set using -E ISO-8859-1 command-line option from save-exec.
; Note that the setting below for custom:*default-file-encoding* works for
; files, but we were unable to do the analogous thing successfully for
; custom:*terminal-encoding*, even when restricting that assignment to
; (interactive-stream-p *terminal-io*).
#+cmu
(setq *default-external-format* :iso-8859-1)
; #+gcl -- already iso-8859-1, it seems, and nothing we can do to change
; the encoding anyhow
#+lispworks
; This the default on our linux system, at least on both 32- and 64-bit,
; version 6.1.0. But it doesn't seem to suffice; see
; our-lispworks-file-encoding below.
(setq stream::*default-external-format* '(:LATIN-1 :EOL-STYLE :LF))
#+sbcl
(setq sb-impl::*default-external-format* :iso-8859-1)
; ;;;
; We have made only limited attempts to set the character encoding at the
; terminal, as discussed above.
; ;;;
; #+allegro
; Handled by *locale* setting above. Formerly the following was later in
; this file; now we include it only as a comment.
; #+(and allegro allegro-version>= (version>= 6 0))
; (setf (stream-external-format *terminal-io*)
; (excl::find-external-format
; #+unix :latin1-base
; #-unix :latin1))
; #+ccl
; For terminal, set using -K ISO-8859-1 command-line option from save-exec.
; #+cmucl -- Probably no setting is necessary.
; #+clisp -- Set using command-line option (see above).
; #+gcl -- There seems to be nothing we can do.
; #+lispworks -- No support seems to be available.
; #+sbcl
; We found that "unsetenv LANG" results in (stream-external-format
; *terminal-io*) being ascii at the terminal instead of utf-8; or, just start
; up sbcl like this to get ascii:
; LANG=C ; XTERM_LOCALE=C ; sbcl
; But we don't know how to get latin-1. We even tried each of these, but got
; ascii:
; LANG=en_US.LATIN-1 ; XTERM_LOCALE=en_US.LATIN-1
; LANG=en_US.ISO-8859-1 ; XTERM_LOCALE=en_US.ISO-8859-1
)
; Here, we invoke the function defined above, so that a suitable character
; encoding is used during the build, not only when starting up a built image
; (which is why we call acl2-set-character-encoding in acl2-default-restart).
(acl2-set-character-encoding)
; We also do the following for clisp, since we set the encoding on the command
; line (see comment above) but we want to be able to read our own source files
; during the build. See the comment in (defxdoc character-encoding ...) in
; community book books/system/doc/acl2-doc.lisp.
#+clisp
(setq custom:*default-file-encoding*
(ext:make-encoding :charset 'charset:iso-8859-1
; The following is consistent with what we used to do in acl2-init.lisp; see
; the commented-out call there that sets custom:*default-file-encoding*.
; Unfortunately, according to http://www.clisp.org/impnotes/clhs-newline.html,
; this doesn't treat CR/LF as two characters when reading files -- for example,
; the file "foo.lisp" defined in a comment below for dealing with LispWorks
; provides (len *c*) = 3, not 4.
:line-terminator :unix))
; We seem to need to do more for LispWorks. To see why, create a book
; "foo.lisp" as follows.
;
; (in-package "ACL2")
; (defconst *c*
; "x
; y")
;
; Next, if you have arranged in emacs to set save-buffer-coding-system
; 'iso-8859-1, as in emacs/emacs-acl2.el, turn that off and bring foo.lisp into
; a buffer; then add control-M at the end of every line; and finally, save the
; buffer, which will save the control-M at the end of every line and, in
; particular, in the middle of the string. (And now restore your handling of
; save-buffer-coding-system.) In a Lispworks image of ACL2, execute (ld
; "foo.lisp"), and you can evaluate (length *c*) to get 3, where 4 is expected
; because of the control-M. We adopt here a solution found on the web at:
; http://www.lispworks.com/documentation/lw60/LW/html/lw-470.htm
#+lispworks
(defun our-file-encoding (pathname ef-spec buffer length)
(system:merge-ef-specs ef-spec '(:LATIN-1 :EOL-STYLE :LF)))
#+lispworks
(setq system::*file-encoding-detection-algorithm*
'(our-file-encoding))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; LISP BUGS AND QUIRKS
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; See acl2-fns.lisp for a fix to user-homedir-pathname for some versions of
; GCL.
; See the function print-number-base-16-upcase-digits for an explanation of the
; following code, which pushes a feature when that function can be needed.
(let ((*print-base* 16) (*print-case* :downcase))
(let ((tmp (with-output-to-string (s) (princ 10 s))))
(cond ((equal tmp "A"))
((equal tmp "a")
(format t
"~%Note: Numbers in base 16 will be printed using a ~
special-purpose~% ACL2 function, ~s."
'print-number-base-16-upcase-digits)
(push :acl2-print-number-base-16-upcase-digits *features*))
(t (error "Surprising result for (princ 10 s) in base 16: ~s"
tmp)))))
; To use ACL2 under LispWorks 3.2.0, execute the following to work around a
; bug.
; #+lispworks
; (setf (svref ccl::*funny-symbol-char-table* (char-code #\.)) t)
; Next, we correct *features* for Windows.
#+(and (or winnt win32 windows) (not mswindows))
(setq *features*
(cons :mswindows *features*))
#+(and (or mswindows winnt) unix)
(setq *features*
(delete :unix *features*
:test
(function (lambda (x y)
(equal (symbol-name x) (symbol-name y))))))
; Turn off automatic declaration of special variables, in particular since we
; do not want state declared special; see the comment above
; (eval '(setq state *the-live-state*)) in load-acl2.
#+cmu
(setq ext:*top-level-auto-declare* nil)
; Turn off compiler verbosity going to error stream, since even >& does not
; seem to redirect that stream to a file.
#+(or cmu sbcl)
(setq *compile-verbose* nil)
#+(or cmu sbcl)
(setq *compile-print* nil)
; Turn off gc verbosity (same reason as above).
#+cmu
(setq ext:*gc-verbose* nil)
#+ccl
(when (fboundp 'ccl::gc-verbose) ; not in OpenMCL 1.0 (CCL)
; This gets overridden for ACL2(h) in acl2h-init.
(apply 'ccl::gc-verbose nil nil))
; See later in this file for with-warnings-suppressed (after we introduce and
; enter the ACL2 package).
; Avoid saving source file information, which could cause some slowdown and
; isn't typically exploited by ACL2 users.
#+ccl
(setq ccl::*record-source-file* nil)
; Camm Maguire has suggested, on 9/22/2013, the following forms, which allowed
; him to complete an ACL2 regression using 2.6.10pre.
#+gcl
(progn
(si::allocate 'contiguous 15000 t)
(si::allocate-sgc 'contiguous 15000 100000 10))
; The following avoids errors from extra right parentheses, but we leave it
; commented out since it doesn't seem important enough to merit messing around
; at this low level, and for just one Lisp.
; #+ccl
; (setq ccl::*ignore-extra-close-parenthesis* t)
; We have tried to build under ECL (Embeddable Common-Lisp), and with some
; modifications, we made progress -- except there appears (as of Sept. 2011) to
; be no good way for us to save an executable image. Specifically, it appears
; that c:build-program not will suffice for saving state (properties etc.) --
; it's just for saving specified .o files. (This impression seems to be
; confirmed at http://stackoverflow.com/questions/7686246/saving-lisp-state .)
; Here we document steps to take towards possibly porting to ECL in the future.
; If state-global-let* expansion causes an error due to excessive code blow-up,
; then consider replacing its definition by placing the following after
; state-free-global-let*. HOWEVER, first think about whether this is right; we
; haven't thought through the effect of mixing a stack of let*-bindings of
; state global variables with the acl2-unwind-protect mechanism. Also,
; comments are omitted here; be sure to restore them.
;;; (defmacro state-global-let*-logical (bindings body)
;;; (declare (xargs :guard (and (state-global-let*-bindings-p bindings)
;;; (no-duplicatesp-equal (strip-cars bindings)))))
;;;
;;; `(let ((state-global-let*-cleanup-lst
;;; (list ,@(state-global-let*-get-globals bindings))))
;;; ,@(and (null bindings)
;;; '((declare (ignore state-global-let*-cleanup-lst))))
;;; (acl2-unwind-protect
;;; "state-global-let*"
;;; (pprogn ,@(state-global-let*-put-globals bindings)
;;; (check-vars-not-free (state-global-let*-cleanup-lst) ,body))
;;; (pprogn
;;; ,@(state-global-let*-cleanup bindings 0)
;;; state)
;;; (pprogn
;;; ,@(state-global-let*-cleanup bindings 0)
;;; state))))
;;;
;;; #-acl2-loop-only
;;; (defmacro enforce-live-state-p (form)
;;;
;;; ; Note that STATE is intended to be lexically bound at the point where this
;;; ; macro is called.
;;;
;;; `(progn (when (not (live-state-p state)) ; (er hard! ...)
;;; (let ((*hard-error-returns-nilp* nil))
;;; (illegal 'enforce-live-state-p
;;; "The state was expected to be live in the context of ~
;;; an evaluation of the form:~|~x0"
;;; (list (cons #\0 ',form)))))
;;; ,form))
;;;
;;; (defmacro state-global-let* (bindings body)
;;; (cond #-acl2-loop-only
;;; ((and (symbol-doublet-listp bindings)
;;; (not (assoc-eq 'acl2-raw-mode-p bindings)))
;;;
;;; ; The test above guarantees that we merely have bindings of state globals. A
;;; ; triple requires cleanup using a setter function. Also we avoid giving this
;;; ; simple treatment to 'acl2-raw-mode-p because the semantics of
;;; ; state-global-let* are to call f-put-global, which has side effects in the
;;; ; case of 'acl2-raw-mode-p.
;;;
;;; `(enforce-live-state-p
;;; (warn-about-parallelism-hazard
;;; '(state-global-let* ,bindings ,body)
;;; (state-free-global-let* ,bindings ,body))))
;;; (t `(state-global-let*-logical ,bindings ,body))))
; Also, place the following forms in file acl2-fns.lisp, just above qfuncall
; (but there may be better ways to do this).
;;; ; The following is in acl2.lisp, but seems to be needed here as well.
;;; #+ecl
;;; (ext:package-lock "COMMON-LISP" nil)
;;;
;;; Similarly in acl2.lisp, just before handling of package-lock on
;;; "COMMON-LISP" for clisp:
;;;
;;; #+ecl
;;; (ext:package-lock "COMMON-LISP" nil)
; Finally, consider these additional notes.
;;; We need (require "cmp") if we're to use c:build-program.
;;; Special-form-or-op-p: treat ecl like sbcl.
;;; System-call: treat ecl like akcl (actually replace #+akcl by #+(or akcl
;;; ecl)).
;;; Initialize-state-globals: treat ecl just like lispworks.
;;; Where we have the binding (compiler:*suppress-compiler-notes* t) for akcl,
;;; perhaps include the binding (*compile-verbose* t) for ecl.
;;; Modify exit-lisp to treat ecl like akcl, except using ext::quit instead of
;;; si::bye.
#+ccl
(defvar *acl2-egc-on* ; in "CL-USER" package; see second paragraph below
; This variable provides the initial garbage collection strategy, by way of the
; call of set-gc-strategy in acl2h-init.
; This variable is in the "CL-USER" package (see comment above) because users
; are welcome to set its value, for example by writing the form (defparameter
; cl-user::*acl2-egc-on* nil) to acl2r.lisp before doing the build by using
; ACL2_EGC_ON; see GNUmakefile.
; We formerly turned off EGC in CCL because it didn't seem to work well with
; memoizing worse-than-builtin and sometimes seemed buggy. But Gary Byers made
; changes to improve EGC, in particular its interaction with static conses,
; starting in version 16378 (with the feature below introduced in 16384). It
; seems best not to mess with GC heuristics such as post-gc hooks (see
; set-gc-strategy-builtin-delay), and instead rely on EGC.
#+static-conses-should-work-with-egc-in-ccl
t
#-static-conses-should-work-with-egc-in-ccl
nil)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; PACKAGES
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; We never intend that this file should be compiled, and hence we do
; not need to obey the CLTL1 strictures about putting all IN-PACKAGE
; forms near the front.
(let ((lisp-pkg (find-package "LISP")))
(if lisp-pkg
(let ((cl-pkg (find-package "COMMON-LISP")))
(cond
((and cl-pkg (eq cl-pkg lisp-pkg))
; Then all is well.
)
#+(or cmu (and gcl cltl2))
; Starting with CMUCL 19a, lisp-pkg and cl-pkg are no longer the same. We view
; CMUCL as CLTL2; see (push :CLTL2 *features*) above, noting that :ANSI-CL is
; in *features*. So in this case, we simply ignore lisp-pkg. Probably we can
; do the same for most other lisps, and in fact we do so for ANSI GCL as well.
; However, non-ANSI GCL is handled differently, since the "LISP" package is
; populated there but the "COMMON-LISP" appears to be largely irrelevant.
(t nil)
#-(or cmu (and gcl cltl2))
(t
(when cl-pkg ; but by the test above, cl-pkg is not lisp-pkg
#-gcl ; not non-ANSI GCL
; Perhaps we can just add the present lisp to the case for #+(or cmu (and gcl
; cltl2)), above.
(error "This Lisp is unsuitable for ACL2, because the ~
COMMON-LISP~% package is defined but is not the LISP ~
package.")
#+gcl ; non-ANSI GCL
; Early versions of GCL 2.4.3/2.5.0 had a "COMMON-LISP" package that was
; initially populated only with LISP::T and LISP::NIL. It seems safe to move
; any GCL COMMON-LISP package out of the way before we make "COMMON-LISP" a
; nickname for "LISP".
(rename-package "COMMON-LISP" "COMMON-LISP-renamed"))
(let ((old-name (package-name lisp-pkg)) ; reuse old name, nicknames
(old-nicknames (package-nicknames lisp-pkg)))
(rename-package "LISP"
old-name
(cons "COMMON-LISP" old-nicknames))))))))
(eval-when #-cltl2 (compile)
#+cltl2 (:compile-toplevel)
(error "The file acl2.lisp should never be compiled."))
(dolist
(p (list-all-packages))
(cond ((equal 4 (string< "ACL2" (package-name p)))
(format t
"~%~%Warning: There is already a package with the ~
name ~a. ~%The ACL2 implementation depends upon ~
having complete knowledge of ~%and control over any ~
package whose name begins with the ~%four letters ``ACL2'', ~
so ACL2 may not work in this Lisp." (package-name p))
(cond ((package-use-list p)
(format t "~%~%Warning: The package with name ~a ~
USES the packages in the list ~a. ACL2 will not work ~
in state of affairs."
(package-name p) (package-use-list p)))))))
(or (find-package "ACL2")
(make-package "ACL2" :use nil))
; The definition of defconst appears just below because we use it
; early in axioms.lisp. But first, we define the constant
; *the-live-state* because it is used below in the definition of
; defconst and cmulisp warns if we use it before it has been defined.
; And, in order to define *the-live-state* we need the ACL2_INVISIBLE
; package, which we define here. This package is used for a few odd
; objects that are to be hidden from the ACL2 user. Symbols in this
; package having names that start with "HONS" are reserved for the
; hons/memoization implementation.
(let ((inv "ACL2_INVISIBLE"))
(or (find-package inv)
(make-package inv :use nil)))
; LispWorks has a package named "DEF", and that name conflicts with an ACL2
; package of that name introduced in community book books/coi/. We deal with
; that issue here. Thanks to Martin Simmons for providing this code in place
; of the original code, which instead invoked (rename-package "DEF"
; "DEF-FROM-LW-RENAMED").
#+lispworks
(when (find-package "DEF")
(unless (equal (package-name "DEF") "DSPEC")
(error "Expected LispWorks DEF package to be called DSPEC"))
(rename-package "DSPEC" "DSPEC"
(remove "DEF" (package-nicknames "DSPEC") :test 'equal)))
; The value of the constant *the-live-state* is actually just a
; symbol, but that symbol is the unique representative of the one
; single active, global, real-time state of ACL2, which is represented
; both in real-time (e.g., characters not yet typed) and also rather
; efficiently, using typical von Neumann storage techniques.
; Functions that wish to access the global state must have received
; *the-live-state* as an arg. Functions that modify this global state
; must receive it as an arg and return it.
(defconstant acl2::*the-live-state* 'acl2_invisible::|The Live State Itself|)
; (Defconst *var* term) is essentially just (defparameter *var* term). But
; things are made complicated by the desire not to evaluate term unnecessarily.
; Suppose (defconst *var* term) appears in a certified book, say "book.lisp".
; Then when the events in "book.lisp" are processed, a CLTL-COMMAND is executed
; which causes (defconst *var* term) to be evaluated in the underlying raw
; lisp, assigning a value to *var* in Lisp. But now suppose that the compiled
; file for another book, say "book2.o", is loaded on behalf of include-book.
; If defconst were just defparameter, term would be evaluated again (yielding a
; presumably EQUAL value), which is an unfortunate waste of computation.
; We avoid this in the code below by saving, on the raw Lisp property list of
; *var*, under the key 'REDUNDANT-RAW-LISP-DISCRIMINATOR, a triple, (DEFCONST
; term . val), giving the term we evaluated to produce the setting of the var
; and the value, val, produced. When a defconst (defconst *var* term) is
; evaluated, we ask whether *var* has a value. If not, we just proceed
; normally. But if it has a value, we insist that the discriminator be present
; and appropriate or else we cause a hard error. By appropriate in this case
; we mean that it be a DEFCONST such that the value produced last time is EQ to
; the current setting of *var*, and moreover, either the old and new DEFCONST
; have the same (EQUAL) term to evaluate or else the new value is EQUAL to the
; old. The EQ check is meant to provide some safety if the user has manually
; set *var* in raw lisp, as with setq, since the last defconst to it.
; We anticipate that redundant-raw-lisp-discriminator may be used by the
; support functions for other events, e.g., defstobj. So the value of that
; property is not necessarily (DEFCONST term . val) but may depend on the kind
; of event that stored it. The reason we put the discriminator on the raw lisp
; property list of *var* rather than looking in the world of *the-live-state*,
; where we could in principle find an event-landmark, is that we execute many
; defconsts in axioms.lisp, before the world processing functions, like
; getprop, are defined and so the defmacro below must expand to code that can
; be executed in a partially booted ACL2.
(defvar acl2::*compiling-certified-file* nil)
(defun acl2::defconst-redeclare-error (name)
(let ((stk (symbol-value 'acl2::*load-compiled-stack*)))
(cond (stk
(error
"Illegal attempt to redeclare the constant ~s.~%~
The problem appears to be that you are including a book,~%~
~2T~a,~%~
that attempts to give a definition of this constant that~%~
is incompatible with its existing definition. The ~%~
discrepancy is being discovered while loading that book's~%~
compiled (or expansion) file~:[, as the last such load for~%~
the following nested sequence of included books (outermost~%~
to innermost):~%~{ ~a~%~}~;.~]"
name
(caar stk)
(null (cdr stk))
(reverse (loop for x in stk collect (car x)))))
(t
(error "Illegal attempt to redeclare the constant ~s."
name)))))
(defparameter acl2::*safe-mode-verified-p*
; This global may be bound to t when we are evaluating a form that we know will
; not lead to an ill-guarded call in raw Lisp (say, because the form was
; previously evaluated by ACL2 in safe-mode). See also the comment in
; ec-call1-raw.
nil)
(declaim (ftype (function (t)
(values t))
acl2::large-consp))
(defmacro acl2::defconst (name term &rest rst)
(declare (ignore rst)) ; e.g., documentation
(let ((disc (gensym)))
`(defparameter ,name
(let ((acl2::*safe-mode-verified-p* t))
(cond
((boundp ',name)
(cond
(acl2::*compiling-certified-file*
; We avoid the potentially expensive redundancy check done below, which is
; legitimate since we are simply loading a compiled file at the end of
; certify-book. To see how important this optimization can be, try removing it
; before certifying the following book (thanks to Sol Swords for this
; example).
; (in-package "ACL2")
; (defun tree (n)
; (if (zp n)
; nil
; (let ((sub (tree (1- n))))
; (cons sub sub))))
; (defmacro deftree (name n)
; `(defconst ,name ',(tree n)))
; (deftree *big* 35)
(symbol-value ',name))
(t
; Even though ',name is bound, we refer to its value with
; (symbol-value ',name) rather than simply an in-line ,name, to avoid
; compiler warnings.
(let ((,disc (get ',name
'acl2::redundant-raw-lisp-discriminator)))
(cond
((and (consp ,disc)
(eq (car ,disc) 'acl2::defconst))
(assert (consp (cdr ,disc)))
(cond
((and (eq (cdr (cdr ,disc)) (symbol-value ',name))
; Here, as in defconst-fn, we skip the check just below (which is merely an
; optimization, as explained in defconst-fn) if it seems expensive but the
; second check (below) -- against the term -- could be cheap. Without this
; check, if two books each contain a form (defconst *a* (hons-copy
; '<large_cons_tree>)) then when the compiled file for the second book is
; loaded, the check against the term (i.e. the first check below, as opposed to
; the second check, which uses that term's value) could be intractable. For a
; concrete example, see :doc note-7-2.
(or (let ((disc ,disc)
(qterm ',term))
; We check that acl2::large-consp to avoid a boot-strapping problem in GCL.
(and (not (and (fboundp 'acl2::large-consp)
(acl2::large-consp qterm)))
(equal (car (cdr disc)) qterm)))
(equal (cdr (cdr ,disc)) ,term)))
(symbol-value ',name))
(t (acl2::defconst-redeclare-error ',name))))
((acl2::raw-mode-p acl2::*the-live-state*)
; In this case we allow redeclaration of the constant; this is, after all, raw
; mode, where there are no guarantees.
,term)
(t
(acl2::defconst-redeclare-error ',name)))))))
; If ',name is not bound, we must evaluate ,term. Note that we do so
; outside of all local bindings, so as not to disturb variables in
; term. (There should be none -- this is supposed to be a constant,
; but you never know!) We may want to enforce that this code is only executed
; during the boot-strap; see the Essay on Guard Checking.
(t (let* ((val ,term)
(d (list* 'acl2::defconst ',term val)))
(setf (get ',name 'acl2::redundant-raw-lisp-discriminator)
d)
(cdr (cdr d)))))))))
; We now get our imports for package ACL2, putting them into the
; variable acl2::*common-lisp-symbols-from-main-lisp-package*.
; We use different variables for common-lisp-symbols-from-main-lisp-package*,
; *acl2-version*, and *acl2-files*, in order to avoid compiler warnings for
; redefined variables. Actually, *acl2-version* no longer exists starting with
; Version_2.9.1, but we keep the name below nonetheless.
(defvar acl2::*copy-of-common-lisp-symbols-from-main-lisp-package*)
(defvar acl2::*copy-of-common-lisp-specials-and-constants*)
(defvar acl2::*copy-of-acl2-version*)
(defconstant acl2::*acl2-files*
; The order of these files determines compilation order.
; Note regarding backups at UT CS:
; Even though it's convenient to refer to our UT CS development directory as
; /projects/acl2/devel/, we'll need to get backups from
; /v/filer4b/v11q002/acl2space/acl2/.snapshot/*/devel, not from
; /projects/acl2/.snapshot/*/devel. The latter is just a soft link to
; /projects/acl2/devel, i.e., to /v/filer4b/v11q002/acl2space/acl2/devel.
'(
#+acl2-par "multi-threading-raw"
#+hons "serialize-raw"
"axioms"
"hons" ; but only get special under-the-hood treatment with #+hons
#+hons "hons-raw" ; avoid possible inlining of hons fns in later sources
"basis-a" ; to be included in any "toothbrush"
"memoize" ; but only get special under-the-hood treatment with #+hons
"serialize" ; but only get special under-the-hood treatment with #+hons
"basis-b" ; not to be included in any "toothbrush"
"parallel" ; but only get special under-the-hood treatment with #+acl2-par
#+acl2-par "futures-raw"
#+acl2-par "parallel-raw"
#+hons "memoize-raw"
"translate"
"type-set-a"
"linear-a"
"type-set-b"
"linear-b"
"non-linear"
"tau"
"rewrite"
"simplify"
"bdd"
"other-processes"
"induct"
"proof-builder-pkg"
"doc"
"history-management"
"prove"
"defuns"
"proof-builder-a"
"defthm"
"other-events"
"ld"
"proof-builder-b"
"apply-raw"
"interface-raw"
"defpkgs"
"boot-strap-pass-2-a"
"apply-prim"
"apply-constraints"
"apply"
"boot-strap-pass-2-b"