-
Notifications
You must be signed in to change notification settings - Fork 104
/
Copy pathacl2-init.lisp
2469 lines (2133 loc) · 103 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 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 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.
; This file cannot be compiled because it changes packages in the middle.
; We use the static honsing scheme on 64-bit CCL.
#+(and ccl x86_64)
(push :static-hons *features*)
; We use the static honsing scheme on 64-bit GCL when the support is there.
; Actually, with our restriction to GCL Version 2.6.12 and later, we believe
; that the test below will always be true for ANSI GCL.
#+(and gcl x86_64)
(when (and (fboundp 'si::static-inverse-cons)
(fboundp 'si::without-interrupts))
(pushnew :static-hons *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 parallelism 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 every time 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-acl
F438
2p. 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.")
#+gcl
(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 interpreted 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)
#+lispworks
(hcl:extend-current-stack
; For LispWorks, we extend the stack size to avoid stack overflows.
; We have also considered setting system::*stack-overflow-behaviour* to nil (as
; we did in ACL2 Version 7.4 and some (perhaps many) versions earlier -- or
; :warn, as we did similarly for ACL2(p). However, it seems best not to mess
; with the default of :error: a stack overflow seems unlikely to be caught with
; safety 0, and with safety 3, we prefer to see the error rather than having
; the stack automatically extended, so that we can find the offending loop and
; fix it. For example, for the community book books/centaur/truth/perm4.lisp,
; we sent a bug report to LispWorks (during post-7.4 development) for a hang in
; "Computing the guard conjecture for RECORD-ALL-NPN4-PERMS-TOP"; but the
; problem was simply a stack overflow. We didn't catch the problem with safety
; 3 because system::*stack-overflow-behaviour* was nil, so the stack grew
; automatically. Why not set it to nil for safety 0 and :error for safety 3?
; Because perhaps (not sure) when investigating an issue with safety 3, we
; could get stack overflows that aren't actually the problem.
; We choose 20000 somewhat arbitrarily. The value of 400 (representing a 4x
; addition, i.e., increasing the stack by a factor of 5) was insufficient for
; community book books/centaur/aignet/rwlib.lisp (this, before unmemoizing
; bad-lisp-consp): we had to increase the stack 50% seven times in order to
; complete a LD of that book. Since (* 5 (expt 1.5 7)) = 85, we needed to add
; a total of something like 8400% to the default stack size. So 10000 might be
; safe, but 20000 seems safer.
20000)
; 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")
; Now that acl2-fns.lisp has been loaded (by loading acl2.lisp) so that
; getenv$-raw has been defined, we can evaluate the code that may set feature
; :acl2-small-fixnums.
(let* ((smallp (acl2::getenv$-raw "ACL2_SMALL_FIXNUMS"))
(smallp (and smallp
(not (equal smallp "")))))
(cond
((and (>= most-positive-fixnum (1- (expt 2 60)))
(<= most-negative-fixnum (- (expt 2 60)))
(not smallp))
; ACL2 will assume that every fixnum is of type (signed-byte 61),
; hence also of type (unsigned-byte 60) if it is non-negative.
nil)
((and (>= most-positive-fixnum (1- (expt 2 29)))
(<= most-negative-fixnum (- (expt 2 29))))
(cond (smallp
; ACL2 will assume that every fixnum is of type (signed-byte 30),
; hence also of type (unsigned-byte 29) if it is non-negative.
(pushnew :acl2-small-fixnums *features*))
(t
(error "ACL2 generally assumes that all integers that are
at least -2^60 but less than 2^60 are Lisp fixnums,
but that is not the case for this Lisp implementation.
You can defeat this check by setting environment variable
ACL2_SMALL_FIXNUMS to a non-empty value when building the
ACL2 executable. However, such ACL2 builds are not as
fully tested as the usual builds and thus may be less
reliable, and they are not guaranteed to work compatibly
with ordinary ACL2 builds on the same set of books."))))
(t
; The absolute value of most-positive-fixnum or of most-negative-fixnum is too
; sall for ACL2.
(error "This Lisp implementation is not a suitable host for ACL2:
the values of most-negative-fixnum and most-positive-fixnum are
~s and ~s (respectively),
but ACL2 assumes that these have absolute values that are
respectively at least (1- (expt 2 29)) and (expt 2 29), which are
~s and ~s, respectively."
most-positive-fixnum
most-negative-fixnum
(1- (expt 2 29))
(expt 2 29)))))
(acl2::proclaim-optimize)
; 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))
))
; 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.
(exit-with-build-error
"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*))
#+(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.
#+gcl
(declaim (special si::arglist))
#+gcl
(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+.
; Unlike system-call+, we allow an error to occur.
#+gcl
(when (not (fboundp 'si::system))
(exit-with-build-error
"SYSTEM-CALL is not defined in this version of GCL."))
#+gcl
(si::system ; if undefined, ignore compiler warning; see check above
(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::run-shell-commad 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
(let ((ans (ext:process-exit-code
(common-lisp-user::run-program string arguments :output t))))
(if (integerp ans) ans 1))
#+sbcl
(let ((ans (sb-ext:process-exit-code
(sb-ext:run-program string arguments
:output t
:search t))))
(if (integerp ans) ans 1))
#+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 read-file-by-lines (file &optional delete-after-reading)
(let ((acc nil)
(eof '(nil))
missing-newline-p)
(with-open-file
(s file :direction :input)
(loop (multiple-value-bind (line temp)
(read-line s nil eof)
(cond ((eq line eof)
(return acc))
(t
(setq missing-newline-p temp)
(setq acc
(if acc
(concatenate 'string acc (string #\Newline) line)
line)))))))
(when delete-after-reading
(delete-file file))
(if missing-newline-p
acc
(concatenate 'string acc (string #\Newline)))))
(defun getpid$ ()
; This function is intended to return the process id. But it may return nil
; instead, depending on the underlying lisp platform.
(let ((fn
#+allegro 'excl::getpid
#+gcl 'si::getpid
#+sbcl 'sb-unix::unix-getpid
#+cmu 'unix::unix-getpid
#+clisp (or (let ((fn0 (find-symbol "PROCESS-ID" "SYSTEM")))
(and (fboundp fn0) ; CLISP 2.34
fn0))
(let ((fn0 (find-symbol "PROGRAM-ID" "SYSTEM")))
(and (fboundp fn0) ; before CLISP 2.34
fn0)))
#+ccl 'ccl::getpid
#+lispworks 'system::getpid
#-(or allegro gcl sbcl cmu clisp ccl lispworks) nil))
(and fn
(fboundp fn)
(funcall fn))))
(defun system-call+ (string arguments)
; Warning: Keep this in sync with system-call.
; Unlike system-call, we catch Lisp errors and treat the status as 1 in those
; cases.
#-(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.")
#+gcl
(when (not (fboundp 'si::system))
(exit-with-build-error
"SYSTEM-CALL is not defined in this version of GCL."))
(let* (exit-code ; assigned below
#+(or gcl clisp)
(tmp-file (format nil
"~a/tmp~s"
(or (our-ignore-errors
(f-get-global 'tmp-dir *the-live-state*))
"/tmp")
(getpid$)))
(output-string
(our-ignore-errors
#+gcl ; does wildcard expansion
(progn (setq exit-code
; If si::system is undefined, ignore compiler warning; see check above.
(si::system
(let ((result string))
(dolist
(x arguments)
(setq result (concatenate 'string result " " x)))
(concatenate 'string result " > " tmp-file))))
(read-file-by-lines tmp-file t))
#+lispworks ; does wildcard expansion (see comment below)
(with-output-to-string
(s)
(setq exit-code
(system::call-system-showing-output
; It was tempting to use (cons string arguments). This would cause the given
; command, string, to be applied to the given arguments, without involving the
; shell. But then a command such as "ls" would not work; one would have to
; provide a string such as "/bin/ls". So instead of using a list here, we use
; a string, which according to the LispWorks manual will invoke the shell,
; which will find commands (presumably including built-ins and also using the
; user's path).
(let ((result string))
(dolist
(x arguments)
(setq result (concatenate 'string result " " x)))
result)
:output-stream s
:prefix ""
:show-cmd nil
:kill-process-on-abort t)))
#+allegro ; does wildcard expansion
(multiple-value-bind
(stdout-lines stderr-lines exit-status)
(excl.osi::command-output
(let ((result string))
(dolist
(x arguments)
(setq result (concatenate 'string result " " x)))
result))
(declare (ignore stderr-lines))
(setq exit-code exit-status)
(let ((acc nil))
(loop for line in stdout-lines
do
(setq acc
(if acc
(concatenate 'string
acc
(string #\Newline)
line)
line)))
acc))
#+cmu
(with-output-to-string
(s)
(setq exit-code
(let (temp)
(if (progn
(setq temp
(ext:process-exit-code
(common-lisp-user::run-program
string arguments
:output s)))
1)
temp
1))))
#+sbcl
(with-output-to-string
(s)
(setq exit-code
(let (temp)
(if (progn
(setq temp
(sb-ext:process-exit-code
(sb-ext:run-program string arguments
:output s
:search t)))
1)
temp
1))))
#+clisp
(progn (setq exit-code
(or (ext:run-program string
:arguments arguments
:output tmp-file)
0))
(read-file-by-lines tmp-file t))
#+ccl
(with-output-to-string
(s)
(setq exit-code
(let* ((proc
(ccl::run-program string arguments
:output s
:wait 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))))))))
(values (if (integerp exit-code)
exit-code
1)
(if (stringp output-string)
output-string
""))))
(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 (cond ((and (not (equal filename ""))
(eql (char filename (1- (length filename))) #\/))
(subseq filename 0 (1- (length filename))))
(t 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.
; This function calls error rather than exit-with-build-error simply because
; we don't expect it to be called much by users and if a user does call it,
; then it might be from within an existing session, not at build time.
; 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 ()
(when (not (eql (ignore-errors (system-call "which" '("etags"))) 0))
(f
426B
ormat 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)))))
#+acl2-par
lst
#-acl2-par
(append lst (list "multi-threading-raw.lisp"
"futures-raw.lisp"
"parallel-raw.lisp")))))
(defvar *saved-build-date-lst* nil)
(defun git-commit-hash (&optional quiet)
(multiple-value-bind
(exit-code hash)
(ignore-errors (system-call+ "git" '("rev-parse" "HEAD")))
(cond ((and (eql exit-code 0)
(stringp hash))
(coerce (remove #\Newline (coerce hash 'list))
'string))
(quiet nil)
(t (exit-with-build-error "Unable to determine git commit hash.")))))
(defvar *acl2-release-p*
; Notes to developers (users should ignore this!):
; (1) Replace the value below by t when making a release, then to nil after a
; release.
; (2) More generally, see UT CS file
; /projects/acl2/devel-misc/release.cmds
; for release instructions.
nil)
(defun acl2-snapshot-info ()
(let* ((var "ACL2_SNAPSHOT_INFO")
(s (getenv$-raw var))
(err-string
"Unable to determine git commit hash for use in the startup~%~
banner. Consider setting environment variable ACL2_SNAPSHOT_INFO~%~
to a
772D
message to use in its place, or set it to NONE if you simply~%~
want to avoid this error."))
(cond ((and s (string-equal s "NONE"))
(format nil "~% +~72t+"))
((and s (not (equal s "")))
(format nil
"~% + (Note from the environment when this executable was ~
saved:~72t+~% + ~a)~72t+"
s))
(*acl2-release-p* "")
(t (let ((h (git-commit-hash t)))
(cond (h
(format nil
"~% + (Git commit hash: ~a)~72t+"
h))
(t (exit-with-build-error err-string var))))))))
(defvar *saved-string*
(concatenate
'string
"~% ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"
"~% + ~a~72t+"
"~% + built ~a.~72t+"
(acl2-snapshot-info)
"~% + Copyright (C) 2025, Regents of the University of Texas.~72t+"
"~% + ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and~72t+"
"~% + you are welcome to redistribute it under certain conditions. For~72t+"
"~% + details, see the LICENSE file distributed with ACL2.~72t+"
"~% ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++~%"
; Here, we formerly printed "Includes support for hash cons, memoization, and
; applicative hash tables." Now that ACL2(c) is deprecated, we have decided
; that this is no longer appropriate to print (after all, we don't say that
; ACL2 includes support for rewriting).
#+acl2-par
"~%~% Experimental modification for parallel evaluation. Please expect at~
~% most limited maintenance for this version~%"))
(defun maybe-load-acl2-init ()
(let* ((home (our-user-homedir-pathname))
(fl (and home
(probe-file (merge-pathnames home "acl2-init.lsp")))))
(when fl
(format t "; Loading file ~s...~%" fl)
(load fl)
(format t "; Finished loading file ~s.~%" 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)
; See comment about SBCL below.
; Note for GCL: