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
|
; NOTE: An Allegro CL dynamic runtime license is needed in order for this to
; create an Allegro CL ACL2 application acl2.exe in the bin/ directory.
; See target allegro-app in GNUmakefile.
#|
Execute the following form from the ACL2 sources directory, setting the
variable *acl2-application-distributed-books-dir* if necessary as shown below
(probably not necessary).
echo '(generate-application "acl2.exe" (or (sys::getenv "ACL2_BIN_DIR") "app/") (quote ("../build-image.cl")) :runtime :dynamic :include-compiler t)' \
| lisp >& generate-application.log&
Then look at generate-application.log and see if it's OK, especially near the end.
|# ; |
; The file our-develenv.cl will not be distributed with ACL2. It is obtained
; from a path such as <path-to-allegro>/AllegroCL-7.0/acl70/develenv.cl, then
; commenting out those not allowed in runtime images, as suggested in the above
; file.
(load "our-develenv.cl")
(load "init.lisp")
(in-package "ACL2")
; The sources had better already be compiled! The following form just informs
; ACL2 of that fact.
(note-compile-ok)
; We are attempting to replicate the effects of this form from the Makefile:
; (acl2::save-acl2 (quote (acl2::initialize-acl2 (quote acl2::include-book) acl2::*acl2-pass-2-files* t)) "${PREFIXsaved_acl2}")
; From save-acl2
(load-acl2)
(setq *saved-build-date* (saved-build-date-string))
; It is legal to replace nil below by, e.g., "/u/acl2/v2-9/acl2-sources/books/".
(defconstant *acl2-application-distributed-books-dir* nil)
(initialize-acl2 (quote include-book) *acl2-pass-2-files* *acl2-application-distributed-books-dir*)
; Adapted from save-acl2-in-allegro
(setq *saved-mode*
(quote (initialize-acl2 (quote include-book)
*acl2-pass-2-files*
*acl2-application-distributed-books-dir*)))
(tpl:setq-default *PACKAGE* (find-package "ACL2"))
(setq EXCL:*RESTART-INIT-FUNCTION* 'acl2-default-restart)
(load "allegro-acl2-trace.lisp")
; Copied exactly from acl2-init.lisp:
(defvar *acl2-default-restart-complete* nil)
; Copied exactly from acl2-init.lisp:
(defun acl2-default-restart ()
(if *acl2-default-restart-complete*
(return-from acl2-default-restart nil))
(format t *saved-string*
*copy-of-acl2-version*
*saved-build-date*
(cond (*saved-mode*
(format nil "~% Initialized with ~a." *saved-mode*))
(t ""))
(eval '(latest-release-note-string)) ; avoid possible warning
)
(maybe-load-acl2-init)
(in-package "ACL2")
; The following two lines follow the recommendation in Allegro CL's
; documentation file doc/delivery.htm.
#+allegro (tpl:setq-default *package* (find-package "ACL2"))
#+allegro (rplacd (assoc 'tpl::*saved-package*
tpl:*default-lisp-listener-bindings*)
'common-lisp:*package*)
#+allegro (lp)
#+openmcl (eval '(lp)) ; using eval to avoid compiler warning
; See the comment in save-acl2-in-lispworks for why we need the following call.
#+lispworks (mp:initialize-multiprocessing)
;;Lispworks 4.2.0 no longer recognizes the following:
;;#+lispworks (lw::extend-current-stack 1000)
(setq *acl2-default-restart-complete* t)
nil)
; Now optionally include some books.
;(load "/home/kaufmann/foo.fasl")
|
