rpms/pvs-sbcl/F-11 pvs-4.2-ansi.patch, NONE, 1.1 pvs-4.2-autoconf.patch, NONE, 1.1 pvs-4.2-build-id.patch, NONE, 1.1 pvs-4.2-emacs.patch, NONE, 1.1 pvs-4.2-latex.patch, NONE, 1.1 pvs-4.2-mona.patch, NONE, 1.1 pvs-4.2-sbcl.patch, NONE, 1.1 pvs-sbcl.desktop, NONE, 1.1 pvs-sbcl.spec, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2
Jerry James
jjames at fedoraproject.org
Mon Jan 4 22:20:57 UTC 2010
- Previous message (by thread): rpms/libselinux/F-12 libselinux.spec,1.378,1.379 sources,1.191,1.192
- Next message (by thread): rpms/pvs-sbcl/devel pvs-4.2-ansi.patch, NONE, 1.1 pvs-4.2-autoconf.patch, NONE, 1.1 pvs-4.2-build-id.patch, NONE, 1.1 pvs-4.2-emacs.patch, NONE, 1.1 pvs-4.2-latex.patch, NONE, 1.1 pvs-4.2-mona.patch, NONE, 1.1 pvs-4.2-sbcl.patch, NONE, 1.1 pvs-sbcl.desktop, NONE, 1.1 pvs-sbcl.spec, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
Author: jjames
Update of /cvs/pkgs/rpms/pvs-sbcl/F-11
In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv13599/F-11
Modified Files:
.cvsignore sources
Added Files:
pvs-4.2-ansi.patch pvs-4.2-autoconf.patch
pvs-4.2-build-id.patch pvs-4.2-emacs.patch pvs-4.2-latex.patch
pvs-4.2-mona.patch pvs-4.2-sbcl.patch pvs-sbcl.desktop
pvs-sbcl.spec
Log Message:
Initial checkin.
pvs-4.2-ansi.patch:
ess/allegro-runtime.lisp | 2 +-
ess/lang/ab-term/rel/af-runtime.lisp | 2 +-
ess/lang/ab-term/rel/af-top.lisp | 2 +-
ess/lang/sb-term/rel/access-par.lisp | 2 +-
ess/lang/sb-term/rel/access.lisp | 20 ++++++++++----------
ess/lang/sb-term/rel/aux-funs.lisp | 4 ++--
ess/lang/sb-term/rel/flatten.lisp | 2 +-
ess/lang/sb-term/rel/new-rt-format.lisp | 6 +++---
ess/lang/sb-term/rel/old-rt-format.lisp | 6 +++---
ess/lang/sb-term/rel/old-rt-unp-structs.lisp | 4 ++--
ess/lang/sb-term/rel/old-rt-unparse.lisp | 8 ++++----
ess/lang/sb-term/rel/rt-format.lisp | 6 +++---
ess/lang/sb-term/rel/rt-lex.lisp | 2 +-
ess/lang/sb-term/rel/rt-parse-mac.lisp | 4 ++--
ess/lang/sb-term/rel/rt-term.lisp | 2 +-
ess/lang/sb-term/rel/rt-unp-structs.lisp | 4 ++--
ess/lang/sb-term/rel/rt-unparse.lisp | 8 ++++----
ess/lang/sb-term/rel/unparse-gen.lisp | 8 ++++----
ess/sys/constr/rel/constr.lisp | 2 +-
ess/sys/ergolisp/rel/dlambda.lisp | 2 +-
ess/sys/ergolisp/rel/ergo-system.lisp | 2 +-
ess/sys/ergolisp/rel/type-check.lisp | 2 +-
ess/sys/tools/rel/box.lisp | 4 ++--
ess/sys/tools/rel/retry.lisp | 2 +-
ess/term/attr/rel/attr-lang.lisp | 6 +++---
ess/term/attr/rel/attr-lib.lisp | 2 +-
ess/term/attr/rel/attr-sort.lisp | 6 +++---
ess/term/language/rel/languages.lisp | 4 ++--
ess/term/terms/rel/occur.lisp | 6 +++---
ess/term/terms/rel/opers.lisp | 2 +-
ess/term/terms/rel/sorts.lisp | 6 +++---
ess/term/terms/rel/terms.lisp | 6 +++---
ess/term/trep/rel/attr-prims.lisp | 2 +-
ess/term/trep/rel/gterm.lisp | 2 +-
pvs-config.lisp | 4 ++--
pvs.system | 4 ++--
src/defcl.lisp | 8 ++++----
src/defsystem.lisp | 14 +++++++-------
src/globals.lisp | 2 +-
src/interface/allegro.lisp | 2 +-
src/interface/cl-ilisp.lisp | 2 +-
src/macros.lisp | 2 +-
src/make-allegro-pvs.lisp | 2 +-
src/make-pvs-methods.lisp | 2 +-
src/make-pvs-parser.lisp | 2 +-
src/metering.lisp | 12 ++++++------
src/prover/strategies.lisp | 2 +-
src/utils/file-utils.lisp | 4 ++--
48 files changed, 105 insertions(+), 105 deletions(-)
--- NEW FILE pvs-4.2-ansi.patch ---
diff -dur pvs-4.2.ORIG/ess/allegro-runtime.lisp pvs-4.2/ess/allegro-runtime.lisp
--- pvs-4.2.ORIG/ess/allegro-runtime.lisp 2006-09-12 13:46:53.000000000 -0600
+++ pvs-4.2/ess/allegro-runtime.lisp 2010-01-04 13:32:05.215925367 -0700
@@ -1,5 +1,5 @@
#+allegro
-(eval-when (eval load)
+(eval-when (:execute :load-toplevel)
(setq system:*load-search-list*
(list #p"" #p(:type "lfasl") #p(:type "cl") #p(:type "lisp"))))
(defvar *ess-path*
diff -dur pvs-4.2.ORIG/ess/lang/ab-term/rel/af-runtime.lisp pvs-4.2/ess/lang/ab-term/rel/af-runtime.lisp
--- pvs-4.2.ORIG/ess/lang/ab-term/rel/af-runtime.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/lang/ab-term/rel/af-runtime.lisp 2010-01-04 13:32:05.215925367 -0700
@@ -25,7 +25,7 @@
;;; 07-22-87 rln Initial development release.
;;;
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
(unless (find-package "AF-RUNTIME-LIB")
(make-package "AF-RUNTIME-LIB"
:nicknames '("ABRT" "AFRT")
diff -dur pvs-4.2.ORIG/ess/lang/ab-term/rel/af-top.lisp pvs-4.2/ess/lang/ab-term/rel/af-top.lisp
--- pvs-4.2.ORIG/ess/lang/ab-term/rel/af-top.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/lang/ab-term/rel/af-top.lisp 2010-01-04 13:32:05.216926010 -0700
@@ -85,7 +85,7 @@
nil))))
-(eval-when (compile eval)
+(eval-when (:compile-toplevel :execute)
(defmacro ab-read-line ()
`(string-trim '(#\space #\tab) (read-line)))
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/access.lisp pvs-4.2/ess/lang/sb-term/rel/access.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/access.lisp 2010-01-04 13:30:14.576611529 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/access.lisp 2010-01-04 13:32:05.217738919 -0700
@@ -132,7 +132,7 @@
*sb-package*))))
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
;; The following were originally destructive versions of the above, but my
;; timing tests show that you don't gain that much and I'm worried about
@@ -197,7 +197,7 @@
nil)))
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro grammar-new-line-comment-char (grammar)
`(grammar-comment-chars 0 ,grammar))
@@ -357,7 +357,7 @@
pat))
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro get-nt-slot-total (nt-term)
`(get-sb-attr ,nt-term 'slots))
@@ -436,7 +436,7 @@
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro get-nt-left-bracket (nt-name grammar)
`(get-nt-bracket ,nt-name ,grammar 'left-bracket))
@@ -485,7 +485,7 @@
;;; Precedence access (con.)
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro get-nt-prec-initials (nt-name grammar)
`(nth 0 (get-nt-prec ,nt-name ,grammar)))
(defmacro get-nt-prec-medial-lefts (nt-name grammar)
@@ -604,7 +604,7 @@
(defparameter pattern-ops (make-hash-table :test #'eq :size (expt 2 8)))
-(eval-when (load eval)
+(eval-when (:load-toplevel :execute)
(mapcar #'(lambda (x)
(setf (gethash x pattern-ops) t))
pattern-op-list))
@@ -750,7 +750,7 @@
(ds-id (term-arg1 pat))))))))
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro pattern-tag (pat)
`(pattern-name ,pat))
@@ -875,7 +875,7 @@
pat))
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
;; There is a compiler error for mapcan.
(defun map-pattern (pat funct)
(if (pattern-p pat)
@@ -927,7 +927,7 @@
(defparameter augment-ops (make-hash-table :test #'eq :size (expt 2 8)))
-(eval-when (load eval)
+(eval-when (:load-toplevel :execute)
(mapcar #'(lambda (x)
(setf (gethash x augment-ops) t))
augment-op-list))
@@ -1005,7 +1005,7 @@
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro augment-args (aug)
`(augment-sons ,aug))
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/access-par.lisp pvs-4.2/ess/lang/sb-term/rel/access-par.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/access-par.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/access-par.lisp 2010-01-04 13:32:05.218926226 -0700
@@ -49,7 +49,7 @@
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro atomic (pat)
`(memq (get-kind ,pat)
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/aux-funs.lisp pvs-4.2/ess/lang/sb-term/rel/aux-funs.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/aux-funs.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/aux-funs.lisp 2010-01-04 13:32:05.219780041 -0700
@@ -127,7 +127,7 @@
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro sb-write (&rest write-calls)
`(let ((*package* *sb-package*)
(*print-level* nil)
@@ -331,7 +331,7 @@
(sb-intern-nupcase (format nil "V~D" x)))
-(eval-when (load compile eval)
+(eval-when (:load-toplevel :compile-toplevel :execute)
(defmacro get-number (fragment)
`(car ,fragment))
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/flatten.lisp pvs-4.2/ess/lang/sb-term/rel/flatten.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/flatten.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/flatten.lisp 2010-01-04 13:32:05.220926450 -0700
@@ -365,7 +365,7 @@
(defun make-and (as-list)
; get rid of extra nulls.
- (delete-if #'null as-list)
+ (setq as-list (delete-if #'null as-list))
(if (> (length as-list) 1)
(make-augment :kind 'and :args as-list)
(car as-list)))
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/new-rt-format.lisp pvs-4.2/ess/lang/sb-term/rel/new-rt-format.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/new-rt-format.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/new-rt-format.lisp 2010-01-04 13:32:05.221783462 -0700
@@ -48,7 +48,7 @@
(defvar *sb-fontheight* sb-deffontheight)
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro sb-chars-to-pixels (chars)
`(* (the fixnum *sb-fontwidth*) ,chars))
@@ -95,7 +95,7 @@
; Changes if original nesting will not
; work.
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro indent-width (units)
`(* *indent-unit-width* ,units)))
@@ -301,7 +301,7 @@
)
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro tinfo-bp-value (tinfo)
`(bp-value (tinfo-bp ,tinfo)))
(defmacro tinfo-bp-united-flag (tinfo)
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/old-rt-format.lisp pvs-4.2/ess/lang/sb-term/rel/old-rt-format.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/old-rt-format.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/old-rt-format.lisp 2010-01-04 13:32:05.222926189 -0700
@@ -48,7 +48,7 @@
(defvar *sb-fontheight* sb-deffontheight)
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro sb-chars-to-pixels (chars)
`(* *sb-fontwidth* ,chars))
@@ -93,7 +93,7 @@
; Changes if original nesting will not
; work.
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro indent-width (units)
`(* *indent-unit-width* ,units)))
@@ -293,7 +293,7 @@
)
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro tinfo-bp-value (tinfo)
`(bp-value (tinfo-bp ,tinfo)))
(defmacro tinfo-bp-united-flag (tinfo)
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/old-rt-unparse.lisp pvs-4.2/ess/lang/sb-term/rel/old-rt-unparse.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/old-rt-unparse.lisp 1994-10-04 20:10:52.000000000 -0600
+++ pvs-4.2/ess/lang/sb-term/rel/old-rt-unparse.lisp 2010-01-04 13:32:05.223778102 -0700
@@ -133,7 +133,7 @@
;;; Generic macros.
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro dis-op (op x)
`(equal ,op
@@ -158,7 +158,7 @@
;;; Stack routines for unparsing abstract syntax.
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro init-as-stack ()
nil)
@@ -596,7 +596,7 @@
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro dis-lt (kind as)
`(funcall *apply-LT-dis-fun*
@@ -827,7 +827,7 @@
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro nt-unp (nt-name as body)
`(let* ((*uterm-nt-name* ,nt-name)
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/old-rt-unp-structs.lisp pvs-4.2/ess/lang/sb-term/rel/old-rt-unp-structs.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/old-rt-unp-structs.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/old-rt-unp-structs.lisp 2010-01-04 13:32:05.224644692 -0700
@@ -107,7 +107,7 @@
(format stream "#<oct>")))
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
(defmacro width (oct)
`(- (rightx ,oct) (leftx ,oct)))
@@ -175,7 +175,7 @@
;(format stream "#<aw>")
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro aw-term (aw)
`(uterm-term (aw-uterm ,aw)))
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/rt-format.lisp pvs-4.2/ess/lang/sb-term/rel/rt-format.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/rt-format.lisp 2001-06-26 04:46:33.000000000 -0600
+++ pvs-4.2/ess/lang/sb-term/rel/rt-format.lisp 2010-01-04 13:32:05.225646042 -0700
@@ -48,7 +48,7 @@
(defvar *sb-fontheight* sb-deffontheight)
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro sb-chars-to-pixels (chars)
`(* *sb-fontwidth* ,chars))
@@ -93,7 +93,7 @@
; Changes if original nesting will not
; work.
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro indent-width (units)
`(* *indent-unit-width* ,units)))
@@ -293,7 +293,7 @@
)
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro tinfo-bp-value (tinfo)
`(bp-value (tinfo-bp ,tinfo)))
(defmacro tinfo-bp-united-flag (tinfo)
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/rt-lex.lisp pvs-4.2/ess/lang/sb-term/rel/rt-lex.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/rt-lex.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/rt-lex.lisp 2010-01-04 13:32:05.225646042 -0700
@@ -49,7 +49,7 @@
;;; export different symbols from the LISP package, so it is important that
;;; the SBST package does not use the LISP package, so we can get repeatable
;;; behavior on different machines.
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
(defvar *sbst-package*
(cond ((find-package "SBST"))
(t
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/rt-parse-mac.lisp pvs-4.2/ess/lang/sb-term/rel/rt-parse-mac.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/rt-parse-mac.lisp 2001-06-26 04:46:33.000000000 -0600
+++ pvs-4.2/ess/lang/sb-term/rel/rt-parse-mac.lisp 2010-01-04 13:32:05.226643105 -0700
@@ -43,7 +43,7 @@
(export '(rbp))
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
;;; Determine whether this entry in a fs-list allows an epsilon for the second
;;; token. The "rt" in the name is to avoid a name conflict with an SB routine
@@ -73,7 +73,7 @@
;;; otherwise error and return nil. It isn't clear whether the original code
;;; always returned nil when an error occurred.
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro lam (fs-list &body code)
(if code
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/rt-term.lisp pvs-4.2/ess/lang/sb-term/rel/rt-term.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/rt-term.lisp 2009-07-30 23:54:17.224091000 -0600
+++ pvs-4.2/ess/lang/sb-term/rel/rt-term.lisp 2010-01-04 13:32:05.228636235 -0700
@@ -33,7 +33,7 @@
;;; the SBST package does not use the LISP package, so we can get repeatable
;;; behavior on different machines.
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
(defvar *sbst-package*
(cond ((find-package "SBST"))
(t
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/rt-unparse.lisp pvs-4.2/ess/lang/sb-term/rel/rt-unparse.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/rt-unparse.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/rt-unparse.lisp 2010-01-04 13:32:05.229637055 -0700
@@ -135,7 +135,7 @@
;;; Generic macros.
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro dis-op (op x)
`(equal ,op
@@ -160,7 +160,7 @@
;;; Stack routines for unparsing abstract syntax.
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro init-as-stack ()
nil)
@@ -602,7 +602,7 @@
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro dis-lt (kind as)
`(funcall *apply-lt-dis-fun*
@@ -836,7 +836,7 @@
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro nt-unp (nt-name as body)
`(let* ((*uterm-nt-name* ,nt-name)
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/rt-unp-structs.lisp pvs-4.2/ess/lang/sb-term/rel/rt-unp-structs.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/rt-unp-structs.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/rt-unp-structs.lisp 2010-01-04 13:32:05.229637055 -0700
@@ -107,7 +107,7 @@
(format stream "#<oct>")))
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
(defmacro width (oct)
`(- (rightx ,oct) (leftx ,oct)))
@@ -176,7 +176,7 @@
;(format stream "#<aw>")
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro aw-term (aw)
`(uterm-term (aw-uterm ,aw)))
diff -dur pvs-4.2.ORIG/ess/lang/sb-term/rel/unparse-gen.lisp pvs-4.2/ess/lang/sb-term/rel/unparse-gen.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/unparse-gen.lisp 2004-12-08 16:07:08.000000000 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/unparse-gen.lisp 2010-01-04 13:32:05.230617604 -0700
@@ -17,7 +17,7 @@
(in-package :syntax-box) (use-package :ergolisp)
-(eval-when (eval compile load)
+(eval-when (:execute :compile-toplevel :load-toplevel)
(defmacro map-append (function &rest lists)
`(do ((list-to-append
@@ -68,7 +68,7 @@
string)))))
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro mk-bracket-table-name ()
`(mk-conc-var-name "BRACKET-INFO"))
@@ -248,7 +248,7 @@
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro keyword-intern (x)
`(let ((x ,x))
(intern (if (stringp x)
@@ -983,7 +983,7 @@
t))
((plus star and)
- (error "Illegal augment for choose-discriminator:" aug))
+ (error "Illegal augment for choose-discriminator:~%~S~%" aug))
(term-const
(cond ((has-elist-arg? aug) ; routines imported from sort-gen.
diff -dur pvs-4.2.ORIG/ess/sys/constr/rel/constr.lisp pvs-4.2/ess/sys/constr/rel/constr.lisp
--- pvs-4.2.ORIG/ess/sys/constr/rel/constr.lisp 2006-08-02 01:36:30.000000000 -0600
+++ pvs-4.2/ess/sys/constr/rel/constr.lisp 2010-01-04 13:32:05.231695899 -0700
@@ -31,7 +31,7 @@
image). This doesn't work. It always insists on inline expanding.")
(defmacro proclaim-constrs-inline (flag)
- `(eval-when (compile load eval)
+ `(eval-when (:compile-toplevel :load-toplevel :execute)
(setq *proclaim-constrs-inline* ,flag)))
diff -dur pvs-4.2.ORIG/ess/sys/ergolisp/rel/dlambda.lisp pvs-4.2/ess/sys/ergolisp/rel/dlambda.lisp
--- pvs-4.2.ORIG/ess/sys/ergolisp/rel/dlambda.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/sys/ergolisp/rel/dlambda.lisp 2010-01-04 13:32:05.232616636 -0700
@@ -117,7 +117,7 @@
(values selectors (length selectors)))
`(progn
(defreconstr ,constr ,arg-cnt :equal ,equal)
- (eval-when (compile load eval)
+ (eval-when (:compile-toplevel :load-toplevel :execute)
(setf (get-constructor-info ',constr)
(list ',sel-spec
',discrim))))))
diff -dur pvs-4.2.ORIG/ess/sys/ergolisp/rel/ergo-system.lisp pvs-4.2/ess/sys/ergolisp/rel/ergo-system.lisp
--- pvs-4.2.ORIG/ess/sys/ergolisp/rel/ergo-system.lisp 2006-08-02 01:36:30.000000000 -0600
+++ pvs-4.2/ess/sys/ergolisp/rel/ergo-system.lisp 2010-01-04 13:32:05.233642604 -0700
@@ -128,7 +128,7 @@
(when (probe-file file-name)
(rename-file file-name next-file-name))))
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro ergo-ignore-if-unused (&rest vars)
#+excl ; for allegro
nil ;;`(declare (excl:ignore-if-unused , at vars))
diff -dur pvs-4.2.ORIG/ess/sys/ergolisp/rel/type-check.lisp pvs-4.2/ess/sys/ergolisp/rel/type-check.lisp
--- pvs-4.2.ORIG/ess/sys/ergolisp/rel/type-check.lisp 2006-08-02 01:36:30.000000000 -0600
+++ pvs-4.2/ess/sys/ergolisp/rel/type-check.lisp 2010-01-04 13:32:05.233642604 -0700
@@ -48,7 +48,7 @@
"Expands to nothing, but saves something on the property list of
NAME. This can be used on the top level, or as the first thing in
a DEFUN."
- `(eval-when (compile load eval)
+ `(eval-when (:compile-toplevel :load-toplevel :execute)
(setf (get ',name 'type-info) (cons ',argtypes ',resulttypes))))
(defmacro declare-ftype (name argtypes &rest resulttypes)
diff -dur pvs-4.2.ORIG/ess/sys/tools/rel/box.lisp pvs-4.2/ess/sys/tools/rel/box.lisp
--- pvs-4.2.ORIG/ess/sys/tools/rel/box.lisp 2006-08-02 01:36:30.000000000 -0600
+++ pvs-4.2/ess/sys/tools/rel/box.lisp 2010-01-04 13:32:05.234646805 -0700
@@ -269,7 +269,7 @@
(defun \#> ()
(set-dispatch-macro-character #\# #\> #'box-reader))
-(eval-when (load eval)
+(eval-when (:load-toplevel :execute)
(\#>))
(defun box-cerror (continue-string format-string &rest args)
@@ -327,7 +327,7 @@
(def-disksave-hook (setq *null-output* (make-broadcast-stream)))
-(eval-when (load eval)
+(eval-when (:load-toplevel :execute)
(if (streamp *null-output*)
*null-output*
(setq *null-output* (make-broadcast-stream))))
diff -dur pvs-4.2.ORIG/ess/sys/tools/rel/retry.lisp pvs-4.2/ess/sys/tools/rel/retry.lisp
--- pvs-4.2.ORIG/ess/sys/tools/rel/retry.lisp 2006-08-02 01:36:30.000000000 -0600
+++ pvs-4.2/ess/sys/tools/rel/retry.lisp 2010-01-04 13:32:05.235631096 -0700
@@ -21,7 +21,7 @@
;;; First a lucid 2.1 bug workaround.
#+(or (and lucid (not lcl3.0)) harlequin-common-lisp)
-(eval-when (load compile eval)
+(eval-when (:load-toplevel :compile-toplevel :execute)
(dolist (s '("*catchers*" "retry" "retry-catch" "reinit-retry-catch"))
(export (list (intern s :lisp)) :lisp)))
diff -dur pvs-4.2.ORIG/ess/term/attr/rel/attr-lang.lisp pvs-4.2/ess/term/attr/rel/attr-lang.lisp
--- pvs-4.2.ORIG/ess/term/attr/rel/attr-lang.lisp 1994-10-05 14:23:17.000000000 -0600
+++ pvs-4.2/ess/term/attr/rel/attr-lang.lisp 2010-01-04 13:32:05.236634549 -0700
@@ -30,7 +30,7 @@
(defmacro defcon (con-name lang-name &optional (doc-string ""))
"Predefines a context."
(let ((deltafun (deltafun-fam-name con-name :global)))
- `(eval-when (compile load eval)
+ `(eval-when (:compile-toplevel :load-toplevel :execute)
(setf (gethash ',con-name *context-table*)
(make-context-family
:name ',con-name
@@ -42,7 +42,7 @@
(defmacro defsyn (syn-name lang-name con-name &optional (doc-string ""))
"Predefines a syntext depending on a context."
(let ((compfun (compfun-fam-name syn-name :global)))
- `(eval-when (compile load eval)
+ `(eval-when (:compile-toplevel :load-toplevel :execute)
(let* ((con
(sometable-lookup ',con-name *context-table*
,(format nil "The context ~S on which the syntext ~~S
@@ -63,7 +63,7 @@
(defmacro defattr (attr-name lang-name syn-name &optional (doc-string ""))
"Predefines an attribute by declaring the syntext it depends on."
(let ((attrfun (attrfun-fam-name attr-name :global)))
- `(eval-when (compile load eval)
+ `(eval-when (:compile-toplevel :load-toplevel :execute)
(let* ((syn
(sometable-lookup ',syn-name *syntext-table*
,(format nil "The syntext ~S on which the attribute ~~S
diff -dur pvs-4.2.ORIG/ess/term/attr/rel/attr-lib.lisp pvs-4.2/ess/term/attr/rel/attr-lib.lisp
--- pvs-4.2.ORIG/ess/term/attr/rel/attr-lib.lisp 1994-10-05 14:23:17.000000000 -0600
+++ pvs-4.2/ess/term/attr/rel/attr-lib.lisp 2010-01-04 13:32:05.236634549 -0700
@@ -22,7 +22,7 @@
(defconstant undefined 'undefined)
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
(defun is-underline (form)
(and (symbolp form) (string-equal (symbol-name form) "_")))
diff -dur pvs-4.2.ORIG/ess/term/attr/rel/attr-sort.lisp pvs-4.2/ess/term/attr/rel/attr-sort.lisp
--- pvs-4.2.ORIG/ess/term/attr/rel/attr-sort.lisp 2006-08-02 01:36:30.000000000 -0600
+++ pvs-4.2/ess/term/attr/rel/attr-sort.lisp 2010-01-04 13:32:05.237636052 -0700
@@ -116,7 +116,7 @@
(mapcar #'(lambda (sort)
(cons sort (deltafun-fam-name confam-name sort)))
sortlist)))
- `(eval-when (compile load eval)
+ `(eval-when (:compile-toplevel :load-toplevel :execute)
(setf (gethash ',confam-name *context-table*)
(make-context-family
:name ',confam-name
@@ -143,7 +143,7 @@
(defmacro defsynfam (synfam-name lang-name confam-name
&optional (doc-string ""))
"Predefines a syntext family depending on a context family."
- `(eval-when (compile load eval)
+ `(eval-when (:compile-toplevel :load-toplevel :execute)
(let* ((con-fam
(sometable-lookup ',confam-name *context-table*
,(format nil "The context family ~S on which the syntext family ~~S
@@ -187,7 +187,7 @@
(defmacro defattrfam (attrfam-name lang-name synfam-name
&optional (doc-string ""))
"Predefines an attribute family depending on a syntext family."
- `(eval-when (compile load eval)
+ `(eval-when (:compile-toplevel :load-toplevel :execute)
(let* ((syn-fam
(sometable-lookup ',synfam-name *syntext-table*
,(format nil "The syntext family ~S on which the attribute family ~~S
diff -dur pvs-4.2.ORIG/ess/term/language/rel/languages.lisp pvs-4.2/ess/term/language/rel/languages.lisp
--- pvs-4.2.ORIG/ess/term/language/rel/languages.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/term/language/rel/languages.lisp 2010-01-04 13:32:05.238575834 -0700
@@ -137,7 +137,7 @@
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro not-empty-str? (s)
`(not (string= ,s ""))))
@@ -176,7 +176,7 @@
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro lang-name (lang)
`(lang-struct-name ,lang))
diff -dur pvs-4.2.ORIG/ess/term/terms/rel/occur.lisp pvs-4.2/ess/term/terms/rel/occur.lisp
--- pvs-4.2.ORIG/ess/term/terms/rel/occur.lisp 2006-08-02 01:36:30.000000000 -0600
+++ pvs-4.2/ess/term/terms/rel/occur.lisp 2010-01-04 13:32:05.239646579 -0700
@@ -118,7 +118,7 @@
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro nil-occ ()
"Returns the empty occurrence."
@@ -181,7 +181,7 @@
; doc.
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro occ-rest (occ)
"Synonym for occ-parent."
`(occ-parent ,occ))
@@ -266,7 +266,7 @@
(defun ergolisp::\#q ()
(set-dispatch-macro-character #\# #\q #'read-list-to-occ))
-(eval-when (load eval)
+(eval-when (:load-toplevel :execute)
(ergolisp::\#q))
diff -dur pvs-4.2.ORIG/ess/term/terms/rel/opers.lisp pvs-4.2/ess/term/terms/rel/opers.lisp
--- pvs-4.2.ORIG/ess/term/terms/rel/opers.lisp 2006-08-02 01:36:30.000000000 -0600
+++ pvs-4.2/ess/term/terms/rel/opers.lisp 2010-01-04 13:32:05.239646579 -0700
@@ -295,7 +295,7 @@
(defun ergolisp::\#^ ()
(set-dispatch-macro-character #\# #\^ #'read-sexp-to-oper))
-(eval-when (load eval)
+(eval-when (:load-toplevel :execute)
(ergolisp::\#^))
diff -dur pvs-4.2.ORIG/ess/term/terms/rel/sorts.lisp pvs-4.2/ess/term/terms/rel/sorts.lisp
--- pvs-4.2.ORIG/ess/term/terms/rel/sorts.lisp 2006-08-02 01:36:30.000000000 -0600
+++ pvs-4.2/ess/term/terms/rel/sorts.lisp 2010-01-04 13:32:05.240644987 -0700
@@ -484,7 +484,7 @@
(defun ergolisp::\#t ()
(set-dispatch-macro-character #\# #\t #'read-sexp-to-ttype))
-(eval-when (load eval)
+(eval-when (:load-toplevel :execute)
(ergolisp::\#t))
@@ -504,7 +504,7 @@
(defun ergolisp::\#\@ ()
(set-dispatch-macro-character #\# #\@ #'read-sexp-to-opsig))
-(eval-when (load eval)
+(eval-when (:load-toplevel :execute)
(ergolisp::\#\@))
@@ -710,7 +710,7 @@
-(eval-when (load)
+(eval-when (:load-toplevel)
(setq *global-sort-table* (make-sort-table))
(setq *global-opsig-table* (make-opsig-table)))
diff -dur pvs-4.2.ORIG/ess/term/terms/rel/terms.lisp pvs-4.2/ess/term/terms/rel/terms.lisp
--- pvs-4.2.ORIG/ess/term/terms/rel/terms.lisp 2006-08-02 01:36:30.000000000 -0600
+++ pvs-4.2/ess/term/terms/rel/terms.lisp 2010-01-04 13:32:05.241642494 -0700
@@ -80,7 +80,7 @@
"The term ~S does not have a ~dth argument" term n)
(elt args n)))
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro term-arg0 (term)
"Get the 0th argument (child) of a term"
`(term-argn ,term 0))
@@ -122,7 +122,7 @@
"Number of TERM's arguments (sons)."
(length (term-args term)))
-(eval-when (compile eval load)
+(eval-when (:compile-toplevel :execute :load-toplevel)
(defmacro term-arity0? (term)
"Does TERM have 0 arguments?"
`(eql (term-arity ,term) 0))
@@ -258,6 +258,6 @@
(defun ergolisp::\#! ()
(set-dispatch-macro-character #\# #\! #'read-sexp-to-term))
-(eval-when (load eval)
+(eval-when (:load-toplevel :execute)
(ergolisp::\#!))
diff -dur pvs-4.2.ORIG/ess/term/trep/rel/attr-prims.lisp pvs-4.2/ess/term/trep/rel/attr-prims.lisp
--- pvs-4.2.ORIG/ess/term/trep/rel/attr-prims.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/term/trep/rel/attr-prims.lisp 2010-01-04 13:32:05.241642494 -0700
@@ -19,7 +19,7 @@
;;; features from the terms, so it is the default method for storing
;;; attributes.
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
(unless (find-package "TERM")
(make-package "TERM" :nicknames '("GTERM")
:use '(:cl-user :common-lisp :ergolisp))))
diff -dur pvs-4.2.ORIG/ess/term/trep/rel/gterm.lisp pvs-4.2/ess/term/trep/rel/gterm.lisp
--- pvs-4.2.ORIG/ess/term/trep/rel/gterm.lisp 2009-01-23 14:03:38.023198000 -0700
+++ pvs-4.2/ess/term/trep/rel/gterm.lisp 2010-01-04 13:32:05.242647427 -0700
@@ -29,7 +29,7 @@
;;; instead of a real operator.
;;;
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
(unless (find-package "TERM")
(make-package "TERM" :nicknames '("GTERM")
:use '(:cl-user :common-lisp :ergolisp))))
diff -dur pvs-4.2.ORIG/pvs-config.lisp pvs-4.2/pvs-config.lisp
--- pvs-4.2.ORIG/pvs-config.lisp 2010-01-04 01:42:48.463502000 -0700
+++ pvs-4.2/pvs-config.lisp 2010-01-04 13:32:05.242647427 -0700
@@ -41,7 +41,7 @@
;; Assume this is loaded while cd'd to the PVS directory
(namestring (truename *default-pathname-defaults*))))
-(eval-when (eval load)
+(eval-when (:execute :load-toplevel)
(defvar *pvs-platform*
(let ((cmd (format nil "~a/bin/pvs-platform" *pvs-path*)))
#+allegro (car (excl.osi:command-output cmd))
@@ -104,7 +104,7 @@
)
#+sbcl
-(eval-when (eval load)
+(eval-when (:execute :load-toplevel)
(setq sb-c::*fasl-file-type* *pvs-binary-type*))
#+allegro
diff -dur pvs-4.2.ORIG/pvs.system pvs-4.2/pvs.system
--- pvs-4.2.ORIG/pvs.system 2009-07-30 23:54:43.972932000 -0600
+++ pvs-4.2/pvs.system 2010-01-04 13:32:05.243641533 -0700
@@ -76,11 +76,11 @@
*print-pretty* t))
#+sbcl
-(eval-when (eval load)
+(eval-when (:execute :load-toplevel)
(setq *compile-verbose* nil)
(setq *compile-print* nil))
-(eval-when (eval load)
+(eval-when (:execute :load-toplevel)
;; This sets *pvs-path* and sets *pvs-binary-type*
(load "pvs-config.lisp")
#+allegro (chdir *pvs-path*))
diff -dur pvs-4.2.ORIG/src/defcl.lisp pvs-4.2/src/defcl.lisp
--- pvs-4.2.ORIG/src/defcl.lisp 2009-02-10 14:07:16.072144000 -0700
+++ pvs-4.2/src/defcl.lisp 2010-01-04 13:32:05.243641533 -0700
@@ -38,7 +38,7 @@
nil)
#+gcl
-(eval-when (eval compile load)
+(eval-when (:execute :compile-toplevel :load-toplevel)
(defmacro ignore-errors (&body forms)
`(progn , at forms)))
@@ -84,7 +84,7 @@
(proclaim '(inline ,(intern (format nil "~a?" name))))
(defun ,(intern (format nil "~a?" name)) (obj)
(typep obj ',name))
- (eval-when (eval compile load)
+ (eval-when (:execute :compile-toplevel :load-toplevel)
(setq *slot-info*
(cons (cons ',name
'(,classes ,args))
@@ -164,7 +164,7 @@
obj
(apply #'copy obj initargs)))
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
(defun remove-keyword (key list)
(let ((tail (member key list)))
(if tail
@@ -327,7 +327,7 @@
;(defmethod eequal (obj1 obj2)
; (equal obj1 obj2))
-(eval-when (eval compile load)
+(eval-when (:execute :compile-toplevel :load-toplevel)
(unless (fboundp 'memq)
(defun memq (elt list)
(member elt list :test #'eq))))
diff -dur pvs-4.2.ORIG/src/defsystem.lisp pvs-4.2/src/defsystem.lisp
--- pvs-4.2.ORIG/src/defsystem.lisp 2010-01-04 13:30:14.582611539 -0700
+++ pvs-4.2/src/defsystem.lisp 2010-01-04 13:32:05.245651845 -0700
@@ -834,7 +834,7 @@
;;; Massage CLtL2 onto *features* **
;;; ********************************
;;; Let's be smart about CLtL2 compatible Lisps:
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
#+(or (and allegro-version>= (version>= 4 0)) :mcl :sbcl)
(pushnew :cltl2 *features*))
@@ -1027,7 +1027,7 @@
#+(and :cltl2 (not (or :cmu :clisp :sbcl
(and :excl (or :allegro-v4.0 :allegro-v4.1))
:mcl)))
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
(unless (find-package "MAKE")
(make-package "MAKE" :nicknames '("MK") :use '("COMMON-LISP"))))
@@ -1046,7 +1046,7 @@
(:nicknames :mk))
#+(or :cltl2 :lispworks :scl)
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
(in-package "MAKE"))
#+ecl
@@ -1106,7 +1106,7 @@
;;; the compile form, so that you can't use a defvar with a default value and
;;; then a succeeding export as well.
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
(defvar *special-exports* nil)
(defvar *exports* nil)
(defvar *other-exports* nil)
@@ -1397,7 +1397,7 @@
;;; ********************************
;;; Massage people's *features* into better shape.
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
(dolist (feature *features*)
(when (and (symbolp feature) ; 3600
(equal (symbol-name feature) "CMU"))
@@ -1522,7 +1522,7 @@
;;; mc 11-Apr-91: Bashes MCL's point reader, so commented out.
#-:mcl
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
;; Define #@"foo" as a shorthand for (afs-binary-directory "foo").
;; For example,
;; <cl> #@"foo"
@@ -5134,7 +5134,7 @@
(t
nil)))))
-(eval-when (load eval)
+(eval-when (:load-toplevel :execute)
(component-operation :clean 'delete-binaries-operation)
(component-operation 'clean 'delete-binaries-operation)
(component-operation :delete-binaries 'delete-binaries-operation)
diff -dur pvs-4.2.ORIG/src/globals.lisp pvs-4.2/src/globals.lisp
--- pvs-4.2.ORIG/src/globals.lisp 2010-01-04 13:30:14.583612346 -0700
+++ pvs-4.2/src/globals.lisp 2010-01-04 13:32:05.247646832 -0700
@@ -69,7 +69,7 @@
(let ((end (position #\space excl::cl-release-date :from-end t)))
(subseq excl::cl-release-date 0 end)))
-(eval-when (eval compile load)
+(eval-when (:execute :compile-toplevel :load-toplevel)
(defparameter *pvs-version* "4.3")
;; Not used in PVS sources, but may be useful for patches, strategies, etc.
diff -dur pvs-4.2.ORIG/src/interface/allegro.lisp pvs-4.2/src/interface/allegro.lisp
--- pvs-4.2.ORIG/src/interface/allegro.lisp 2007-10-13 18:27:31.785169000 -0600
+++ pvs-4.2/src/interface/allegro.lisp 2010-01-04 13:32:05.255617163 -0700
@@ -78,7 +78,7 @@
;;;===========================================================================
;;; Epilogue
-(eval-when (load eval)
+(eval-when (:load-toplevel :execute)
(unless (compiled-function-p #'ilisp-callers)
(ilisp-message t "File is not compiled, use M-x ilisp-compile-inits")))
diff -dur pvs-4.2.ORIG/src/interface/cl-ilisp.lisp pvs-4.2/src/interface/cl-ilisp.lisp
--- pvs-4.2.ORIG/src/interface/cl-ilisp.lisp 2007-09-25 02:55:27.666195000 -0600
+++ pvs-4.2/src/interface/cl-ilisp.lisp 2010-01-04 13:32:05.256590085 -0700
@@ -775,7 +775,7 @@
nil))))
#-:cormanlisp
-(eval-when (load eval)
+(eval-when (:load-toplevel :execute)
(when
#+(and :CMU (or :CMU17 :CMU18))
(eval:interpreted-function-p #'ilisp-matching-symbols)
diff -dur pvs-4.2.ORIG/src/macros.lisp pvs-4.2/src/macros.lisp
--- pvs-4.2.ORIG/src/macros.lisp 2006-08-15 19:08:38.000000000 -0600
+++ pvs-4.2/src/macros.lisp 2010-01-04 13:32:05.256590085 -0700
@@ -370,7 +370,7 @@
(assert (symbolp name) () "NAME should be a symbol")
(assert (stringp term) () "TERM should be a string")
(assert (stringp theory) () "THEORY should be a string")
- (eval-when (eval load)
+ (eval-when (:execute :load-toplevel)
(let ((var (gensym))
(reset-name (intern (format nil "%RESET-~a" name)))
(hook (if (gethash (intern theory) *prelude*)
diff -dur pvs-4.2.ORIG/src/make-allegro-pvs.lisp pvs-4.2/src/make-allegro-pvs.lisp
--- pvs-4.2.ORIG/src/make-allegro-pvs.lisp 2008-07-22 05:15:55.475014000 -0600
+++ pvs-4.2/src/make-allegro-pvs.lisp 2010-01-04 13:32:05.257601202 -0700
@@ -26,7 +26,7 @@
(in-package :cl-user)
(defvar *pvs-path* (or (sys:getenv "PVSPATH") "."))
-(eval-when (load eval)
+(eval-when (:load-toplevel :execute)
(require 'tpl-debug)
#+(or runtime-standard runtime-dynamic)
(pushnew :runtime *features*)
diff -dur pvs-4.2.ORIG/src/make-pvs-methods.lisp pvs-4.2/src/make-pvs-methods.lisp
--- pvs-4.2.ORIG/src/make-pvs-methods.lisp 2009-02-10 14:09:51.780822000 -0700
+++ pvs-4.2/src/make-pvs-methods.lisp 2010-01-04 13:32:05.258561299 -0700
@@ -29,7 +29,7 @@
(in-package :cl-user)
-(eval-when (eval load)
+(eval-when (:execute :load-toplevel)
;; This sets *pvs-path* and sets *pvs-binary-type*
(load "pvs-config.lisp"))
diff -dur pvs-4.2.ORIG/src/make-pvs-parser.lisp pvs-4.2/src/make-pvs-parser.lisp
--- pvs-4.2.ORIG/src/make-pvs-parser.lisp 2009-07-31 01:53:25.344382000 -0600
+++ pvs-4.2/src/make-pvs-parser.lisp 2010-01-04 13:32:05.258561299 -0700
@@ -40,7 +40,7 @@
(in-package :cl-user)
-(eval-when (eval load)
+(eval-when (:execute :load-toplevel)
;; This sets *pvs-path* and sets *pvs-binary-type*
(load "pvs-config.lisp"))
diff -dur pvs-4.2.ORIG/src/metering.lisp pvs-4.2/src/metering.lisp
--- pvs-4.2.ORIG/src/metering.lisp 2009-07-31 01:53:25.344382000 -0600
+++ pvs-4.2/src/metering.lisp 2010-01-04 13:32:05.258561299 -0700
@@ -289,7 +289,7 @@
(progn
#-(or sbcl cmu allegro)
- (eval-when (compile eval)
+ (eval-when (:compile-toplevel :execute)
(warn
"You may want to supply implementation-specific get-time functions."))
@@ -320,7 +320,7 @@
#-(or sbcl :cmu :lcl3.0)
(progn
- (eval-when (compile eval)
+ (eval-when (:compile-toplevel :execute)
(warn "No consing will be reported unless a get-cons function is ~
defined."))
@@ -401,10 +401,10 @@
#-(or sbcl :cmu :lcl3.0 (and :allegro (not :coral)))
(progn
- (eval-when (compile eval)
+ (eval-when (:compile-toplevel :execute)
(warn
"You may want to add an implementation-specific Required-Arguments function."))
- (eval-when (load eval)
+ (eval-when (:load-toplevel :execute)
(defun required-arguments (name)
(declare (ignore name))
(values 0 t))))
@@ -547,7 +547,7 @@
;;; ********************************
;;; Encapsulate ********************
;;; ********************************
-(eval-when (compile load eval)
+(eval-when (:compile-toplevel :load-toplevel :execute)
;; Returns a lambda expression for a function that, when called with the
;; function name, will set up that function for metering.
;;
@@ -642,7 +642,7 @@
;;; along with any new ones we encounter. Since we're now precomputing
;;; closure functions for common argument signatures, this eliminates
;;; the former need to call COMPILE for each monitored function.
-(eval-when (compile eval)
+(eval-when (:compile-toplevel :execute)
(defconstant precomputed-encapsulations 8))
(defvar *existing-encapsulations* (make-hash-table :test #'equal))
diff -dur pvs-4.2.ORIG/src/prover/strategies.lisp pvs-4.2/src/prover/strategies.lisp
--- pvs-4.2.ORIG/src/prover/strategies.lisp 2010-01-02 07:27:48.897224000 -0700
+++ pvs-4.2/src/prover/strategies.lisp 2010-01-04 13:32:05.260886822 -0700
@@ -29,7 +29,7 @@
(in-package :pvs)
-(eval-when (eval compile load)
+(eval-when (:execute :compile-toplevel :load-toplevel)
(defun check-formals (formals &optional opt-flag)
(or (null formals)
(if (eq (car formals) '&optional)
diff -dur pvs-4.2.ORIG/src/utils/file-utils.lisp pvs-4.2/src/utils/file-utils.lisp
--- pvs-4.2.ORIG/src/utils/file-utils.lisp 2006-08-03 01:03:34.000000000 -0600
+++ pvs-4.2/src/utils/file-utils.lisp 2010-01-04 13:32:05.261988137 -0700
@@ -19,12 +19,12 @@
;; --------------------------------------------------------------------
(in-package :pvs)
-(eval-when (compile)
+(eval-when (:compile-toplevel)
(require :foreign))
(export '(file-exists-p directory-p read-permission? write-permission?
file-write-time get-file-info))
-(eval-when (eval compile load)
+(eval-when (:execute :compile-toplevel :load-toplevel)
(ff:def-foreign-call fileutils___file_exists_p
((filename (* :char) simple-string))
#+(version>= 6) :strings-convert #+(version>= 6) t
pvs-4.2-autoconf.patch:
configure.in | 7 +++----
1 file changed, 3 insertions(+), 4 deletions(-)
--- NEW FILE pvs-4.2-autoconf.patch ---
diff -dur pvs-4.2.ORIG/configure.in pvs-4.2/configure.in
--- pvs-4.2.ORIG/configure.in 2007-04-01 00:02:51.000000000 -0600
+++ pvs-4.2/configure.in 2009-11-05 17:09:13.484872102 -0700
@@ -21,7 +21,8 @@
dnl make sure we are using a recent autoconf version
-AC_PREREQ(2.59)
+AC_PREREQ(2.61)
+AC_INIT([pvs],[4.2],[pvs-bugs at csl.sri.com])
dnl If it doesn't look like GNU Make is being used, give a friendly warning
tem=`make --version -f /dev/null 2>&1 | grep GNU`
@@ -30,8 +31,6 @@
fi
dnl This file must exist for configure to run
-AC_MSG_CHECKING(for existence of src/pvs.lisp)
-AC_INIT
AC_CONFIG_SRCDIR([src/pvs.lisp])
dnl This sets build, build_cpu, build_vendor, and build_os
@@ -146,7 +145,7 @@
export PLATFORM
# Finally create all the generated files
-AC_CONFIG_FILES([Makefile pvs pvsio doc/user-guide/Makefile doc/language/Makefile doc/language/pvs-doc.el doc/prover/Makefile])
+AC_CONFIG_FILES([Makefile pvs pvsio doc/api/Makefile doc/user-guide/Makefile doc/language/Makefile doc/language/pvs-doc.el doc/prover/Makefile])
AC_OUTPUT
chmod a+x pvs
pvs-4.2-build-id.patch:
ix86-Linux/Makefile | 4 ++--
ix86_64-Linux/Makefile | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
--- NEW FILE pvs-4.2-build-id.patch ---
diff -dur pvs-4.2.ORIG/BDD/ix86_64-Linux/Makefile pvs-4.2/BDD/ix86_64-Linux/Makefile
--- pvs-4.2.ORIG/BDD/ix86_64-Linux/Makefile 2009-10-04 13:25:53.000000000 -0600
+++ pvs-4.2/BDD/ix86_64-Linux/Makefile 2009-12-17 08:38:07.606881718 -0700
@@ -5,7 +5,7 @@
#LD = gcc
#LDFLAGS = -shared -L./
LD = ld
-LDFLAGS = -Bsymbolic -shared -warn-once -L./
+LDFLAGS = -Xlinker -Bsymbolic -shared -L./
CC = gcc
CFLAGS = -D_POSIX_SOURCE -DSYSV $(INCLUDES) -DLINUX -DLINUX_REDHAT5 -DSIGNALS_LINUX -fPIC -Wall -Winline -ggdb
XCFLAGS = -O
@@ -24,7 +24,7 @@
all : mu.so
mu.so : ${muobj} libutils.a ../bdd-ld-table ../mu-ld-table
- $(LD) ../bdd-ld-table ../mu-ld-table $(LDFLAGS) -o mu.so ${muobj} -lutils -lm -lbsd
+ $(CC) ../bdd-ld-table ../mu-ld-table $(LDFLAGS) -o mu.so ${muobj} -lutils -lm -lbsd
libutils.a : ${utilobj}
ar r libutils.a ${utilobj}
diff -dur pvs-4.2.ORIG/BDD/ix86-Linux/Makefile pvs-4.2/BDD/ix86-Linux/Makefile
--- pvs-4.2.ORIG/BDD/ix86-Linux/Makefile 2006-07-23 13:41:58.000000000 -0600
+++ pvs-4.2/BDD/ix86-Linux/Makefile 2009-12-17 08:38:38.734006137 -0700
@@ -3,7 +3,7 @@
UTILS = ../bdd/utils
INCLUDES = -I/usr/include -I$(BDD) -I$(UTILS) -I$(MU)
LD = ld
-LDFLAGS = -Bsymbolic -shared -warn-once -L./
+LDFLAGS = -Xlinker -Bsymbolic -shared -L./
CC = gcc
CFLAGS = -D_POSIX_SOURCE -DSYSV $(INCLUDES) -DLINUX -DLINUX_REDHAT5 -DSIGNALS_LINUX
XCFLAGS = -O
@@ -22,7 +22,7 @@
all : mu.so
mu.so : ${muobj} libutils.a ../bdd-ld-table ../mu-ld-table
- $(LD) ../bdd-ld-table ../mu-ld-table $(LDFLAGS) -o mu.so ${muobj} -lutils -lm -lbsd
+ $(CC) ../bdd-ld-table ../mu-ld-table $(LDFLAGS) -o mu.so ${muobj} -lutils -lm -lbsd
libutils.a : ${utilobj}
ar r libutils.a ${utilobj}
pvs-4.2-emacs.patch:
Makefile.in | 4 ++++
emacs/emacs-src/ilisp/ilcompat.el | 6 +-----
emacs/emacs-src/pvs-cmds.el | 6 ++++--
pvs.in | 1 -
4 files changed, 9 insertions(+), 8 deletions(-)
--- NEW FILE pvs-4.2-emacs.patch ---
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilcompat.el pvs-4.2/emacs/emacs-src/ilisp/ilcompat.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilcompat.el 2010-01-04 13:30:39.919550709 -0700
+++ pvs-4.2/emacs/emacs-src/ilisp/ilcompat.el 2010-01-04 13:30:18.847800402 -0700
@@ -25,11 +25,7 @@
((string-match "XEmacs " (emacs-version))
(message "ILISP: Unknown XEmacs. Assuming XEmacs 20 - best of luck!")
'xemacs-20)
- ((string-match "Emacs 22" (emacs-version))
- 'fsf-20)
- ((string-match "Emacs 21" (emacs-version))
- 'fsf-20)
- ((string-match "Emacs 20" (emacs-version))
+ ((string-match "Emacs 2[[:digit:]]" (emacs-version))
'fsf-20)
((string-match "Emacs 19" (emacs-version))
'fsf-19)
diff -dur pvs-4.2.ORIG/emacs/emacs-src/pvs-cmds.el pvs-4.2/emacs/emacs-src/pvs-cmds.el
--- pvs-4.2.ORIG/emacs/emacs-src/pvs-cmds.el 2010-01-04 13:30:39.920550469 -0700
+++ pvs-4.2/emacs/emacs-src/pvs-cmds.el 2010-01-04 13:30:18.848800418 -0700
@@ -1353,9 +1353,11 @@
(comint-send (ilisp-process) "(exit-pvs t)")
(while (and (ilisp-process)
(eq (process-status (ilisp-process)) 'run))
- (sit-for 1)))
+ (if (null (accept-process-output nil 1))
+ (discard-input))))
(error
- (sleep-for 1)
+ (if (null (accept-process-output nil 1))
+ (discard-input))
(when (equal (process-status process) 'run)
(error "PVS Lisp process did not exit properly"))))))))
diff -dur pvs-4.2.ORIG/Makefile.in pvs-4.2/Makefile.in
--- pvs-4.2.ORIG/Makefile.in 2010-01-04 13:30:39.921550486 -0700
+++ pvs-4.2/Makefile.in 2010-01-04 13:30:18.849800438 -0700
@@ -132,6 +132,9 @@
: '[^X]*\(X*Emacs [0-9][0-9]\)')
+ifeq ($(emacsversion),Emacs 23)
+EMACSSUBDIR = emacs23
+else
ifeq ($(emacsversion),Emacs 22)
EMACSSUBDIR = emacs22
else
@@ -157,6 +160,7 @@
endif
endif
endif
+endif
endif # end of buildcmds check
diff -dur pvs-4.2.ORIG/pvs.in pvs-4.2/pvs.in
--- pvs-4.2.ORIG/pvs.in 2010-01-04 13:30:39.922550544 -0700
+++ pvs-4.2/pvs.in 2010-01-04 13:30:18.850800423 -0700
@@ -385,7 +385,6 @@
case $PVSEMACS in
*[xl]emacs*) \
- PVSEMACS="LD_ASSUME_KERNEL=${LD_ASSUME_KERNEL} ${PVSEMACS}"
if [ $nobg ] ; then
("$PVSEMACS" $flags -name pvs -in PVS@$HOST -wn PVS@$HOST \
$PVSXINIT $pvsemacsinit )
pvs-4.2-latex.patch:
api/Makefile.in | 4 ++++
api/pvs-api.tex | 4 ++--
datatypes/Makefile | 4 ++++
datatypes/datatypes.tex | 4 ++--
interpretations/interpretations.tex | 2 +-
language/Makefile.in | 4 ++++
language/language.tex | 2 +-
prover/Makefile.in | 4 ++++
prover/prover.tex | 2 +-
semantics/Makefile | 4 ++++
user-guide/Makefile.in | 11 ++++++++---
user-guide/user-guide.tex | 2 +-
12 files changed, 36 insertions(+), 11 deletions(-)
--- NEW FILE pvs-4.2-latex.patch ---
diff -dur pvs-4.2.ORIG/doc/api/Makefile.in pvs-4.2/doc/api/Makefile.in
--- pvs-4.2.ORIG/doc/api/Makefile.in 2007-05-19 17:05:32.000000000 -0600
+++ pvs-4.2/doc/api/Makefile.in 2009-11-06 10:30:25.765410326 -0700
@@ -22,6 +22,10 @@
pvs-api.pdf : ${sources} ${grammar-tables}
pdflatex $<
+ makeindex -c pvs-api.idx
+ bibtex pvs-api || echo
+ pdflatex $<
+ pdflatex $<
.PHONY: clean
clean :
diff -dur pvs-4.2.ORIG/doc/api/pvs-api.tex pvs-4.2/doc/api/pvs-api.tex
--- pvs-4.2.ORIG/doc/api/pvs-api.tex 2007-05-19 17:05:32.000000000 -0600
+++ pvs-4.2/doc/api/pvs-api.tex 2009-11-06 10:30:25.767409186 -0700
@@ -8,7 +8,7 @@
\usepackage{makeidx}
\usepackage{relsize}
\usepackage{boxedminipage}
-\usepackage{fancyheadings}
+\usepackage{fancyhdr}
%\usepackage{../../pvs}
\usepackage{url}
\usepackage{../makebnf}
@@ -5962,7 +5962,7 @@
from the root to the given sequent, of the form \texttt{top.0.1.3}.
\bibliographystyle{plain}
-\bibliography{../pvs,/homes/owre/pvs3.0/doc/pvs}
+\bibliography{../pvs}
{\smaller
\printindex
diff -dur pvs-4.2.ORIG/doc/datatypes/datatypes.tex pvs-4.2/doc/datatypes/datatypes.tex
--- pvs-4.2.ORIG/doc/datatypes/datatypes.tex 2007-05-19 17:03:30.000000000 -0600
+++ pvs-4.2/doc/datatypes/datatypes.tex 2009-11-06 10:30:25.769462544 -0700
@@ -2,7 +2,7 @@
% Master File: datatypes.tex
\documentclass[11pt,twoside]{book}
\usepackage{relsize,url,makeidx,alltt}
-\usepackage{fancyheadings}
+\usepackage{fancyhdr}
\usepackage[chapter]{tocbibind}
\makeatletter
\@ifundefined{pdfoutput}%
@@ -2805,5 +2805,5 @@
\bibliographystyle{alpha}
-\bibliography{/homes/rushby/jmr,/homes/shankar/tex}
+\bibliography{../pvs}
\end{document}
diff -dur pvs-4.2.ORIG/doc/datatypes/Makefile pvs-4.2/doc/datatypes/Makefile
--- pvs-4.2.ORIG/doc/datatypes/Makefile 2007-05-19 17:03:30.000000000 -0600
+++ pvs-4.2/doc/datatypes/Makefile 2009-11-06 10:30:25.770464299 -0700
@@ -17,6 +17,10 @@
datatypes.pdf : ${sources}
pdflatex $<
+ makeindex -c datatypes.idx
+ bibtex datatypes || echo
+ pdflatex $<
+ pdflatex $<
.PHONY: clean
clean :
diff -dur pvs-4.2.ORIG/doc/interpretations/interpretations.tex pvs-4.2/doc/interpretations/interpretations.tex
--- pvs-4.2.ORIG/doc/interpretations/interpretations.tex 2007-05-19 18:57:36.000000000 -0600
+++ pvs-4.2/doc/interpretations/interpretations.tex 2009-11-06 10:30:25.772441992 -0700
@@ -1200,5 +1200,5 @@
\newpage
\bibliographystyle{alpha}
\addcontentsline{toc}{chapter}{Bibliography}
-\bibliography{/homes/rushby/jmr,/homes/owre/tex/sam,/homes/shankar/tex}
+\bibliography{../pvs}
\end{document}
diff -dur pvs-4.2.ORIG/doc/language/language.tex pvs-4.2/doc/language/language.tex
--- pvs-4.2.ORIG/doc/language/language.tex 2006-09-21 22:54:57.000000000 -0600
+++ pvs-4.2/doc/language/language.tex 2009-11-06 10:30:25.773456354 -0700
@@ -6,7 +6,7 @@
\usepackage{makeidx}
\usepackage{relsize}
\usepackage{boxedminipage}
-\usepackage{fancyheadings}
+\usepackage{fancyhdr}
%\usepackage{../../pvs}
\usepackage{url}
\usepackage{../makebnf}
diff -dur pvs-4.2.ORIG/doc/language/Makefile.in pvs-4.2/doc/language/Makefile.in
--- pvs-4.2.ORIG/doc/language/Makefile.in 2006-09-21 22:54:57.000000000 -0600
+++ pvs-4.2/doc/language/Makefile.in 2009-11-06 10:30:25.773456354 -0700
@@ -43,6 +43,10 @@
language.pdf : ${sources} ${grammar-tables}
pdflatex $<
+ makeindex -c language.idx
+ bibtex language || echo
+ pdflatex $<
+ pdflatex $<
.PHONY: clean
clean :
diff -dur pvs-4.2.ORIG/doc/prover/Makefile.in pvs-4.2/doc/prover/Makefile.in
--- pvs-4.2.ORIG/doc/prover/Makefile.in 2002-07-05 13:50:53.000000000 -0600
+++ pvs-4.2/doc/prover/Makefile.in 2009-11-06 10:30:25.774457266 -0700
@@ -17,6 +17,10 @@
prover.pdf : ${sources}
pdflatex $<
+ makeindex -c prover.idx
+ bibtex prover || echo
+ pdflatex $<
+ pdflatex $<
.PHONY: clean
clean :
diff -dur pvs-4.2.ORIG/doc/prover/prover.tex pvs-4.2/doc/prover/prover.tex
--- pvs-4.2.ORIG/doc/prover/prover.tex 2006-09-21 23:13:37.000000000 -0600
+++ pvs-4.2/doc/prover/prover.tex 2009-11-06 10:30:25.777429336 -0700
@@ -1,7 +1,7 @@
% Document Type: LaTeX
% Master File: prover.tex
\documentclass[12pt,twoside]{book}
-\usepackage{relsize,alltt,makeidx,url,boxedminipage,fancyheadings,tabularx}
+\usepackage{relsize,alltt,makeidx,url,boxedminipage,fancyhdr,tabularx}
%\usepackage{../../pvs}
\usepackage{../makebnf}
\usepackage[chapter]{tocbibind}
diff -dur pvs-4.2.ORIG/doc/semantics/Makefile pvs-4.2/doc/semantics/Makefile
--- pvs-4.2.ORIG/doc/semantics/Makefile 2007-05-19 17:28:21.000000000 -0600
+++ pvs-4.2/doc/semantics/Makefile 2009-11-06 10:30:25.779593316 -0700
@@ -17,6 +17,10 @@
semantics.pdf : ${sources}
pdflatex $<
+ makeindex -c semantics.idx
+ bibtex semantics || echo
+ pdflatex $<
+ pdflatex $<
.PHONY: clean
clean :
diff -dur pvs-4.2.ORIG/doc/user-guide/Makefile.in pvs-4.2/doc/user-guide/Makefile.in
--- pvs-4.2.ORIG/doc/user-guide/Makefile.in 2002-08-01 00:35:38.000000000 -0600
+++ pvs-4.2/doc/user-guide/Makefile.in 2009-11-06 10:31:27.193544625 -0700
@@ -20,11 +20,16 @@
user-guide.ps : user-guide.dvi
dvips -o $@ $<
-user-guide.pdf : ${sources} pvs-screen1.pdf
- pdflatex $<
+user-guide.pdf : $(headers) $(sources) pvs-screen1.pdf \
+ sum-nosub.tex sum-sub.tex sum-tccs.tex
+ pdflatex user-guide
+ bibtex user-guide || echo
+ makeindex -o user-guide.ind user-guide.idx
+ pdflatex user-guide
+ pdflatex user-guide
sum-nosub.tex sum-sub.tex sum-tccs.tex : sum.pvs sum.el
- @PVSPATH@/pvs -batch -q -l sum.el -f kill-process
+ $(pvs-path)/pvs -batch -q -l sum.el
.PHONY: clean
clean :
diff -dur pvs-4.2.ORIG/doc/user-guide/user-guide.tex pvs-4.2/doc/user-guide/user-guide.tex
--- pvs-4.2.ORIG/doc/user-guide/user-guide.tex 2006-09-21 17:52:37.000000000 -0600
+++ pvs-4.2/doc/user-guide/user-guide.tex 2009-11-06 10:30:25.780423733 -0700
@@ -7,7 +7,7 @@
%\usepackage{showidx} % use for index debugging
\usepackage{relsize}
\usepackage{boxedminipage}
-\usepackage{fancyheadings}
+\usepackage{fancyhdr}
\usepackage{graphicx}
\usepackage{../../pvs}
\usepackage{url}
pvs-4.2-mona.patch:
BDD/bdd-ld-table | 8 ++++----
BDD/bdd-sbcl.lisp | 14 +++++++-------
BDD/bdd.lisp | 4 ++--
BDD/bdd/draw/main.c | 2 +-
BDD/bdd/src/bdd.c | 8 ++++----
BDD/bdd/src/bdd_extern.h | 8 ++++----
BDD/bdd/src/main.c | 6 +++---
BDD/bdd/src/template.c | 2 +-
BDD/bdd_table.c | 8 ++++----
BDD/mu.lisp | 2 +-
BDD/mu/src/main.c | 2 +-
BDD/mu/src/mu.c | 10 +++++-----
BDD/mu/src/yacc.y | 2 +-
BDD/mu_interface.c | 2 +-
pvs.system | 2 +-
src/WS1S/ix86-Linux/Makefile | 12 ++----------
src/WS1S/ix86_64-Linux/Makefile | 12 ++----------
src/WS1S/lisp/dfa.lisp | 2 +-
src/WS1S/ws1s-ld-table | 2 +-
src/WS1S/ws1s_table.c | 4 ++--
src/pvs.lisp | 2 +-
21 files changed, 49 insertions(+), 65 deletions(-)
--- NEW FILE pvs-4.2-mona.patch ---
diff -dur pvs-4.2.ORIG/BDD/bdd/draw/main.c pvs-4.2/BDD/bdd/draw/main.c
--- pvs-4.2.ORIG/BDD/bdd/draw/main.c 1999-01-06 12:36:48.000000000 -0700
+++ pvs-4.2/BDD/bdd/draw/main.c 2010-01-01 14:38:49.082596637 -0700
@@ -292,7 +292,7 @@
aux_table = make_hashtab (0);
/* bdd_sizeof_user_data = sizeof (XYPOS);*/
- bdd_init ();
+ BDD_bdd_init ();
/* Create the dummy 0 var: */
/* bdd_free (bdd_create_var_last ());*/
diff -dur pvs-4.2.ORIG/BDD/bdd/src/bdd.c pvs-4.2/BDD/bdd/src/bdd.c
--- pvs-4.2.ORIG/BDD/bdd/src/bdd.c 2009-10-04 13:25:53.000000000 -0600
+++ pvs-4.2/BDD/bdd/src/bdd.c 2010-01-01 14:55:36.176596416 -0700
@@ -780,7 +780,7 @@
Depending on the use of complemented edges in the BDDs there exist
either 2 constant nodes or 3.
*/
-int bdd_size (BDDPTR f)
+int BDD_bdd_size (BDDPTR f)
{
node_counter = 0;
if (!BDD_VOID_P (f)) {
@@ -3162,7 +3162,7 @@
print_computed_table_stats (fp);
}
-void bdd_init (void)
+void BDD_bdd_init (void)
{
/* Guard against multiple initialisations: */
if (BDD_PACKAGE_INITIALIZED) {
@@ -3562,7 +3562,7 @@
return BDD_VOID_P (f) ? -1 : BDD_RANK (f);
}
-BDDPTR bdd_then (BDDPTR f)
+BDDPTR BDD_bdd_then (BDDPTR f)
{
BDDPTR R = BDD_COFACTOR_POS (f);
@@ -3570,7 +3570,7 @@
return R;
}
-BDDPTR bdd_else (BDDPTR f)
+BDDPTR BDD_bdd_else (BDDPTR f)
{
BDDPTR R = BDD_COFACTOR_NEG (f);
diff -dur pvs-4.2.ORIG/BDD/bdd/src/bdd_extern.h pvs-4.2/BDD/bdd/src/bdd_extern.h
--- pvs-4.2.ORIG/BDD/bdd/src/bdd_extern.h 2009-10-04 13:25:53.000000000 -0600
+++ pvs-4.2/BDD/bdd/src/bdd_extern.h 2010-01-01 14:54:39.558596780 -0700
@@ -90,7 +90,7 @@
/* ------------------------------------------------------------------------ */
/* Package administration related routines: */
-extern void bdd_init (void);
+extern void BDD_bdd_init (void);
extern void bdd_quit (void);
extern void bdd_print_stats (FILE *fp);
extern int bdd_gc (void);
@@ -155,8 +155,8 @@
extern int bdd_implies_taut (BDDPTR f, BDDPTR g);
extern BDDPTR bdd_nand (BDDPTR f, BDDPTR g);
extern BDDPTR bdd_invert_input_top (BDDPTR f);
-extern BDDPTR bdd_then (BDDPTR f);
-extern BDDPTR bdd_else (BDDPTR f);
+extern BDDPTR BDD_bdd_then (BDDPTR f);
+extern BDDPTR BDD_bdd_else (BDDPTR f);
extern BDDPTR bdd_constrain (BDDPTR f, BDDPTR c);
extern BDDPTR bdd_restrict (BDDPTR f, BDDPTR c);
@@ -169,7 +169,7 @@
extern BDDPTR bdd_top_var (BDDPTR f);
extern int bdd_top_var_id (BDDPTR f);
extern int bdd_top_var_rank (BDDPTR f);
-extern int bdd_size (BDDPTR f);
+extern int BDD_bdd_size (BDDPTR f);
extern int bdd_depth (BDDPTR f);
extern int bdd_size_vec (BDDPTR *f_vec, int size);
extern int bdd_size_ceil (BDDPTR f, int ceiling);
diff -dur pvs-4.2.ORIG/BDD/bdd/src/main.c pvs-4.2/BDD/bdd/src/main.c
--- pvs-4.2.ORIG/BDD/bdd/src/main.c 2008-12-15 00:50:28.000000000 -0700
+++ pvs-4.2/BDD/bdd/src/main.c 2010-01-01 14:49:11.489721954 -0700
@@ -90,7 +90,7 @@
/* Note: we don't count the dummy 0 variable! */
fprintf (stdout, "/* Size: %d, (%s minterms, %s X terms, %d vars), Depth: %d, Alive: %d */\n",
- bdd_size (f),
+ BDD_bdd_size (f),
D_sprintf (buf, bdd_count_sat_assignments (f, BDD_0), 0),
D_sprintf (buf2, bdd_count_X_terms (f), 0),
bdd_nr_vars,
@@ -316,7 +316,7 @@
/* if (!_setjmp (Context))*/
if (1) {
- bdd_init ();
+ BDD_bdd_init ();
current_interface = bdd_get_factor_interface ();
/* current_interface->out = stdout;*/
@@ -388,7 +388,7 @@
#ifdef COMMENT
/* Just for testing purposes: */
bdd_quit ();
- bdd_init ();
+ BDD_bdd_init ();
free_hashtab (var_table);
var_table = make_hashtab (3);
/* Let's not use entry nr. 0 for fun: */
diff -dur pvs-4.2.ORIG/BDD/bdd/src/template.c pvs-4.2/BDD/bdd/src/template.c
--- pvs-4.2.ORIG/BDD/bdd/src/template.c 2008-12-15 00:50:28.000000000 -0700
+++ pvs-4.2/BDD/bdd/src/template.c 2010-01-01 14:43:20.321596917 -0700
@@ -61,7 +61,7 @@
*/
/* This is a must! And should also be done prior to any BDD operation. */
- bdd_init ();
+ BDD_bdd_init ();
fprintf (stdout, "BDD Package Initialised.\n");
bdd_print_stats (stdout);
diff -dur pvs-4.2.ORIG/BDD/bdd-ld-table pvs-4.2/BDD/bdd-ld-table
--- pvs-4.2.ORIG/BDD/bdd-ld-table 2008-12-15 00:50:28.000000000 -0700
+++ pvs-4.2/BDD/bdd-ld-table 2010-01-01 14:52:28.921596712 -0700
@@ -25,8 +25,8 @@
bdd___bdd_lit_p = bdd_lit_p ;
bdd___bdd_cofactor_pos_ = bdd_cofactor_pos_ ;
bdd___bdd_cofactor_neg_ = bdd_cofactor_neg_ ;
-bdd___bdd_size = bdd_size ;
-bdd___bdd_init = bdd_init ;
+bdd___BDD_bdd_size = BDD_bdd_size ;
+bdd___BDD_bdd_init = BDD_bdd_init ;
bdd___bdd_free = bdd_free ;
bdd___bdd_gc = bdd_gc ;
bdd___bdd_ite = bdd_ite ;
@@ -57,8 +57,8 @@
bdd___bdd_1 = bdd_1 ;
bdd___bdd_X = bdd_X ;
bdd___bdd_assign = bdd_assign ;
-bdd___bdd_then = bdd_then ;
-bdd___bdd_else = bdd_else ;
+bdd___BDD_bdd_then = BDD_bdd_then ;
+bdd___BDD_bdd_else = BDD_bdd_else ;
bdd___bdd_apply = bdd_apply ;
bdd___bdd_constrain = bdd_constrain ;
/* bdd___bdd_sum_of_cubes = bdd_sum_of_cubes ; */
diff -dur pvs-4.2.ORIG/BDD/bdd.lisp pvs-4.2/BDD/bdd.lisp
--- pvs-4.2.ORIG/BDD/bdd.lisp 2008-12-15 00:50:28.000000000 -0700
+++ pvs-4.2/BDD/bdd.lisp 2010-01-01 14:37:29.132596592 -0700
@@ -89,7 +89,7 @@
(selected-sforms (select-seq sforms fnums)))
(cond ((null selected-sforms)
(values 'X nil nil))
- (t (unless *bdd-initialized* (bdd_init))
+ (t (unless *bdd-initialized* (BDD_bdd_init))
(if dynamic-ordering?
(set_bdd_do_dynamic_ordering 1)
(set_bdd_do_dynamic_ordering 0))
@@ -119,7 +119,7 @@
(defvar *ignore-boolean-equalities?* nil)
(defun bdd-simplify (expr &optional ignore-boolean-equalities?)
- (unless *bdd-initialized* (bdd_init))
+ (unless *bdd-initialized* (BDD_bdd_init))
(let* ((*pvs-bdd-hash* (make-pvs-hash-table))
(*bdd-pvs-hash* (make-hash-table))
(*recognizer-forms-alist* nil)
diff -dur pvs-4.2.ORIG/BDD/bdd-sbcl.lisp pvs-4.2/BDD/bdd-sbcl.lisp
--- pvs-4.2.ORIG/BDD/bdd-sbcl.lisp 2009-07-31 02:00:41.000000000 -0600
+++ pvs-4.2/BDD/bdd-sbcl.lisp 2010-01-01 14:52:13.539596694 -0700
@@ -207,16 +207,16 @@
;;; void bdd_traverse_pre (register BDDPTR v, void (*pre_action)(BDDPTR))
;;; void bdd_traverse_post (register BDDPTR v, void (*post_action)(BDDPTR))
-;;; int bdd_size (BDDPTR f)
-(sb-alien:define-alien-routine ("bdd___bdd_size" bdd_size)
+;;; int BDD_bdd_size (BDDPTR f)
+(sb-alien:define-alien-routine ("bdd___BDD_bdd_size" BDD_bdd_size)
(integer 32)
(f (* t)))
;;; int bdd_size_vec (BDDPTR *f_vec, int size)
;;; int bdd_size_ceil (BDDPTR f, int ceiling)
-;;; void bdd_init (void)
-(sb-alien:define-alien-routine ("bdd___bdd_init" bdd_init)
+;;; void BDD_bdd_init (void)
+(sb-alien:define-alien-routine ("bdd___BDD_bdd_init" BDD_bdd_init)
sb-alien:void)
;;; void bdd_free (BDDPTR f)
@@ -400,12 +400,12 @@
;;; BDDPTR bdd_top_var (BDDPTR f)
;;; int bdd_top_var_rank (BDDPTR f)
;;; BDDPTR bdd_then (BDDPTR f)
-(sb-alien:define-alien-routine ("bdd___bdd_then" bdd_then)
+(sb-alien:define-alien-routine ("bdd___BDD_bdd_then" BDD_bdd_then)
(* t)
(f (* t)))
;;; BDDPTR bdd_else (BDDPTR f)
-(sb-alien:define-alien-routine ("bdd___bdd_else" bdd_else)
+(sb-alien:define-alien-routine ("bdd___BDD_bdd_else" BDD_bdd_else)
(* t)
(f (* t)))
@@ -552,4 +552,4 @@
(defun bdd-interrupted? ()
(not (zerop bdd_interrupted)))
-(bdd_init)
+(BDD_bdd_init)
diff -dur pvs-4.2.ORIG/BDD/bdd_table.c pvs-4.2/BDD/bdd_table.c
--- pvs-4.2.ORIG/BDD/bdd_table.c 2008-12-15 00:50:28.000000000 -0700
+++ pvs-4.2/BDD/bdd_table.c 2010-01-01 14:52:50.567596941 -0700
@@ -61,9 +61,9 @@
return (BDDPTR) bdd_cofactor_neg_ (f);
}
-int bdd___bdd_size (BDDPTR f) {return bdd_size (f);}
+int bdd___BDD_bdd_size (BDDPTR f) {return BDD_bdd_size (f);}
-void bdd___bdd_init (void) {bdd_init ();}
+void bdd___BDD_bdd_init (void) {BDD_bdd_init ();}
void bdd___bdd_free (BDDPTR f) {bdd_free (f);}
@@ -128,9 +128,9 @@
BDDPTR bdd___bdd_assign (BDDPTR f) {return bdd_assign (f);}
-BDDPTR bdd___bdd_then (BDDPTR f) {return bdd_then (f);}
+BDDPTR bdd___BDD_bdd_then (BDDPTR f) {return BDD_bdd_then (f);}
-BDDPTR bdd___bdd_else (BDDPTR f) {return bdd_else (f);}
+BDDPTR bdd___BDD_bdd_else (BDDPTR f) {return BDD_bdd_else (f);}
BDDPTR bdd___bdd_apply (BDDPTR (*f)(BDDPTR,BDDPTR), BDDPTR a, BDDPTR b)
{return bdd_apply (f, a, b);}
diff -dur pvs-4.2.ORIG/BDD/mu/src/main.c pvs-4.2/BDD/mu/src/main.c
--- pvs-4.2.ORIG/BDD/mu/src/main.c 1998-12-31 13:30:32.000000000 -0700
+++ pvs-4.2/BDD/mu/src/main.c 2010-01-01 14:43:32.838597226 -0700
@@ -173,7 +173,7 @@
return 1;
}
- bdd_init ();
+ BDD_bdd_init ();
mu_init ();
if (optind == argc)
diff -dur pvs-4.2.ORIG/BDD/mu/src/mu.c pvs-4.2/BDD/mu/src/mu.c
--- pvs-4.2.ORIG/BDD/mu/src/mu.c 2009-10-04 13:25:53.000000000 -0600
+++ pvs-4.2/BDD/mu/src/mu.c 2010-01-01 14:49:32.575722103 -0700
@@ -753,7 +753,7 @@
int size_Tkplus1;
int size_Front;
- size_Tkplus1 = bdd_size (Tkplus1);
+ size_Tkplus1 = BDD_bdd_size (Tkplus1);
if (mu_use_restrict)
Front = bdd_restrict (Tkplus1, Tknot);
@@ -763,7 +763,7 @@
else
Front = bdd_and (Tkplus1, Tknot);
- size_Front = bdd_size (Front);
+ size_Front = BDD_bdd_size (Front);
bdd_free (Tknot);
@@ -928,7 +928,7 @@
/* D_sprintf (buf, bdd_count_sat_assignments (R, Domain), 0); */
fprintf (stdout, "Reachable took %.2f msec (%u BDD nodes).\n",
(clock () - start_t) / CLOCKS_PER_MSEC,
- bdd_size (R));
+ BDD_bdd_size (R));
fflush (stdout);
bdd_free (Domain);
}
@@ -1954,7 +1954,7 @@
R_VAR_VALUE (var) = R = mu_interpret_term (T, Ip, NULL);
if (mu_verbose) {
- fprintf (stdout, "done (%d BDD nodes).\n", bdd_size (R));
+ fprintf (stdout, "done (%d BDD nodes).\n", BDD_bdd_size (R));
fflush (stdout);
}
@@ -1991,7 +1991,7 @@
if (mu_verbose) {
fprintf (stdout, "Definition for `%s' took %.2f msec (%d BDD nodes).\n",
name, (clock () - start_t) / CLOCKS_PER_MSEC,
- bdd_size (R));
+ BDD_bdd_size (R));
fflush (stdout);
}
}
diff -dur pvs-4.2.ORIG/BDD/mu/src/yacc.y pvs-4.2/BDD/mu/src/yacc.y
--- pvs-4.2.ORIG/BDD/mu/src/yacc.y 2007-04-01 02:10:09.000000000 -0600
+++ pvs-4.2/BDD/mu/src/yacc.y 2010-01-01 14:49:43.862504601 -0700
@@ -166,7 +166,7 @@
R = mu_interpret_formula ($1, Ip, NULL);
bdd_print_as_sum_of_cubes (stdout, R, 0);
if (mu_verbose)
- fprintf (stdout, "Formula amounts to %d BDD nodes.\n", bdd_size (R));
+ fprintf (stdout, "Formula amounts to %d BDD nodes.\n", BDD_bdd_size (R));
bdd_free (R);
mu_free_formula ($1);
}
diff -dur pvs-4.2.ORIG/BDD/mu_interface.c pvs-4.2/BDD/mu_interface.c
--- pvs-4.2.ORIG/BDD/mu_interface.c 2009-10-04 13:25:53.000000000 -0600
+++ pvs-4.2/BDD/mu_interface.c 2010-01-01 14:47:29.920596857 -0700
@@ -258,7 +258,7 @@
mu_free_formula(fml);
/* bdd_print_as_sum_of_cubes (stdout, R,0) ; */
if (mu_verbose) {
- fprintf (stdout, "Formula amounts to %d BDD nodes.\n", bdd_size (R));
+ fprintf (stdout, "Formula amounts to %d BDD nodes.\n", BDD_bdd_size (R));
fflush (stdout);
}
return R;
diff -dur pvs-4.2.ORIG/BDD/mu.lisp pvs-4.2/BDD/mu.lisp
--- pvs-4.2.ORIG/BDD/mu.lisp 2009-12-29 01:45:35.000000000 -0700
+++ pvs-4.2/BDD/mu.lisp 2010-01-01 14:43:48.194596776 -0700
@@ -59,7 +59,7 @@
(defun run-musimp (ps fnums dynamic-ordering? irredundant? verbose?)
- (bdd_init)
+ (BDD_bdd_init)
;; Need to look at this, or somehow it gets a nonzero value
(bdd-interrupted?)
(mu_init)
diff -dur pvs-4.2.ORIG/pvs.system pvs-4.2/pvs.system
--- pvs-4.2.ORIG/pvs.system 2010-01-01 14:32:41.874471788 -0700
+++ pvs-4.2/pvs.system 2010-01-01 14:44:02.007596582 -0700
@@ -260,7 +260,7 @@
#+lucid (precompile-generic-functions)
#+lcl4.1 (clos::flush-pv-caches)
#-(or cmu sbcl)
- (pvs::bdd_init)
+ (pvs::BDD_bdd_init)
(when *load-pvs-prelude*
(pvs::load-prelude))
#+allegro
diff -dur pvs-4.2.ORIG/src/pvs.lisp pvs-4.2/src/pvs.lisp
--- pvs-4.2.ORIG/src/pvs.lisp 2009-10-01 03:25:19.000000000 -0600
+++ pvs-4.2/src/pvs.lisp 2010-01-01 14:44:27.400721511 -0700
@@ -115,7 +115,7 @@
#+cmu (fmakunbound 'bdd_cofactor_neg_)
#+cmu (lf "bdd-cmu") #+sbcl (lf "bdd-sbcl")
#+cmu (lf "mu-cmu") #+sbcl (lf "mu-sbcl")
- (bdd_init)
+ (BDD_bdd_init)
#+cmu (lf "dfa-foreign-cmu") #+sbcl (lf "dfa-foreign-sbcl"))
(setq *started-with-minus-q*
(or dont-load-user-lisp
diff -dur pvs-4.2.ORIG/src/WS1S/ix86_64-Linux/Makefile pvs-4.2/src/WS1S/ix86_64-Linux/Makefile
--- pvs-4.2.ORIG/src/WS1S/ix86_64-Linux/Makefile 2008-12-15 01:43:07.000000000 -0700
+++ pvs-4.2/src/WS1S/ix86_64-Linux/Makefile 2010-01-01 14:36:03.189477043 -0700
@@ -14,15 +14,7 @@
SHELL = /bin/sh
VPATH = ..:../mona/BDD:../mona/DFA:../mona/Mem
-obj = analyze.o prefix.o product.o \
- quotient.o basic.o external.o \
- makebasic.o minimize.o printdfa.o \
- project.o dfa.o \
- bdd.o bdd_double.o bdd_external.o \
- bdd_manager.o hash.o bdd_dump.o \
- bdd_trace.o bdd_cache.o \
- dlmalloc.o mem.o \
- ws1s_extended_interface.o
+obj = ws1s_table.o ws1s_extended_interface.o -lmonadfa
.SUFFIXES:
.SUFFIXES: .c .o
@@ -34,7 +26,7 @@
$(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
ws1s.so : ${obj}
- $(LD) ../ws1s-ld-table $(LDFLAGS) -o ws1s.so ${obj}
+ $(CC) -shared $(CFLAGS) -o ws1s.so ${obj}
bdd.o: bdd.c bdd.h bdd_internal.h
bdd_double.o: bdd_double.c bdd.h bdd_internal.h
diff -dur pvs-4.2.ORIG/src/WS1S/ix86-Linux/Makefile pvs-4.2/src/WS1S/ix86-Linux/Makefile
--- pvs-4.2.ORIG/src/WS1S/ix86-Linux/Makefile 2006-09-04 18:29:55.000000000 -0600
+++ pvs-4.2/src/WS1S/ix86-Linux/Makefile 2010-01-01 14:35:19.105597056 -0700
@@ -14,15 +14,7 @@
SHELL = /bin/sh
VPATH = ..:../mona/BDD:../mona/DFA:../mona/Mem
-obj = analyze.o prefix.o product.o \
- quotient.o basic.o external.o \
- makebasic.o minimize.o printdfa.o \
- project.o dfa.o \
- bdd.o bdd_double.o bdd_external.o \
- bdd_manager.o hash.o bdd_dump.o \
- bdd_trace.o bdd_cache.o \
- dlmalloc.o mem.o \
- ws1s_extended_interface.o
+obj = ws1s_table.o ws1s_extended_interface.o -lmonadfa
.SUFFIXES:
.SUFFIXES: .c .o
@@ -34,7 +26,7 @@
$(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
ws1s.so : ${obj}
- $(LD) ../ws1s-ld-table $(LDFLAGS) -o ws1s.so ${obj}
+ $(CC) -shared $(CFLAGS) -o ws1s.so ${obj}
bdd.o: bdd.c bdd.h bdd_internal.h
bdd_double.o: bdd_double.c bdd.h bdd_internal.h
diff -dur pvs-4.2.ORIG/src/WS1S/lisp/dfa.lisp pvs-4.2/src/WS1S/lisp/dfa.lisp
--- pvs-4.2.ORIG/src/WS1S/lisp/dfa.lisp 2006-11-02 02:06:48.000000000 -0700
+++ pvs-4.2/src/WS1S/lisp/dfa.lisp 2010-01-01 14:50:38.749596895 -0700
@@ -292,7 +292,7 @@
(defun number-of-states (a) (mona-dfa-ns (address a)))
(defun start-state (a) (mona-dfa-s (address a)))
-(defun number-of-bdd-nodes (a) (mona-bdd-size (dfa-bddm (address a))))
+(defun number-of-bdd-nodes (a) (bdd-size (dfa-bddm (address a))))
(defun number-of-transitions (a) (mona-transition-table-size (address a)))
diff -dur pvs-4.2.ORIG/src/WS1S/ws1s-ld-table pvs-4.2/src/WS1S/ws1s-ld-table
--- pvs-4.2.ORIG/src/WS1S/ws1s-ld-table 2006-11-06 13:14:58.000000000 -0700
+++ pvs-4.2/src/WS1S/ws1s-ld-table 2010-01-01 14:50:08.331477095 -0700
@@ -46,7 +46,7 @@
ws1s___dfaPrint = dfaPrint ;
ws1s___dfaPrintGraphviz = dfaPrintGraphviz ;
ws1s___dfaPrintVerbose = dfaPrintVerbose ;
-ws1s___bdd_size = mona_bdd_size ;
+ws1s___bdd_size = bdd_size ;
ws1s___dfaSetup = dfaSetup ;
ws1s___dfaAllocExceptions = dfaAllocExceptions ;
ws1s___dfaStoreException = dfaStoreException ;
diff -dur pvs-4.2.ORIG/src/WS1S/ws1s_table.c pvs-4.2/src/WS1S/ws1s_table.c
--- pvs-4.2.ORIG/src/WS1S/ws1s_table.c 2006-11-06 13:14:58.000000000 -0700
+++ pvs-4.2/src/WS1S/ws1s_table.c 2010-01-01 14:51:27.140473890 -0700
@@ -182,8 +182,8 @@
int (*ws1s___dfaPrintVerbose)(int) = dfaPrintVerbose;
-extern int mona_bdd_size (int);
-int (*ws1s___bdd_size)(int) = mona_bdd_size;
+extern int bdd_size (int);
+int (*ws1s___bdd_size)(int) = bdd_size;
extern int dfaSetup (int);
pvs-4.2-sbcl.patch:
Makefile.in | 6
ess/dist-ess.lisp | 4
ess/lang/sb-term/rel/access.lisp | 13 +
ess/lang/sb-term/rel/sb-parser.lisp | 2
ess/lang/sb-term/rel/top.lisp | 4
pvs.in | 13 +
src/WS1S/lisp/dfa-foreign-sbcl.lisp | 275 ++++++++++++++++++++++++++++++++++++
src/defsystem.lisp | 4
src/globals.lisp | 2
src/ground-prover/prmacros.lisp | 2
src/list-decls.lisp | 4
src/pvs.lisp | 7
src/rahd/cocoa.lisp | 1
src/rahd/opencad.lisp | 3
src/rahd/rahd.lisp | 1
src/status-cmds.lisp | 2
src/utils.lisp | 2
17 files changed, 319 insertions(+), 26 deletions(-)
--- NEW FILE pvs-4.2-sbcl.patch ---
diff -durN pvs-4.2.ORIG/ess/dist-ess.lisp pvs-4.2/ess/dist-ess.lisp
--- pvs-4.2.ORIG/ess/dist-ess.lisp 2006-09-12 13:46:53.000000000 -0600
+++ pvs-4.2/ess/dist-ess.lisp 2010-01-01 17:37:56.808727140 -0700
@@ -112,8 +112,8 @@
(defun save-ess-lisp (ess-filename features)
(let ((feature-alist (filter-features features)))
- (let ((ess-string (format nil #-GCL "~{~A~:^, ~}."
- #+GCL "~{~A~^, ~}."
+ (let ((ess-string (format nil #-(or GCL sbcl) "~{~A~:^, ~}."
+ #+(or GCL sbcl) "~{~A~^, ~}."
(mapcar #'fourth feature-alist))))
(format t "Now disksaving ... ")
(let ((in-reborn-image-p nil)
diff -durN pvs-4.2.ORIG/ess/lang/sb-term/rel/access.lisp pvs-4.2/ess/lang/sb-term/rel/access.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/access.lisp 2004-12-08 16:07:08.000000000 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/access.lisp 2010-01-01 17:37:56.809721210 -0700
@@ -22,11 +22,16 @@
;;(in-package "SB" :nicknames '("SYNTAX-BOX"))
-(in-package :syntax-box :nicknames '(:sb)) (use-package :ergolisp)
-
-
-(use-package '(:oper :term :sort :sb-runtime :lang))
+#+sbcl
+(eval-when (:compile-toplevel :load-toplevel :execute)
+ (unless (find-package :syntax-box)
+ (defpackage :syntax-box (:nicknames "SB")
+ (:use :common-lisp :ergolisp :oper :term :sort :sb-runtime :lang)
+ (:shadowing-import-from :sb-int memq))))
+(in-package :syntax-box)
+#-sbcl (use-package :ergolisp)
+#-sbcl (use-package '(:oper :term :sort :sb-runtime :lang))
(defparameter *sb-package* (find-package :sb))
diff -durN pvs-4.2.ORIG/ess/lang/sb-term/rel/sb-parser.lisp pvs-4.2/ess/lang/sb-term/rel/sb-parser.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/sb-parser.lisp 2001-06-26 04:46:33.000000000 -0600
+++ pvs-4.2/ess/lang/sb-term/rel/sb-parser.lisp 2010-01-01 17:37:56.810727318 -0700
@@ -8,7 +8,7 @@
(export '( sb-parse ))
-(defparameter sb-abs-syn-package (find-package "syntax-box"))
+(defparameter sb-abs-syn-package (find-package :syntax-box))
(defun sb-parse (&key (nt 'meta-grammar) error-threshold ask-about-bad-tokens
(return-errors nil) (stream nil streamp) string file (exhaust-stream nil))
diff -durN pvs-4.2.ORIG/ess/lang/sb-term/rel/top.lisp pvs-4.2/ess/lang/sb-term/rel/top.lisp
--- pvs-4.2.ORIG/ess/lang/sb-term/rel/top.lisp 2009-01-23 14:03:38.000000000 -0700
+++ pvs-4.2/ess/lang/sb-term/rel/top.lisp 2010-01-01 17:37:56.810727318 -0700
@@ -29,9 +29,9 @@
(export '(sb sb-make))
-(defconstant sb-version "1 Feb 88")
+(defconstant-if-unbound sb-version "1 Feb 88")
-(defconstant gen-src-file-ext "lisp")
+(defconstant-if-unbound gen-src-file-ext "lisp")
(defmacro string-empty? (s)
diff -durN pvs-4.2.ORIG/Makefile.in pvs-4.2/Makefile.in
--- pvs-4.2.ORIG/Makefile.in 2009-07-30 05:12:11.000000000 -0600
+++ pvs-4.2/Makefile.in 2010-01-01 17:37:56.810727318 -0700
@@ -94,7 +94,7 @@
ifneq ($(SBCLISP_HOME),)
# Check that the given SBCLISP_HOME works
-SBCLISPEXE = $(SBCLISP_HOME)/run-sbcl.sh
+SBCLISPEXE = $(SBCLISP_HOME)/sbcl
ifeq ($(shell if [ -x "$(SBCLISPEXE)" ]; then echo OK; fi),OK)
SBCLVERSION = $(shell $(SBCLISPEXE) --version)
$(warning "$(SBCLVERSION)")
@@ -532,9 +532,7 @@
--eval "(unwind-protect \
(mk:operate-on-system :pvs :compile) \
(save-lisp-and-die \"$@\" \
- :toplevel (function startup-pvs) \
- :executable t \
- ))"
+ :toplevel (function startup-pvs)))"
-rm $(PVSPATH)BDD/$(PLATFORM)/bdd-sbcl.*
cp $(SBCLISPEXE) $(subst $(SYSTEM)-sbclisp,,$@)
cp $(PVSPATH)BDD/$(PLATFORM)/mu.$(LOAD-FOREIGN-EXTENSION) $(subst $(SYSTEM)-sbclisp,,$@)
diff -durN pvs-4.2.ORIG/pvs.in pvs-4.2/pvs.in
--- pvs-4.2.ORIG/pvs.in 2009-10-04 13:36:55.000000000 -0600
+++ pvs-4.2/pvs.in 2010-01-01 17:37:56.811727227 -0700
@@ -261,9 +261,9 @@
then PVSLISP=cmulisp
elif [ -x $binpath/runtime/pvs-cmulisp ]
then PVSLISP=cmulisp
- elif [ -x $binpath/devel/pvs-sbclisp ]
+ elif [ -e $binpath/devel/pvs-sbclisp ]
then PVSLISP=sbclisp
- elif [ -x $binpath/runtime/pvs-sbclisp ]
+ elif [ -e $binpath/runtime/pvs-sbclisp ]
then PVSLISP=sbclisp
else echo "No executable available in $binpath"
exit 1
@@ -271,11 +271,11 @@
fi
PVSIMAGE=pvs-$PVSLISP
-if [ -d $binpath/devel -a -x $binpath/devel/$PVSIMAGE -a ! "$pvsruntime" ]
+if [ -d $binpath/devel -a -e $binpath/devel/$PVSIMAGE -a ! "$pvsruntime" ]
then PATH=$binpath/devel:$binpath:$PVSPATH/bin:$PATH
LD_LIBRARY_PATH=$binpath/devel:$LD_LIBRARY_PATH
DYLD_LIBRARY_PATH=$binpath/devel:$DYLD_LIBRARY_PATH
-elif [ -d $binpath/runtime -a -x $binpath/runtime/$PVSIMAGE ]
+elif [ -d $binpath/runtime -a -e $binpath/runtime/$PVSIMAGE ]
then PATH=$binpath/runtime:$binpath:$PVSPATH/bin:$PATH
LD_LIBRARY_PATH=$binpath/runtime:$LD_LIBRARY_PATH
DYLD_LIBRARY_PATH=$binpath/runtime:$DYLD_LIBRARY_PATH
@@ -316,6 +316,11 @@
for lf in $lisploadfiles
do flags="$flags --load $lf"; done
fi
+ if [ -d $binpath/devel -a -e $binpath/devel/$PVSIMAGE ]; then
+ PVSIMAGE="/usr/bin/sbcl --core $binpath/devel/$PVSIMAGE"
+ else
+ PVSIMAGE="/usr/bin/sbcl --core $binpath/runtime/$PVSIMAGE"
+ fi
;;
esac
diff -durN pvs-4.2.ORIG/src/defsystem.lisp pvs-4.2/src/defsystem.lisp
--- pvs-4.2.ORIG/src/defsystem.lisp 2009-02-10 14:34:14.000000000 -0700
+++ pvs-4.2/src/defsystem.lisp 2010-01-01 17:37:56.812764439 -0700
@@ -1783,6 +1783,10 @@
(push :case-sensitive common-lisp:*features*)
(push :case-insensitive common-lisp:*features*))))
+#+sbcl
+(eval-when (:compile-toplevel :load-toplevel :execute)
+ (push #+:unix :case-sensitive #-:unix :case-insensitive
+ common-lisp:*features*))
#+(and allegro case-sensitive ics)
(compiler-type-translation "excl 6.1" "excl-m")
diff -durN pvs-4.2.ORIG/src/globals.lisp pvs-4.2/src/globals.lisp
--- pvs-4.2.ORIG/src/globals.lisp 2009-10-04 12:51:41.000000000 -0600
+++ pvs-4.2/src/globals.lisp 2010-01-01 17:37:56.813727247 -0700
@@ -293,7 +293,7 @@
;; Used to keep track of which expression have already gone through
;; check-type-actuals processing
-(defvar *exprs-generating-actual-tccs*)
+(defvar *exprs-generating-actual-tccs* nil)
;;; Associate old tcc names with new tccs, so that proofs may be restored.
(defvar *old-tcc-names* nil)
diff -durN pvs-4.2.ORIG/src/ground-prover/prmacros.lisp pvs-4.2/src/ground-prover/prmacros.lisp
--- pvs-4.2.ORIG/src/ground-prover/prmacros.lisp 2009-10-04 13:18:01.000000000 -0600
+++ pvs-4.2/src/ground-prover/prmacros.lisp 2010-01-01 17:37:56.813727247 -0700
@@ -59,7 +59,7 @@
(defconstant-if-unbound *eqarithrels* '(greatereqp lesseqp))
-(defconstant *ifops* '(if if*))
+(defconstant-if-unbound *ifops* '(if if*))
(defconstant-if-unbound *boolconstants* '(false true))
diff -durN pvs-4.2.ORIG/src/list-decls.lisp pvs-4.2/src/list-decls.lisp
--- pvs-4.2.ORIG/src/list-decls.lisp 2008-07-17 05:03:22.000000000 -0600
+++ pvs-4.2/src/list-decls.lisp 2010-01-01 17:55:15.756471800 -0700
@@ -103,7 +103,7 @@
(pvs-message "~a has not been typechecked" oname)))
(defun typechecked-origin? (name origin)
- (case (intern (string-downcase origin))
+ (case (intern (#+allegro string-downcase #-allegro string-upcase origin))
((ppe tccs) (get-theory name))
((prelude prelude-theory) t)
(t (typechecked-file? name))))
@@ -301,7 +301,7 @@
(values object containing-type)))
(defun get-syntactic-objects-for (name origin)
- (case (intern (string-downcase origin))
+ (case (intern (#+allegro string-downcase #-allegro string-upcase origin))
(ppe (let ((theory (get-theory name)))
(when theory
(values (ppe-form theory) (list theory)))))
diff -durN pvs-4.2.ORIG/src/pvs.lisp pvs-4.2/src/pvs.lisp
--- pvs-4.2.ORIG/src/pvs.lisp 2009-10-01 03:25:19.000000000 -0600
+++ pvs-4.2/src/pvs.lisp 2010-01-01 17:51:42.197846781 -0700
@@ -2129,7 +2129,9 @@
(unproved? (pvs-message "No more unproved formulas below"))
(t (pvs-message
"Not at a formula declaration~@[ - ~a buffer may be invalid~]"
- (car (member (intern (string-downcase origin)) '(tccs ppe))))))))
+ (car (member (intern #+allegro (string-downcase origin)
+ #-allegro (string-upcase origin))
+ '(tccs ppe))))))))
(defun prove-formula (theoryname formname rerun?)
(let ((theory (get-typechecked-theory theoryname)))
@@ -3251,7 +3253,8 @@
(defun show-strategy (strat-name)
- (let* ((strat-id (intern (string-downcase strat-name)))
+ (let* ((strat-id (intern #+allegro (string-downcase strat-name)
+ #-allegro (string-upcase strat-name)))
(strategy (or (gethash strat-id *rulebase*)
(gethash strat-id *steps*)
(gethash strat-id *rules*))))
diff -durN pvs-4.2.ORIG/src/rahd/cocoa.lisp pvs-4.2/src/rahd/cocoa.lisp
--- pvs-4.2.ORIG/src/rahd/cocoa.lisp 2009-02-09 15:35:00.000000000 -0700
+++ pvs-4.2/src/rahd/cocoa.lisp 2010-01-01 17:37:56.813727247 -0700
@@ -56,6 +56,7 @@
(format cocoa-gb-in cocoa-gb-str))
(#+allegro excl:run-shell-command
#+cmu extensions:run-program
+ #+sbcl sb-ext:run-program
"./cocoa-gb.bash")
(let ((computed-gbasis-lst nil))
(with-open-file (cocoa-gb-out (work-pathify "cocoa-gb.out") :direction :input)
diff -durN pvs-4.2.ORIG/src/rahd/opencad.lisp pvs-4.2/src/rahd/opencad.lisp
--- pvs-4.2.ORIG/src/rahd/opencad.lisp 2009-02-09 15:35:00.000000000 -0700
+++ pvs-4.2/src/rahd/opencad.lisp 2010-01-01 17:37:56.814726781 -0700
@@ -57,10 +57,11 @@
(let ((error-code
(#+allegro excl:run-shell-command
#+cmu extensions:run-program
+ #+sbcl sb-ext:run-program
"qepcad.bash")))
(fmt 10 "~% [CAD] :: Sys-call for QEPCAD.BASH successfull with exit code: ~A. ~%" error-code)
(if #+allegro (= error-code 0)
- #+cmu t ;; Need to learn how to get CMUCL error code here.
+ #-allegro t ;; Need to learn how to get CMUCL error code here.
(with-open-file (cad-output "proofobl.out" :direction :input)
(let ((cad-decision (read-line cad-output nil)))
(fmt 10 "~% [CAD] :: CAD decision: ~A ; Generic? ~A. ~%" cad-decision generic)
diff -durN pvs-4.2.ORIG/src/rahd/rahd.lisp pvs-4.2/src/rahd/rahd.lisp
--- pvs-4.2.ORIG/src/rahd/rahd.lisp 2009-03-12 05:38:12.000000000 -0600
+++ pvs-4.2/src/rahd/rahd.lisp 2010-01-01 17:37:56.814726781 -0700
@@ -133,6 +133,7 @@
(fmt 0 "..... DONE.~%")
(fmt 0 " Marking executable +x .......")
(#+allegro excl:run-shell-command #+cmu extensions:run-program
+ #+sbcl sb-ext:run-program
(format nil "chmod +x ~A.exec" build-name))
(fmt 0 "..... DONE.~%~% >> [RAHD-BUILD-STAND-ALONE]: Process complete.~%"))
t)
diff -durN pvs-4.2.ORIG/src/status-cmds.lisp pvs-4.2/src/status-cmds.lisp
--- pvs-4.2.ORIG/src/status-cmds.lisp 2009-10-01 03:21:49.000000000 -0600
+++ pvs-4.2/src/status-cmds.lisp 2010-01-01 17:55:52.105472232 -0700
@@ -1007,7 +1007,7 @@
(if (and (member origin '("ppe" "tccs") :test #'string=)
(not (get-theory bufname)))
(pvs-message "~a is not typechecked" bufname)
- (case (intern (string-downcase origin))
+ (case (intern (#+allegro string-downcase #-allegro string-upcase origin))
(ppe (let* ((theories (ppe-form (get-theory bufname)))
(decl (get-decl-at line t theories)))
(values (find-if #'(lambda (d) (and (declaration? d)
diff -durN pvs-4.2.ORIG/src/utils.lisp pvs-4.2/src/utils.lisp
--- pvs-4.2.ORIG/src/utils.lisp 2009-10-03 01:06:12.000000000 -0600
+++ pvs-4.2/src/utils.lisp 2010-01-01 17:37:56.815722776 -0700
@@ -322,7 +322,7 @@
#+sbcl
(defun working-directory ()
- (pathname (sb-posix:getcwd)))
+ (make-pathname :directory (sb-posix:getcwd)))
#+sbcl
(defun set-working-directory (dir)
diff -durN pvs-4.2.ORIG/src/WS1S/lisp/dfa-foreign-sbcl.lisp pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp
--- pvs-4.2.ORIG/src/WS1S/lisp/dfa-foreign-sbcl.lisp 1969-12-31 17:00:00.000000000 -0700
+++ pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp 2010-01-01 17:37:56.816479976 -0700
@@ -0,0 +1,275 @@
+;; --------------------------------------------------------------------
+;; PVS
+;; Copyright (C) 2006, SRI International. All Rights Reserved.
+
+;; This program is free software; you can redistribute it and/or
+;; modify it under the terms of the GNU General Public License
+;; as published by the Free Software Foundation; either version 2
+;; of the License, or (at your option) any later version.
+
+;; 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
+;; GNU General Public License for more details.
+
+;; You should have received a copy of the GNU General Public License
+;; along with this program; if not, write to the Free Software
+;; Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
+;; --------------------------------------------------------------------
+
+(in-package :pvs)
+
+;; Structure of a DFA in foreign space
+(sb-alien:define-alien-type nil
+ (sb-alien:struct mona-dfa
+ (bddm (* t)) ; Manager of BDD nodes
+ (ns (integer 32)) ; Number of states
+ (q (* t)) ; Transition array
+ (s (integer 32)) ; Start State
+ (f (* (integer 32))))) ; State Status Array
+
+;; Predefined basic automata
+
+(sb-alien:define-alien-routine ("ws1s___dfaTrue" mona-true) ; true
+ (* (sb-alien:struct mona-dfa)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaFalse" mona-false) ; false
+ (* (sb-alien:struct mona-dfa)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaConst" mona-const) ; p_i = n
+ (* (sb-alien:struct mona-dfa))
+ (n (integer 32)) (i (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaLess" mona-less) ; p_i < p_j
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaLesseq" mona-lesseq) ; p_i <= p_j
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPlus1" mona-plus1) ; p_i = p_j + n
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)) (n (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaMinus1" mona-minus1) ; p_i = p_i - p_j
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaEq1" mona-eq1) ; p_i = p_j
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaEq2" mona-eq2) ; P_i = P_j
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPlus2" mona-plus2) ; P_i = P_j + 1
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaMinus2" mona-minus2) ; P_i = P_j - 1
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPlusModulo1" mona-plusmodulo1) ; p_i = p_j + 1 % p_k
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)) (k (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaMinusModulo1" mona-minusmodulo1) ; p_i = p_j - 1 % p_k
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)) (k (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaEmpty" mona-empty) ; P_i = empty
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaIn" mona-in) ; p_i in P_j recognizes <X,X>(<0,X>+)<1,1>(<X,X>*)
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaSubset" mona-subset) ; P_i sub P_j
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaUnion" mona-union) ; P_i = P_j union P_k
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)) (k (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaInter" mona-intersection) ; P_i = P_j inter P_k
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)) (k (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaSetminus" mona-difference) ; P_i = P_j \ P_k
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)) (k (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaMax" mona-max) ; p_i = max(P_j)
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaMin" mona-min) ; p_i = min(P_j)
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (j (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaBoolvar" mona-boolvar) ; b_i
+ (* (sb-alien:struct mona-dfa))
+ (b (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPresbConst" mona-presburger-const) ; P_i = pconst(n)
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)) (n (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaSingleton" mona-singleton) ; singleton(P_i)
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaFirstOrder" mona-first-order) ; recognizes 0*1+
+ (* (sb-alien:struct mona-dfa))
+ (i (integer 32)))
+
+
+;; Automaton operations
+
+(sb-alien:define-alien-routine ("ws1s___dfaFree" mona-free!)
+ sb-alien:void
+ (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaNegation" mona-negation!)
+ sb-alien:void
+ (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaRestrict" mona-restrict!)
+ sb-alien:void
+ (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaUnrestrict" mona-unrestrict!)
+ sb-alien:void
+ (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaCopy" mona-copy)
+ (* (sb-alien:struct mona-dfa))
+ (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaProduct" mona-product)
+ (* (sb-alien:struct mona-dfa))
+ (a1 (* (sb-alien:struct mona-dfa)))
+ (a2 (* (sb-alien:struct mona-dfa)))
+ (mode (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPrefixClose" mona-prefix-close!)
+ sb-alien:void
+ (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaConjunction" mona-conjunction)
+ (* (sb-alien:struct mona-dfa))
+ (a1 (* (sb-alien:struct mona-dfa))) (a2 (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaDisjunction" mona-disjunction)
+ (* (sb-alien:struct mona-dfa))
+ (a1 (* (sb-alien:struct mona-dfa))) (a2 (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaImplication" mona-implication)
+ (* (sb-alien:struct mona-dfa))
+ (a1 (* (sb-alien:struct mona-dfa))) (a2 (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaIff" mona-iff)
+ (* (sb-alien:struct mona-dfa))
+ (a1 (* (sb-alien:struct mona-dfa))) (a2 (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaStatus" mona-status)
+ (integer 32)
+ (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaProject" mona-project)
+ ; projects away track var_index from a and
+ ; determinizes the resulting automaton
+ (* (sb-alien:struct mona-dfa))
+ (a (* (sb-alien:struct mona-dfa))) (index (sb-alien:unsigned 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaRightQuotient" mona-right-quotient!)
+ sb-alien:void
+ (a (* (sb-alien:struct mona-dfa))) (index (sb-alien:unsigned 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaMinimize" mona-minimize) ; Minimization
+ (* (sb-alien:struct mona-dfa))
+ (a (* (sb-alien:struct mona-dfa))))
+
+
+;; Analysis and printing
+
+(sb-alien:define-alien-routine ("ws1s___dfaMakeExample" mona-make-example)
+ sb-alien:c-string
+ (a (* (sb-alien:struct mona-dfa)))
+ (kind (integer 32))
+ (num (integer 32))
+ (indices (array (sb-alien:unsigned 32))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaAnalyze" mona-analyze)
+ sb-alien:void
+ (a (* (sb-alien:struct mona-dfa)))
+ (num (integer 32))
+ (names (array sb-alien:c-string))
+ (indices (array sb-alien:unsigned))
+ (orders (array sb-alien:char))
+ (treestyle (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPrintVitals" mona-print-vitals)
+ sb-alien:void
+ (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPrint" mona-print)
+ sb-alien:void
+ (a (* (sb-alien:struct mona-dfa)))
+ (num (integer 32))
+ (names (array sb-alien:c-string))
+ (indices (array (sb-alien:unsigned 32))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPrintGraphviz" mona-print-graphviz)
+ sb-alien:void
+ (a (* (sb-alien:struct mona-dfa)))
+ (num (integer 32))
+ (indices (array (sb-alien:unsigned 32))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaPrintVerbose" mona-print-verbose)
+ sb-alien:void
+ (a (* (sb-alien:struct mona-dfa))))
+
+(sb-alien:define-alien-routine ("ws1s___bdd_size" bdd-size)
+ (sb-alien:unsigned 32)
+ (bbdm (* t)))
+
+
+;; Constructing Automata Explicitly
+
+(sb-alien:define-alien-routine ("ws1s___dfaSetup" mona-setup)
+ sb-alien:void
+ (s (integer 32))
+ (len (integer 32))
+ (indices (array (integer 32))))
+
+(sb-alien:define-alien-routine ("ws1s___dfaAllocExceptions" mona-alloc-exceptions)
+ sb-alien:void
+ (n (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaStoreException" mona-store-exception)
+ sb-alien:void
+ (s (integer 32)) (path sb-alien:c-string))
+
+(sb-alien:define-alien-routine ("ws1s___dfaStoreState" mona-store-state)
+ sb-alien:void
+ (s (integer 32)))
+
+(sb-alien:define-alien-routine ("ws1s___dfaBuild" mona-build)
+ (* (sb-alien:struct mona-dfa))
+ (statuses (array sb-alien:char)))
+
+;; Exporting
+
+(sb-alien:define-alien-routine ("ws1s___dfaExport" mona-export)
+ (integer 32)
+ (a (* (sb-alien:struct mona-dfa)))
+ (filename sb-alien:c-string)
+ (num (integer 32))
+ (names (array sb-alien:c-string))
+ (orders (array sb-alien:char)))
--- NEW FILE pvs-sbcl.desktop ---
[Desktop Entry]
Version=1.0
Type=Application
Name=PVS (SBCL Build)
GenericName=PVS
Comment=An interactive theorem prover
TryExec=pvs-sbcl
Exec=pvs-sbcl %F
MimeType=image/x-pvs;
Terminal=false
Categories=Application;Development
--- NEW FILE pvs-sbcl.spec ---
Name: pvs-sbcl
Version: 4.2
Release: 2.20100104svn%{?dist}
Summary: Interactive theorem prover from SRI
Group: Applications/Engineering
License: GPLv2+
URL: http://pvs.csl.sri.com/
# SBCL support is only available in the post-4.2 release subversion repository.
# Use the following commands to generate the source tarball corresponding to
# this release:
# svn export -r 5482 https://spartan.csl.sri.com/svn/public/pvs/trunk pvs-4.2
# tar cf pvs-4.2.tar pvs-4.2
# xz pvs-4.2.tar
Source0: pvs-4.2.tar.xz
#Source0: http://pvs.csl.sri.com/download-open/pvs-%{version}-source.tgz
Source1: http://pvs.csl.sri.com/doc/pvs-prelude.pdf
Source2: http://pvs.csl.sri.com/doc/interpretations.pdf
Source3: http://pvs.csl.sri.com/papers/csl-97-2/csl-97-2.ps.gz
Source4: http://pvs.csl.sri.com/papers/csl-93-9/csl-93-9.ps.gz
Source5: pvs-sbcl.desktop
# This patch was sent upstream on 4 Jan 2010. Use the fancyhdr package instead
# of the obsolete fancyheadings package. Don't make Emacs kill an already
# dead process. Refer to the bibliography file in the sources.
Patch0: pvs-4.2-latex.patch
# This patch was sent upstream on 4 Jan 2010. Make a couple of minor updates
# to configure.in to allow processing by autoconf 2.62 and later. In
# particular, the invocation of AC_INIT needs to happen sooner.
Patch1: pvs-4.2-autoconf.patch
# This patch was sent upstream on 4 Jan 2010. Run sbcl as 'sbcl' instead of
# 'run-sbcl.sh'. Make source code changes required by recent versions of SBCL.
Patch2: pvs-4.2-sbcl.patch
# This patch was sent upstream on 4 Jan 2010. Add support for Emacs 23.
Patch3: pvs-4.2-emacs.patch
# This patch was sent upstream on 4 Jan 2010. Fix a few ANSI CL constructs
# that aren't quite ANSI.
Patch4: pvs-4.2-ansi.patch
# This patch will not be sent upstream, as it is Fedora-specific. Link with
# gcc instead of ld to get a build-id and link against libc.
Patch5: pvs-4.2-build-id.patch
# This patch will not be sent upstream, as it is Fedora-specific. Link
# against a system copy of the mona library, rather than compiling in the
# mona sources embedded in the PVS sources.
Patch6: pvs-4.2-mona.patch
BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
BuildRequires: autoconf, sbcl, texinfo-tex, tex(latex), mona-devel
BuildRequires: emacs, emacs-el, xemacs-devel, xemacs-packages-extra
BuildRequires: desktop-file-utils
Requires: sbcl = 1.0.30, tex(latex)
Requires(postun): desktop-file-utils
Provides: pvs = %{version}-%{release}, pvsio = %{version}-%{release}
# Fedora SBCL is only available on Intel platforms
ExclusiveArch: %ix86 x86_64
%description
PVS is a verification system: that is, a specification language integrated
with support tools and a theorem prover. It is intended to capture the
state-of-the-art in mechanized formal methods and to be sufficiently rugged
that it can be used for significant applications.
This build of PVS must be invoked as "pvs-sbcl", both to distinguish it from
builds with other Common Lisp engines, and to distinguish it from /sbin/pvs in
the lvm2 package.
%prep
%setup -q -n pvs-4.2
%patch0 -p1
%patch1 -p1
%patch2 -p1
%patch3 -p1
%patch4 -p1
%patch5 -p1
%patch6 -p1
autoconf
%build
%configure CFLAGS="$RPM_OPT_FLAGS -fPIC -fno-strict-aliasing"
make SBCLISP_HOME=%{_bindir}
# Now that we're done building, we don't want the devel version
rm -fr bin/*/devel
# We also don't want the useless copy of the sbcl binary
rm -f bin/*/runtime/sbcl
# Run it once to force Lisp compilation of the native interfaces
bin/relocate > /dev/null
echo -e '(sb-ext:quit :recklessly-p t)' | ./pvs -raw
# Get rid of some emacs save files and CVS control files
find . -name .cvsignore -o -name \*~ | xargs rm -f
# Get rid of some temporary files we no longer need
rm -f doc/release-notes/pvs-release-notes.{pg,ky,tp,fn,cp,vr}
# Build the documentation
make -C doc/api pvs-api.pdf
make -C doc/language language.pdf
make -C doc/prover prover.pdf
make -C doc/release-notes pvs-release-notes.info
make -C doc/release-notes pvs-release-notes.pdf
make -C doc/user-guide user-guide.pdf
# No sources for the prelude docs
cp -p %{SOURCE1} .
# Cannot be built: needs cslreport.cls
# pushd doc/interpretations
# pdflatex interpretations
# popd
cp -p %{SOURCE2} .
# Cannot be built: missing cslreport.cls
# make -C doc/semantics semantics.pdf
cp -p %{SOURCE3} .
# Cannot be built: missing /homes/rushby/tex/prelude
# make -C doc/datatypes datatypes.pdf
cp -p %{SOURCE4} .
# Mimic the effects of the relocate script for the installed location
sed -i -e "s,^PVSPATH=.*$,PVSPATH=%{_libdir}/pvs," pvs
sed -i -e "s,^PVSPATH=.*$,PVSPATH=%{_libdir}/pvs," pvsio
%install
rm -rf $RPM_BUILD_ROOT
mkdir -p $RPM_BUILD_ROOT%{_bindir}
mkdir -p $RPM_BUILD_ROOT%{_libdir}/pvs/doc/release-notes
mkdir -p $RPM_BUILD_ROOT%{_datadir}/applications
mkdir -p $RPM_BUILD_ROOT%{_datadir}/texmf/tex/latex/pvs
cp -a bin emacs lib pvs-tex.sub wish $RPM_BUILD_ROOT%{_libdir}/pvs
cp -a doc/release-notes/pvs-release-notes.info $RPM_BUILD_ROOT%{_libdir}/pvs/doc/release-notes
cp -a pvs.sty $RPM_BUILD_ROOT%{_datadir}/texmf/tex/latex/pvs
cp -a pvs $RPM_BUILD_ROOT%{_bindir}/pvs-sbcl
cp -a pvsio $RPM_BUILD_ROOT%{_bindir}
# We don't need the make-dist or relocate scripts
rm -f $RPM_BUILD_ROOT%{_libdir}/pvs/bin/make-dist
rm -f $RPM_BUILD_ROOT%{_libdir}/pvs/bin/relocate
# Remove a left-over make artifact
rm -f $RPM_BUILD_ROOT%{_libdir}/pvs/emacs/*/.readme
# Install the desktop file
desktop-file-install --mode=644 --dir=$RPM_BUILD_ROOT%{_datadir}/applications \
%{SOURCE5}
%clean
rm -rf $RPM_BUILD_ROOT
rm -f /tmp/pvs-*.p1
%postun
if [ $1 -eq 0 ]; then
/usr/bin/mktexlsr
update-desktop-database %{_datadir}/applications &>/dev/null
fi
%posttrans
/usr/bin/mktexlsr
update-desktop-database %{_datadir}/applications &>/dev/null
%files
%defattr(-,root,root,-)
%doc *.ps.gz *.pdf LICENSE NOTICES README Examples
%doc doc/PVSio-2.d.pdf doc/api/pvs-api.pdf
%doc doc/language/language.pdf
%doc doc/prover/prover.pdf doc/release-notes/pvs-release-notes.pdf
%{_bindir}/pvs*
%{_libdir}/pvs
%{_datadir}/applications/*.desktop
%{_datadir}/texmf/tex/latex/pvs
%changelog
* Mon Jan 4 2010 Jerry James <loganjerry at gmail.com> - 4.2-2.20100104svn
- Update to 20100104 snapshot.
- Fix mona patch.
- Dump a non-executable SBCL image to avoid prelink and strip issues.
- Solve the build-time hang in (X)Emacs.
* Tue Dec 22 2009 Jerry James <loganjerry at gmail.com> - 4.2-2.20091008svn
- Attempt to solve build-time hang in (X)Emacs.
- Don't fail if sbcl has not been prelinked.
* Mon Dec 21 2009 Jerry James <loganjerry at gmail.com> - 4.2-1.20091008svn
- Initial RPM
Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/pvs-sbcl/F-11/.cvsignore,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- .cvsignore 4 Jan 2010 20:10:58 -0000 1.1
+++ .cvsignore 4 Jan 2010 22:20:56 -0000 1.2
@@ -0,0 +1,5 @@
+csl-93-9.ps.gz
+csl-97-2.ps.gz
+interpretations.pdf
+pvs-4.2.tar.xz
+pvs-prelude.pdf
Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/pvs-sbcl/F-11/sources,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- sources 4 Jan 2010 20:10:58 -0000 1.1
+++ sources 4 Jan 2010 22:20:57 -0000 1.2
@@ -0,0 +1,5 @@
+9646a3fa12ae6112c4ddd17e4a14c846 csl-93-9.ps.gz
+6fd7d301fb569cacb8aa9fb6278498a8 csl-97-2.ps.gz
+3c763226529517d39dfb962628492ec2 interpretations.pdf
+df79d45152a96953801ab2c5ca8d7741 pvs-4.2.tar.xz
+432c4e35d4b172b227c2c3dbe0afb6a6 pvs-prelude.pdf
- Previous message (by thread): rpms/libselinux/F-12 libselinux.spec,1.378,1.379 sources,1.191,1.192
- Next message (by thread): rpms/pvs-sbcl/devel pvs-4.2-ansi.patch, NONE, 1.1 pvs-4.2-autoconf.patch, NONE, 1.1 pvs-4.2-build-id.patch, NONE, 1.1 pvs-4.2-emacs.patch, NONE, 1.1 pvs-4.2-latex.patch, NONE, 1.1 pvs-4.2-mona.patch, NONE, 1.1 pvs-4.2-sbcl.patch, NONE, 1.1 pvs-sbcl.desktop, NONE, 1.1 pvs-sbcl.spec, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
More information about the fedora-extras-commits
mailing list