File: init.lisp

package info (click to toggle)
acl2 8.0dfsg-1
  • links: PTS
  • area: main
  • in suites: buster
  • size: 226,956 kB
  • sloc: lisp: 2,678,900; ansic: 6,101; perl: 5,816; xml: 3,586; cpp: 2,624; ruby: 2,576; makefile: 2,443; sh: 2,312; python: 778; yacc: 764; ml: 763; awk: 260; csh: 186; php: 171; lex: 165; tcl: 44; java: 41; asm: 23; haskell: 17
file content (94 lines) | stat: -rw-r--r-- 4,118 bytes parent folder | download
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
; ACL2 Version 8.0 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2017, 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, init.lisp, is the standard KCL init file.  We use this
; tiny init file, which indirects to akcl-init.lisp, so that we can
; avoid loading in the full init file if it has already been loaded.

; This file need not be distributed with ACL2 and is unimportant for
; the correct operation of ACL2.  This file is loaded automatically by
; ACKL when it starts up, but not by ACL2 when running in any other
; Common Lisp.

; Bob Boyer sometimes uses the following for debugging in CCL:

;(declaim (optimize (safety 3)))
;(setq *print-level* 10)
;(setq *print-length* 10)
;(setq *compile-verbose* t)
;(setq *compile-print* t)
;(setq *load-print* t)
;(setq *load-verbose* t)
;(setq ccl:*trace-print-level* 10)
;(setq ccl:*trace-print-length* 10)
;(setq ccl::*backtrace-print-length* 10)
;(setq ccl::*backtrace-print-level* 10)

(unless (find-package "ACL2")

; File acl2r.lisp is created by GNUmakefile, though the user could create it
; directly.  Its name derives from its initial purpose, which was simply to
; push :non-standard-analysis onto *features*.  We use it now for all sorts of
; things, though; see GNUmakefile.

  (if (probe-file "acl2r.lisp") (load "acl2r.lisp"))
  #+sbcl ; keep this in sync with with-warnings-suppressed
  (handler-bind
   ((style-warning (lambda (c)
                     (declare (ignore c))
                     (invoke-restart 'muffle-warning))))
   (load "acl2-init.lisp"))
  #-sbcl
  (load "acl2-init.lisp"))

; We may need a bigger stack than the default, as evidenced by the failure of
; the event (verify-guards read-utf8-fast ...) in community book
; books/unicode/read-utf8.lisp.  We handle this issue here for GCL, and
; elsewhere for some other lisps.  However, we have seen GCL 2.6.6 on Windows
; break here, so we skip the stack adjustment for Windows.

#+gcl
(progn
  (defvar *acl2-gcl-multiply-stacks-evaluated* nil)
  (when (not *acl2-gcl-multiply-stacks-evaluated*)

; Formerly we multiplied by 2.  But the following problems then bit us in
; ACL2(h).  Certification of community book books/arithmetic-5/top.lisp caused
; a stack overflow because of function pkg-names-memoize;
; books/misc/hons-tests.lisp had a stack overflow because of a memoized
; fibonacci function call; and a stack overflow for
; books/clause-processors/SULFA/books/sat-tests/sudoku.lisp was caused by
; bad-lisp-objectp.  Another doubling fixed each of these, but wasn't enough for
; certifying books/centaur/aig/random-sim.lisp, again because of
; pkg-names-memoize.  So we now multiply by 8.  Camm Maguire has suggested that
; these problems might be solved by avoiding the use of interpreted code, and
; we considered investigating whether that might be done (e.g., by adding (comp
; t) events) in the cases above.  But we see no harm in simply increasing the
; stack size, which could be of benefit in cases where users execute uncompiled
; code.  And besides, when we start ACL2(h) built on GCL we find that
; (symbol-function 'pkg-names-memoize) is compiled.

    (setq si::*multiply-stacks* 8))
  (setq *acl2-gcl-multiply-stacks-evaluated* t))

; Suggestion from Camm Maguire, 6/28/06 (GCL 2.6.7 and beyond), for improved
; efficiency; seconded by Bob Boyer.
#+gcl
(declaim (ftype (function (seqind t) t) si::set-mv))