-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathacl2-init.lisp
2035 lines (1752 loc) · 84.5 KB
/
acl2-init.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 6.4 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2014, 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: [email protected] and [email protected]
; Department of Computer Science
; University of Texas at Austin
; Austin, TX 78712 U.S.A.
; This file cannot be compiled because it changes packages in the middle.
; Allow taking advantage of threads in SBCL, CCL, and Lispworks (where we may
; want to build a parallel version, which needs this to take place). At the
; time that we add (perhaps once again) support for HONS in other lisps besides
; CCL (August, 2012), there has been code developed that depends on mv-let
; being the same as multiple-value-bind; see for example community book
; books/centaur/aig/bddify.lisp, in particular the raw Lisp definition of
; count-branches-to, specifically the use of b* in the labels definition of
; lookup. So we also use multiple-value-bind for mv-let when building the HONS
; version.
#+(or (and sbcl sb-thread) ccl lispworks hons)
(push :acl2-mv-as-values *features*)
; Essay on Parallelism, Parallelism Warts, Parallelism Blemishes, Parallelism
; No-fixes, Parallelism Hazards, and #+ACL2-PAR notes.
; These sources incorporate code for an experimental extension for parallelism
; contributed by David Rager during his master's and Ph.D. dissertation work.
; That extension may be built by setting the :acl2-par feature, for example
; using make (see :DOC compiling-acl2p). The incorporation of code supporting
; parallelism has been carried out while taking great pains to preserve the
; functionality of the ACL2 system proper (i.e., without the experimental
; extension for parallelism).
; At the lowest level, parallel computation is carried out by Lisp threads,
; which provide Lisp-level abstractions of OS threads. A thread can be running
; or blocked (e.g., waiting for a semaphore signal). Threads can create other
; threads. We manage the creation and use of threads to reflect the resources
; we have available, for example the number of available cpu cores according to
; our own tracking.
; The implementation of the multi-threading primitives -- futures, spec-mv-let,
; plet, pargs, pand, and por -- has a dependency structure shown as follows.
; For example, multi-threading primitives are at the base of everything,
; futures and plet/pargs/pand/por are built on top of these primitives, and so
; forth, as indicated by the indentations.
; multi-threading primitives (semaphores, locks, condition variables, etc)
; futures
; spec-mv-let
; waterfall parallelism
; user-level program parallelism (no examples as of April 2012)
; plet, pargs, pand, por
; user-level program parallelism (e.g., community book
; books/parallel/fibonacci.lisp)
; This dependency structure roughly correlates to the following file structure.
; #+acl2-par
; multi-threading-raw.lisp (defines multi-threading primitives)
; parallel-raw.lisp (provides raw Lisp defs. of plet, pargs, pand, and por)
; futures-raw.lisp (defines futures and uses some helper functions
; from parallel-raw.lisp)
; parallel.lisp
; #-acl2-par
; parallel.lisp
; One might wonder how we use threads to execute pieces of parallelism work
; (where "pieces of parallelism work" can mean either futures, bindings of
; plet, arguments of calls surrounded by pargs, or arguments given to pand or
; por). For futures, the story is as follows.
; (1) A primitive adds a piece of parallelism work to one of the two
; parallelism queues (either *future-array* or *work-queue*, as
; appropriate).
;
; (2) The primitive checks to see if there are enough threads already in
; existence to process that piece of parallelism work. If so, the
; primitive returns and execution continues until the result of the
; parallelized computation is needed. If not, the primitive creates one to
; many "worker threads" to consume pieces of parallelism work.
;
; (3) The primitive may eventually need the result from the piece of
; parallelism work. In this case, it will read the value from the piece of
; parallelism work (once it is available) and use it as appropriate. In
; the case that the primitive does not need the value (as can happen with a
; pand/por or a spec-mv-let, when the speculative computation is determined
; to be useless), the primitive will abort (or early terminate) the
; parallel execution of the piece of parallelism work.
;
; When a worker thread is created, it performs the following sequence of
; steps.
;
; (A) Waits until there is a piece of parallelism work to consume. A worker
; thread will wait between 10 and 120 seconds before "giving up", unwinding
; itself, and freeing itself as a resource for the operating system to
; collect. The reader might be tempted to assume that there would
; immediately be work, but this is not guaranteed to be the case (because,
; for efficiency reasons, we typically create a handful more threads than
; are needed).
;
; (B) Waits until there is an idle CPU core available, as determined by our
; resource management using the multi-threading primitives available to us
; in the Lisp (as opposed to trying to tell the operating system how to
; schedule our threads). There is no timeout associated with this wait.
;
; (C) Making it to (C) requires that the thread first made it through (A) and
; then also made it through (B). Thus, the thread has both a piece of
; parallelism work and a CPU core. At this point, the thread executes that
; piece of parallelism work.
;
; (D) Perhaps the piece of parallelism work itself encounters a parallelism
; primitive and decides to further parallelize execution. In this case,
; the worker thread will do (1), (2), and (3), as explained above.
;
; (E) At this point, the worker thread has finished executing the piece of
; parallelism work and stores the result of that execution in the
; appropriate place (e.g., for futures, it stores the execution result in
; the "value" slot of the future).
;
; (F) After performing some cleanup, the thread goes back to (A).
; We use the phrase "Parallelism wart:" to label comments about known issues
; for the #+acl2-par build of ACL2 that we would like to fix, time permitting.
; We also use the phrase "Parallelism blemish:" to identify known issues for
; the #+acl2-par build of ACL2 that we intend to fix only if led to do so by
; user complaints. Finally, we use the phrase "Parallelism no-fix:" to label
; comments about known issues for the #+acl2-par build of ACL2 that we do not
; intend to fix, though we could reclassify these if there are sufficiently
; strong user complaints. Searching through the parallism warts, blemishes,
; and no-fixes could be useful when a user reports a bug in #+acl2-par that
; cannot be replicated in #-acl2-par.
; Parallelism hazards are unrelated to parallelism warts, blemishes, and
; no-fixes. Parallelism hazards are macros or functions that are known to be
; theoretically unsafe when performing multi-threaded execution. We originally
; did not expect users to encounter parallelism hazards (because we should have
; programmed such that the hazards never occur). However, in practice, these
; parallelism hazards are somewhat common and we have disabled the automatic
; warning that occurs everytime a hazard occurs. Once we re-enable that
; warning, in the event that users encounter a parallelism hazard, they will be
; asked to report the associated warning to the ACL2 maintainers. For example,
; if state-global-let* is called while executing concurrently, we want to know
; about it and develop a work-around. See *possible-parallelism-hazards* and
; warn-about-parallelism-hazard for more information.
; #+ACL2-PAR notes contain documentation that only applies to #+acl2-par.
; In an effort to avoid code duplication, we created a definition scheme that
; supports defining both serial and parallel versions of a function with one
; call to a defun-like macro. See the definitions of @par-mappings and
; defun@par for an explanation of this scheme.
; Developer note on emacs and parallelism. When comparing with versions up
; through svn revision 335 (May 27, 2011), it may be useful to ignore "@par"
; when ignoring whitespace with meta-x compare-windows in emacs.
; (setq compare-windows-whitespace "\\(@par\\)?[ \t\n]+")
; To revert to the default behavior:
; (setq compare-windows-whitespace
; "\\(\\s-\\|
; \\)+")
; We indent certain calls as we indent calls of defun. (These forms are in
; emacs/emacs-acl2.el.)
; (put 'er@par 'lisp-indent-function 'defun)
; (put 'warning$@par 'lisp-indent-function 'defun)
; To revert:
; (put 'er@par 'lisp-indent-function nil)
; (put 'warning$@par 'lisp-indent-function nil)
; Only allow the feature :acl2-par in environments that support
; multi-threading. Keep this in sync with the error message about CCL,
; Lispworks, and SBCL in set-parallel-execution-fn and with :doc
; compiling-acl2p. If we add support for non-ANSI GCL, consider providing a
; call of reset-parallelism-variables analogous to the one generated by setting
; *reset-parallelism-variables* in our-abort.
#+(and acl2-par (not ccl) (not (and sbcl sb-thread)) (not lispworks))
(error "It is currently illegal to build the parallel version of ACL2 in this
Common Lisp. See source file acl2-init.lisp for this error message,
which is preceded by information (Lisp features) indicating the legal Lisp
implementations.")
#+akcl
(setq si:*notify-gbc* t)
; The following has been superseded; see the section on reading characters from
; files in acl2.lisp.
; ; Dave Greve reported a problem: the saved_acl2 script in CLISP had characters
; ; that, contrary to expectation, were not being interpreter as newlines. The
; ; CLISP folks explained that "CUSTOM:*DEFAULT-FILE-ENCODING* defaults to :DOS
; ; on cygwin, so #\Newline is printed as '\r\n' (CRLF)." We expect that the
; ; following setting will fix the problem; Dave tried an experiment for us that
; ; seemed to validate this expectation.
; #+clisp
; (setq CUSTOM:*DEFAULT-FILE-ENCODING* :unix)
#+(and lispworks (not acl2-par))
(setq system::*stack-overflow-behaviour*
; The following could reasonably be nil or :warn. David Rager did some
; experiments suggesting that ACL2(p) regressions (as of July 2011) may be more
; robust with the :warn setting. However, that setting causes warnings during
; the build, and it's easy to imagine that ACL2 users would also see that
; cryptic warning -- very un-ACL2-like! So we use nil rather than :warn here.
nil)
#+(and lispworks acl2-par)
(setq system:*stack-overflow-behaviour*
; Since a setting of nil is at least sometimes (if not always) ignored when
; safety is set to 0 (according to an email communication between David Rager
; and Martin Simmons), we choose to use the warn setting for the #+acl2-par
; build.
:warn)
; We have observed a significant speedup with Allegro CL when turning off
; its cross-referencing capability. Here are the times before and after
; evaluating the setq form below, in an example from Dave Greve that spends
; a lot of time loading compiled files.
;
; 165.43 seconds realtime, 163.84 seconds runtime.
; 120.23 seconds realtime, 118.32 seconds runtime.
;
; The user is welcome to edit the form below. Note that it doesn't seem to
; affect the profiler.
#+allegro
(setq excl::*record-xref-info* nil
excl::*load-xref-info* nil
excl::*record-source-file-info* nil
excl::*load-source-file-info* nil)
; Create the packages we use.
(load "acl2.lisp")
; We allow ACL2(h) code to take advantage of Ansi CL features. It's
; conceivable that we don't need this restriction (which only applies to GCL),
; but it doesn't currently seem worth the trouble to figure that out.
#+(and hons (not cltl2))
(progn
(format t "~%ERROR: It is illegal to build the experimental HONS version
of ACL2 in this non-ANSI Common Lisp.~%~%")
(acl2::exit-lisp))
; Fix a bug in SBCL 1.0.49 (https://bugs.launchpad.net/bugs/795705), thanks to
; patch provided by Nikodemus Siivola.
#+sbcl
(in-package :sb-c)
#+sbcl
(when (equal (lisp-implementation-version) "1.0.49")
(without-package-locks
(defun undefine-fun-name (name)
(when name
(macrolet ((frob (type &optional val)
`(unless (eq (info :function ,type name) ,val)
(setf (info :function ,type name) ,val))))
(frob :info)
(frob :type (specifier-type 'function))
(frob :where-from :assumed)
(frob :inlinep)
(frob :kind)
(frob :macro-function)
(frob :inline-expansion-designator)
(frob :source-transform)
(frob :structure-accessor)
(frob :assumed-type)))
(values))
))
; Fix a bug in CMUCL 20D. It seems sad to test (reverse "") twice, but
; attempts to avoid that produced warnings about variable *our-old-reverse*
; being undefined, even when using with-compilation-unit.
#+cmucl
(progn
(when (null (ignore-errors (reverse "")))
(defconstant *our-old-reverse* (symbol-function 'reverse)))
(without-package-locks
(when (boundp '*our-old-reverse*)
(defun reverse (x)
(if (equal x "")
""
(funcall (symbol-value '*our-old-reverse*) x)))
(compile 'reverse))))
; WARNING: The next form should be an in-package (see in-package form for sbcl
; just above).
; Now over to the "ACL2" package for the rest of this file.
(in-package "ACL2")
(defconstant *current-acl2-world-key*
; *Current-acl2-world-key* is the property used for the current-acl2-world
; world. We formerly used a defvar, but there seemed to be no reason to use a
; special variable, which Gary Byers has pointed out takes about 5 instructions
; to read in CCL in order to check if a thread-local binding is dynamically in
; effect. So we tried using a defconstant. Unfortunately, that trick failed
; in Allegro CL; even if we use a boundp test to guard the defconstant, when we
; used make-symbol to create the value; the build failed. So the value is now
; an interned symbol.
'acl2_invisible::*CURRENT-ACL2-WORLD-KEY*)
#+cltl2
(when (not (boundp 'COMMON-LISP::*PRINT-PPRINT-DISPATCH*))
; Many improvements were made to ANSI GCL in May, 2013. If
; COMMON-LISP::*PRINT-PPRINT-DISPATCH* is unbound, then something is wrong with
; this Lisp. In particular, with-standard-io-syntax might not work correctly.
(format t
"ERROR: We do not support building ACL2 in~%~
a host ANSI Common Lisp when variable ~s is unbound. Please~%~
obtain a more recent version of your Lisp implementation."
'COMMON-LISP::*PRINT-PPRINT-DISPATCH*)
(exit-lisp))
#+(and gcl cltl2)
; Deal with undefined cltl2 symbols in ANSI GCL, using values that would be
; assigned by with-standard-io-syntax.
(loop for pair in '((COMMON-LISP::*PRINT-LINES* . nil)
(COMMON-LISP::*PRINT-MISER-WIDTH* . nil)
(COMMON-LISP::*PRINT-RIGHT-MARGIN* . nil)
(COMMON-LISP::*READ-EVAL* . t))
when (not (boundp (car pair)))
do (progn (proclaim `(special ,(car pair)))
(setf (symbol-value (car pair))
(cdr pair))))
; It is a mystery why the following proclamation is necessary, but it
; SEEMS to be necessary in order to permit the interaction of tracing
; with the redefinition of si::break-level.
#+akcl
(declaim (special si::arglist))
#+akcl
(let ((v (symbol-function 'si::break-level)))
(setf (symbol-function 'si::break-level)
(function
(lambda (&rest rst)
(format t "~%Raw Lisp Break.~%")
(apply v rst)))))
(defun system-call (string arguments)
; Warning: Keep this in sync with system-call+.
#+gcl
(si::system
(let ((result string))
(dolist
(x arguments)
(setq result (concatenate 'string result " " x)))
result))
#+lispworks
(system::call-system
(let ((result string))
(dolist
(x arguments)
(setq result (concatenate 'string result " " x)))
result))
#+allegro
(let ((result string))
(dolist
(x arguments)
(setq result (concatenate 'string result " " x)))
#-unix
(excl::shell result)
#+unix
; In Allegro CL in Unix, we can avoid spawning a new shell by calling run-shell-command
; on a simple vector. So we parse the resulting string "cmd arg1 ... argk" and
; run with the simple vector #(cmd cmd arg1 ... argk).
(excl::run-shell-command
(let ((lst nil)
(len (length result))
(n 0))
(loop
(if (>= n len) (return)) ; else get next word
(let ((start n)
(ch (char result n)))
(cond
((member ch '(#\Space #\Tab))
(setq n (1+ n)))
(t (loop
(if (or (>= n len)
(member (setq ch (char result n))
'(#\Space #\Tab)))
(return)
(setq n (1+ n))))
(setq lst (cons (subseq result start n)
lst))))))
(setq result (nreverse lst))
(setq result (coerce (cons (car result) result) 'vector)))))
#+cmu
(ext:process-exit-code
(common-lisp-user::run-program string arguments :output t))
#+sbcl
(sb-ext:process-exit-code
(sb-ext:run-program string arguments :output t :search t))
#+clisp
(let ((result (ext:run-program string :arguments arguments)))
(or result 0))
#+ccl
(let* ((proc (ccl::run-program string arguments :output t))
(status (multiple-value-list (ccl::external-process-status proc))))
(if (not (and (consp status)
(eq (car status) :EXITED)
(consp (cdr status))
(integerp (cadr status))))
1 ; just some non-zero exit code here
(cadr status)))
#-(or gcl lispworks allegro cmu sbcl clisp ccl)
(declare (ignore string arguments))
#-(or gcl lispworks allegro cmu sbcl clisp ccl)
(error "SYSTEM-CALL is not yet defined in this Lisp."))
(defun our-probe-file (filename)
; Use this function instead of probe-file if filename might be a directory.
; We noticed that GCL 2.6.7 on 64-bit Linux doesn't recognize directories with
; probe-file. So we use directory instead, which we have found to work in both
; 32-bit and 64-bit Linux environments.
; BUG: It appears that this function returns nil in GCL 2.6.7 when given an
; existing but empty directory.
#+gcl
(or (probe-file filename)
(let ((x (and (not (equal filename ""))
(cond ((eql (char filename (1- (length filename))) #\/)
filename)
(t (concatenate 'string filename "/"))))))
(directory x)))
#-gcl
(probe-file filename))
(defun copy-distribution (output-file source-directory target-directory
&optional
(all-files "all-files.txt")
(use-existing-target nil))
; We check that all files and directories exist that are supposed to exist. We
; cause an error if not, which ultimately will cause the Unix process that
; calls this function to return an error status, thus halting the make of which
; this operation is a part. Wart: Since probe-file does not check names with
; wildcards, we skip those.
; Note: This function does not actually do any copying or directory creation;
; rather, it creates a file that can be executed.
; FIRST, we make sure we are in the expected directory.
(cond ((not (and (stringp source-directory)
(not (equal source-directory ""))))
(error "The source directory specified for COPY-DISTRIBUTION~%~
must be a non-empty string, but~%~s~%is not."
source-directory)))
(cond ((not (and (stringp target-directory)
(not (equal target-directory ""))))
(error "The target directory specified for COPY-DISTRIBUTION~%must ~
be a non-empty string, but~%~s~%is not. (If you invoked ~
\"make copy-distribution\", perhaps you forgot to set DIR.)"
target-directory)))
(cond ((eql (char source-directory (1- (length source-directory))) #\/)
; In this code we treat all directories as names without the trailing slash.
(setq source-directory
(subseq source-directory 0 (1- (length source-directory))))))
(cond ((not (equal (our-truename (format nil "~a/" source-directory) :safe)
(our-truename
""
"Note: Calling OUR-TRUENAME from COPY-DISTRIBUTION.")))
(error "We expected to be in the directory~%~s~%~
but instead are apparently in the directory~%~s .~%~
Either issue, in Unix, the command~%~
cd ~a~%~
or else edit the file (presumably, makefile) from~%~
which the function COPY-DISTRIBUTION was called,~%~
in order to give it the correct second argument."
source-directory
(our-truename "" t)
source-directory)))
; Next, check that everything exists that is supposed to.
(cond ((and (not use-existing-target)
(our-probe-file target-directory))
(error "Aborting copying of the distribution. The target ~%~
distribution directory~%~s~%~
already exists! You may wish to execute the following~%~
Unix command to remove it and all its contents:~%~
rm -r ~a"
target-directory target-directory)))
(format t "Checking that distribution files are all present.~%")
(let (missing-files)
(with-open-file
(str (concatenate 'string source-directory "/" all-files)
:direction :input)
(let (filename (dir nil))
(loop (setq filename (read-line str nil))
(cond
((null filename) (return))
((or (equal filename "")
(equal (char filename 0) #\#)))
((find #\Tab filename)
(error "Found a line with a Tab in it: ~s" filename))
((find #\Space filename)
(error "Found a line with a Space in it: ~s" filename))
((find #\* filename)
(format t "Skipping wildcard file name, ~s.~%" filename))
((eql (char filename (1- (length filename))) #\:)
; No need to check for directories here; they'll get checked elsewhere. But
; it's harmless enough to do so.
(let* ((new-dir (subseq filename 0 (1- (length filename))))
(absolute-dir
(format nil "~a/~a" source-directory new-dir)))
(cond
((our-probe-file absolute-dir)
(setq dir new-dir))
(t
(setq missing-files
(cons absolute-dir missing-files))
(error "Failed to find directory ~a ."
absolute-dir)))))
(t (let ((absolute-filename
(if dir
(format nil "~a/~a/~a" source-directory dir filename)
(format nil "~a/~a" source-directory filename))))
(cond
((not (our-probe-file absolute-filename))
(setq missing-files
(cons absolute-filename missing-files))
(format t "Failed to find file ~a.~%" absolute-filename)))))))))
(cond
(missing-files
(error "~%Missing the following files (and/or directories):~%~s"
missing-files))
(t (format t "Distribution files are all present.~%"))))
(format t "Preparing to copy distribution files from~%~a/~%to~%~a/ .~%"
source-directory target-directory)
(let (all-dirs)
; In this pass, we look only for directory names.
(with-open-file
(str (concatenate 'string source-directory "/" all-files)
:direction :input)
(let (filename)
(loop (setq filename (read-line str nil))
(cond
((null filename) (return))
((or (equal filename "")
(equal (char filename 0) #\#)))
((find #\Tab filename)
(error "Found a line with a Tab in it: ~s" filename))
((find #\Space filename)
(error "Found a line with a Space in it: ~s" filename))
((eql (char filename (1- (length filename))) #\:)
(setq all-dirs
(cons (subseq filename 0 (1- (length filename)))
all-dirs)))))))
; In the final pass we do our writing.
(with-open-file
(str (concatenate 'string source-directory "/" all-files)
:direction :input)
(with-open-file
(outstr output-file :direction :output)
(let (filename (dir nil))
(if (not use-existing-target)
(format outstr "mkdir ~a~%~%" target-directory))
(loop (setq filename (read-line str nil))
(cond
((null filename) (return))
((or (equal filename "")
(equal (char filename 0) #\#)))
((eql (char filename (1- (length filename))) #\:)
(setq dir (subseq filename 0 (1- (length filename))))
(format outstr "~%mkdir ~a/~a~%"
target-directory dir))
((null dir)
(cond ((not (member filename all-dirs
:test 'equal))
(format outstr "cp -p ~a/~a ~a~%"
source-directory
filename
target-directory))))
(t
(cond ((not (member (format nil "~a/~a"
dir filename)
all-dirs
:test 'equal))
(format outstr "cp -p ~a/~a/~a ~a/~a~%"
source-directory
dir
filename
target-directory
dir)))))))))
(format t "Finished creating a command file for copying distribution files.")))
(defun make-tags ()
#-(or ccl sbcl cmu)
; We disallow ccl and sbcl for the following check. We have found that the
; result of the system-call is a process, (typep <result> 'external-process) in
; ccl and (typep <result> 'sb-impl::process) in sbcl, which can probably be
; made to yield the status. But the status is 0 even for commands not found,
; so why bother? Since cmucl seems to fall victim in the same way as sbcl, we
; treat these two the same here.
(when (not (eql (system-call "which" '("etags")) 0))
(format t "SKIPPING etags: No such program is in the path.")
(return-from make-tags 1))
(system-call "etags"
(let* ((fmt-str
#+(or cmu sbcl clisp ccl) "~a.lisp"
#-(or cmu sbcl clisp ccl) " ~a.lisp")
(lst (append '("acl2.lisp"
"acl2-check.lisp"
"acl2-fns.lisp"
"init.lisp"
"acl2-init.lisp"
"akcl-acl2-trace.lisp"
"allegro-acl2-trace.lisp"
"openmcl-acl2-trace.lisp")
(let ((result nil))
(dolist
(x *acl2-files*)
; Since we don't want to edit doc.lisp, don't go there with tags.
(when (not (equal x "doc.lisp"))
(setq result
(cons (format nil fmt-str x)
result))))
(reverse result)))))
; We want to be sure to include the *-raw.lisp files even if we are not
; building the hons version, in order to assist in maintaining both versions.
(append lst (list "hons-raw.lisp"
"memoize-raw.lisp"
"multi-threading-raw.lisp"
"futures-raw.lisp"
"parallel-raw.lisp"
"serialize-raw.lisp")))))
(defvar *saved-build-date-lst*)
(defvar *saved-mode*)
(defun svn-revision-from-line (s)
; S is a string such as "$Revision: 1053 $" (as in acl2-startup-info.txt) or
; "Revision: 1998" (as printed by "svn info"). In general, it is a string for
; which we want the object that is read immediately after the first #\: . If
; there is none, then we return nil.
(let ((p (position #\: s)))
(and p
(read-from-string s nil nil :start (1+ p)))))
(defconstant *acl2-svn-revision-string*
(let ((file "acl2-startup-info.txt"))
(cond ((probe-file file)
(let ((val (with-open-file
(str file :direction :input)
(read str))))
(cond ((eq val :release)
nil)
((stringp val)
(let ((n (svn-revision-from-line val)))
(or 9999 (error "Unexpected error in getting svn revision ~
from string:~%~s~%"
val))
(format nil
"
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+ WARNING: This is NOT an ACL2 release; it is svn revision ~a. +
+ The authors of ACL2 consider svn distributions to be experimental; +
+ they may be incomplete, fragile, and unable to pass our own +
+ regression tests. Bug reports should include the following line: +
+ ACL2 svn revision ~a; community books svn revision ~a +
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
"
n n "~a")))
(t (error "Illegal value in file ~s: ~s"
file val)))))
(t (error "File ~s appears not to exist." file)))))
(defvar *saved-string*
(concatenate
'string
"~% ~a built ~a.~
~% Copyright (C) 2014, Regents of the University of Texas"
"~% ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you~
~% are welcome to redistribute it under certain conditions. For details,~
~% see the LICENSE file distributed with ACL2.~%"
(or *acl2-svn-revision-string*
; If acl2-startup-info.txt begins with the symbol :release, then
; *acl2-svn-revision-string* is a string with ~a expecting to be bound to the
; svn revision of the books. Otherwise we put "~a" here to be bound to "".
"~a")
"~a"
#+hons
"~%~% Experimental modification for HONS, memoization, and applicative hash~
~% tables.~%"
#+acl2-par
"~%~% Experimental modification for parallel evaluation. Please expect at~
~% most limited maintenance for this version~%"
"~% See the documentation topic ~a for recent changes."
"~% Note: We have modified the prompt in some underlying Lisps to further~
~% distinguish it from the ACL2 prompt.~%"))
(defun maybe-load-acl2-init ()
(let* ((home (our-user-homedir-pathname))
(fl (and home
(probe-file (merge-pathnames home "acl2-init.lsp")))))
(when fl (load fl))))
(defun chmod-executable (sysout-name)
(system-call "chmod" (list "+x" sysout-name)))
(defun saved-build-dates (separator)
(let* ((date-lst (reverse *saved-build-date-lst*))
(result (car date-lst))
(sep (concatenate
'string
(string #\Newline)
(if (eq separator :terminal)
(concatenate
'string
(make-string (+ 3 (length *copy-of-acl2-version*))
:initial-element #\Space)
"then ")
separator))))
(dolist (s (cdr date-lst))
(setq result (concatenate 'string result sep s)))
result))
(defmacro our-with-standard-io-syntax (&rest args)
(cons #-cltl2 'progn
#+cltl2 'with-standard-io-syntax
args))
(defun user-args-string (inert-args &optional (separator '"--"))
; This function is used when saving executable scripts, which may specify that
; certain command line arguments are not to be processed by Lisp (other than to
; affect the value of a variable or function such as
; ccl::*unprocessed-command-line-arguments*; see books/oslib/argv.lisp). Also
; see :doc save-exec. A common convention is that arguments after `--' are not
; processed by Lisp.
(cond ((null inert-args)
"\"$@\"")
((eq inert-args t)
(concatenate 'string separator " \"$@\""))
(t
(concatenate 'string separator " " inert-args " \"$@\""))))
(defmacro write-exec-file (stream prefix string &rest args)
; Prefix is generally nil, but can be (string . fmt-args). String is the
; actual command invocation, with the indicated format args, args.
`(our-with-standard-io-syntax ; Thus, we hope that progn is OK for GCL!
(format ,stream "#!/bin/sh~%~%")
(format ,stream
"# Saved ~a~%~%"
(saved-build-dates "# then "))
,@(and prefix
`((format ,stream ,(car prefix) ,@(cdr prefix))))
(format ,stream
; We generally take Noah Friedman's suggestion of using "exec" since there is
; no reason to keep the saved_acl2 shell script in the process table. However,
; we have seen Windows write out "C:..." as the path of the executable, because
; that is what truename produces. But then the "exec" seems to consider that
; to be a relative pathname, and invoking ./saved_acl2 thus fails. So we
; eliminate the "exec" in Windows; we have found that this works fine, at least
; for GCL and SBCL.
#-mswindows
(concatenate 'string "exec " ,string)
#+mswindows
,string
,@args)))
(defun proclaim-files (&optional outfilename infilename infile-optional-p)
; IMPORTANT: This function assumes that the defconst and defmacro forms in the
; given files have already been evaluated. One way to achieve this state of
; affairs, of course, is to load the files first.
(when (and outfilename infilename)
(error "It is illegal to supply non-nil values for both optional ~
arguments of proclaim-files."))
(when (not *do-proclaims*)
(return-from proclaim-files nil))
(cond
(outfilename
(format t
"Writing proclaim forms for ACL2 source files to file ~s.~%"
outfilename))
(t
(when infilename
(cond ((probe-file infilename)
(format t
"Loading nontrivial generated file of proclaim forms, ~
~s...~%"
infilename)
(load infilename)
(format t
"Completed load of ~s.~%"
infilename)
(return-from proclaim-files nil))
(infile-optional-p) ; fall through as though infilename is nil
(t (error "File ~s is to be loaded by proclaim-files, but does ~
not exist."
infilename))))
(format t
"Generating and evaluating proclaim forms for ACL2 source ~
files.~%")))
(let (str)
(when outfilename
(if (probe-file outfilename)
(delete-file outfilename))
(or (setq str (safe-open outfilename :direction :output))
(error "Unable to open file ~s for output." outfilename)))
; It is tempting to print an in-package form, but we leave that task to
; proclaim-file, which presumably finds the first form to be an in-package
; form.
(dolist (fl *acl2-files*)
(when (not (equal fl "doc.lisp")) ; no need to proclaim that one!
(proclaim-file (format nil "~a.lisp" fl) str)))
(when str ; equivalently, when outfilename is non-nil
(close str))))
(defun insert-string (s)
(cond ((null s) "")
(t (concatenate 'string " " s))))
#+gcl
(defvar *saved-system-banner*
; This variable is only used in GCL 2.6.9 and later, and the following comments
; pertain only to that case.
; Set this variable to nil before save-exec in order to save an image without a
; GCL startup banner, as this will leave si::*system-banner* unbound; see
; below.
; ACL2 keeps this value at nil except when acl2-default-restart unbinds
; si::*system-banner*, in which case *saved-system-banner* is set to the value
; of si::*system-banner* just before that unbinding takes place. When
; save-exec saves an image, it first checks whether si::*system-banner* is
; unbound and *saved-system-banner* is non-nil, in which case it sets
; si::*system-banner* to *saved-system-banner*. Even if si::*system-banner* is
; bound, *saved-system-banner* is set to nil before saving an image.
nil)
#+akcl
(defun save-acl2-in-akcl-aux (sysout-name gcl-exec-name
write-worklispext
set-optimize-maximum-pages
host-lisp-args
inert-args)
(when (and (gcl-version-> 2 6 9 t)
*saved-system-banner*)
(when (not (boundp 'si::*system-banner*)) ; true, unless user intervened
(setq si::*system-banner* *saved-system-banner*))
(setq *saved-system-banner* nil))
(if (and write-worklispext (probe-file "worklispext"))
(delete-file "worklispext"))
(let* ((ext "gcl")
(ext+
; We deal with the apparent fact that Windows implementations of GCL append
; ".exe" to the filename created by save-system.
#+mswindows "gcl.exe"
#-mswindows "gcl")
(gcl-exec-file
(unix-full-pathname gcl-exec-name ext+)))
(if write-worklispext
(with-open-file (str "worklispext" :direction :output)
(format str ext+)))
(if (probe-file sysout-name)
(delete-file sysout-name))
(if (probe-file gcl-exec-file)
(delete-file gcl-exec-file))
(with-open-file (str sysout-name :direction :output)
(write-exec-file str nil "~s~s ~a~%"
gcl-exec-file
(insert-string host-lisp-args)
(user-args-string inert-args)))
(cond ((and set-optimize-maximum-pages
(boundp 'si::*optimize-maximum-pages*))
; We follow a suggestion of Camm Maguire by setting
; 'si::*optimize-maximum-pages* to t just before the save. We avoid the
; combination of 'si::*optimize-maximum-pages* and sgc-on for GCL versions
; through 2.6.3, because of problematic interactions between SGC and
; si::*optimize-maximum-pages*. This issue has been fixed starting with GCL
; 2.6.4. Since si::*optimize-maximum-pages* is only bound starting with
; sub-versions of 2.6, the problem only exists there.
(cond ((or (not (fboundp 'si::sgc-on))
(gcl-version-> 2 6 3))
(setq si::*optimize-maximum-pages* t)))))
(chmod-executable sysout-name)
(si::save-system (concatenate 'string sysout-name "." ext))))
#+akcl
(defun save-acl2-in-akcl (sysout-name gcl-exec-name
&optional mode do-not-save-gcl)
(setq *saved-mode* mode)
(setq *acl2-allocation-alist*
; If *acl2-allocation-alist* is rebound before allocation is done in
; si::*top-level-hook*, e.g., if it is bound in one's init.lisp or
; acl2-init.lsp file, then such binding will override this one. The package
; name shouldn't matter for the keys in user's alist, but in the code below we
; need to keep 'hole in the ACL2 package because we refer to it below.
; Historical Comments:
; Where did these numbers come from? At CLInc we have used the numbers from
; the non-small-p case for some time, and they seem satisfactory. When we
; moved to a "small" image in Version 1.8, we wanted to have roughly the same
; number of free cells as we've had all along, as a default. The cons number
; below is obtained by seeing how many pages we had free (pages in use
; multiplied by percent free, as shown by (room)) the last time we built ACL2,
; before modifying ACL2 to support small images, and adding that to the number
; of pages in use in the small image when no extra pages were allocated at
; start-up. The total was 2917, so that is what we use below. The relocatable
; size is rather arbitrary, and the hole size has been suggested by Bill
; Schelter. Finally, the other numbers were unchanged when we used the same
; algorithm described above for cons (except for fixnum, which came out to 99
; -- close enough!).
; Warning: as of this writing (5/95), there are versions of Linux in which the
; page size is half of that in GCL on a Sparc. In that case, we should double
; the number of pages in each case in order to have the same amount of free
; objects available. We do this below; see the next comment. (We assume that
; there are still the same number of bytes per object; at least, in one
; instance in Linux that appears to be the case for cons, namely, 12 bytes per
; cons.)
; Additional comments during Version_2.9 development:
; When built with GCL 2.6.1-38 and *acl2-allocation-alist* = nil, we have:
; ACL2>(room)
;
; 4972/4972 61.7% CONS RATIO LONG-FLOAT COMPLEX STRUCTURE
; 133/274 14.0% FIXNUM SHORT-FLOAT CHARACTER RANDOM-STATE READTABLE NIL
; 210/462 97.5% SYMBOL STREAM
; 1/2 37.2% PACKAGE
; 69/265 1.0% ARRAY HASH-TABLE VECTOR BIT-VECTOR PATHNAME CCLOSURE FAT-STRING
; 1290/1884 7.4% STRING
; 711/779 0.9% CFUN BIGNUM
; 29/115 82.8% SFUN GFUN CFDATA SPICE NIL
;
; 1302/1400 contiguous (176 blocks)
; 13107 hole
; 5242 0.0% relocatable
;
; 7415 pages for cells
; 27066 total pages