← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to init.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
init.lisp
1
 
; ACL2 Version 6.5 -- A Computational Logic for Applicative Common Lisp
2
 
; Copyright (C) 2014, Regents of the University of Texas
 
1
; ACL2 Version 7.0 -- A Computational Logic for Applicative Common Lisp
 
2
; Copyright (C) 2015, Regents of the University of Texas
3
3
 
4
4
; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
5
5
; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.
43
43
 
44
44
(unless (find-package "ACL2")
45
45
 
46
 
; File acl2r.lisp is created by the makefile, though the user could create it
47
 
; directly (which may be useful in non-Unix environment when make is not
48
 
; available).  It isn't necessary to create this file, however, when one is
49
 
; building a standard image, since all it does it push :non-standard-analysis
50
 
; onto *features*.  (It IS necessary however, when building a standard image,
51
 
; NOT to have acl2r.lisp around if it pushes that feature!)
 
46
; File acl2r.lisp is created by GNUmakefile, though the user could create it
 
47
; directly.  Its name derives from its initial purpose, which was simply to
 
48
; push :non-standard-analysis onto *features*.  We use it now for all sorts of
 
49
; things, though; see GNUmakefile.
52
50
 
53
51
  (if (probe-file "acl2r.lisp") (load "acl2r.lisp"))
54
52
  #+sbcl ; keep this in sync with with-warnings-suppressed
94
92
; Suggestion from Camm Maguire, 6/28/06 (GCL 2.6.7 and beyond), for improved
95
93
; efficiency; seconded by Bob Boyer.
96
94
#+gcl
97
 
(when (acl2::gcl-version->= 2 6 7)
98
 
  (declaim (ftype (function (seqind t) t) si::set-mv)))
 
95
(declaim (ftype (function (seqind t) t) si::set-mv))