Go to:
Gentoo Home
Documentation
Forums
Lists
Bugs
Planet
Store
Wiki
Get Gentoo!
Gentoo's Bugzilla – Attachment 186215 Details for
Bug 257679
[ebuild request] sci-mathematics/pvs
Home
|
New
–
[Ex]
|
Browse
|
Search
|
Privacy Policy
|
[?]
|
Reports
|
Requests
|
Help
|
New Account
|
Log In
[x]
|
Forgot Password
Login:
[x]
[patch]
sci-mathematics/pvs/files/pvs-4.2-patch-sbcl
pvs-4.2-patch-sbcl (text/plain), 219.23 KB, created by
Jonathan-Christofer Demay
on 2009-03-25 10:45:04 UTC
(
hide
)
Description:
sci-mathematics/pvs/files/pvs-4.2-patch-sbcl
Filename:
MIME Type:
Creator:
Jonathan-Christofer Demay
Created:
2009-03-25 10:45:04 UTC
Size:
219.23 KB
patch
obsolete
>diff -Naur pvs4.2-orig/BDD/bdd-allegro.lisp pvs4.2-sbcl/BDD/bdd-allegro.lisp >--- pvs4.2-orig/BDD/bdd-allegro.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/BDD/bdd-allegro.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -39,6 +39,13 @@ > > ;;; #define NULL_LIST ((LIST) 0) > >+;;; int null_list_p (LIST x) >+(ff:def-foreign-call (null_list_p "bdd___null_list_p") >+ ((x :unsigned-int integer)) >+ #+(version>= 6) :strings-convert #+(version>= 6) nil >+ :arg-checking nil >+ :call-direct t >+ :returning :unsigned-int) > ;;; void *elem_contents (LIST_ELEM_PTR x) > (ff:def-foreign-call (elem_contents "bdd___elem_contents") > ((x :unsigned-int integer)) >diff -Naur pvs4.2-orig/BDD/bdd-cmu.lisp pvs4.2-sbcl/BDD/bdd-cmu.lisp >--- pvs4.2-orig/BDD/bdd-cmu.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/BDD/bdd-cmu.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -39,6 +39,11 @@ > > ;;; #define NULL_LIST ((LIST) 0) > >+;;; int null_list_p (LIST x) >+(alien:def-alien-routine ("bdd___null_list_p" null_list_p) >+ unsigned-int >+ (x unsigned-int)) >+ > ;;; void *elem_contents (LIST_ELEM_PTR x) > (alien:def-alien-routine ("bdd___elem_contents" elem_contents) > unsigned-int >diff -Naur pvs4.2-orig/BDD/bdd-ld-table pvs4.2-sbcl/BDD/bdd-ld-table >--- pvs4.2-orig/BDD/bdd-ld-table 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/BDD/bdd-ld-table 2009-03-24 18:56:17.000000000 +0000 >@@ -4,6 +4,7 @@ > bdd___bdd_poslit_p = bdd_poslit_p ; > bdd___bdd_neglit_p = bdd_neglit_p ; > bdd___bdd_equal_p = bdd_equal_p ; >+bdd___null_list_p = null_list_p ; > bdd___elem_contents = elem_contents ; > bdd___list_first = list_first ; > bdd___list_last = list_last ; >diff -Naur pvs4.2-orig/BDD/bdd.lisp pvs4.2-sbcl/BDD/bdd.lisp >--- pvs4.2-orig/BDD/bdd.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/BDD/bdd.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -19,6 +19,7 @@ > > (in-package :pvs) > >+(defmacro null-list? (list) `(= (null_list_p ,list) 1)) > (defmacro bdd-void? (bdd) `(= (bdd_void_p ,bdd) 1)) > (defmacro bdd-1? (bdd) `(= (bdd_1_p ,bdd) 1)) > (defmacro bdd-0? (bdd) `(= (bdd_0_p ,bdd) 1)) >@@ -369,12 +370,12 @@ > (pushnew (cons op name) (cdr entry) :test #'eql :key #'cdr)))))) > > (defun translate-from-bdd-list (bddlist) >- (let ((bdds (unless (zerop bddlist) >+ (let ((bdds (unless (null-list? bddlist) > (translate-from-bdd-list* (list_first bddlist))))) > (mapcar #'translate-bdd-cube bdds))) > > (defun translate-from-bdd-list* (bddlist &optional result) >- (if (zerop bddlist) >+ (if (null-list? bddlist) > (nreverse result) > (translate-from-bdd-list* > (list_next bddlist) >diff -Naur pvs4.2-orig/BDD/bdd-sbcl.lisp pvs4.2-sbcl/BDD/bdd-sbcl.lisp >--- pvs4.2-orig/BDD/bdd-sbcl.lisp 1970-01-01 00:00:00.000000000 +0000 >+++ pvs4.2-sbcl/BDD/bdd-sbcl.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -0,0 +1,550 @@ >+;; -------------------------------------------------------------------- >+;; 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) >+ >+;; SO - We load this from pvs-init (in src/pvs.lisp), as it requires mu.so, >+;; but if mu.so is loaded at save-lisp time, it doesn't work (at least I >+;; can't get it to). >+ >+;;; List accessors >+;;; Lists in the BDD package involve two structures. >+ >+;;; A LIST is a structure with slots for a first element pointer, a last >+;;; element pointer, the size, and user-defined info. >+ >+;;; A LIST_ELEM is a structure with slots for the contents and the next >+;;; element. >+ >+;;; #define NULL_LIST ((LIST) 0) >+ >+;;; void *elem_contents (LIST_ELEM_PTR x) >+(sb-alien:define-alien-routine ("bdd___elem_contents" elem_contents) >+ (* t) >+ (x (* t))) >+ >+;;; LIST_ELEM_PTR list_first (LIST x) >+(sb-alien:define-alien-routine ("bdd___list_first" list_first) >+ (* t) >+ (x (* t))) >+ >+;;; LIST_ELEM_PTR list_last (LIST x) >+(sb-alien:define-alien-routine ("bdd___list_last" list_last) >+ (* t) >+ (x (* t))) >+ >+;;; int list_info (LIST x) >+(sb-alien:define-alien-routine ("bdd___list_info" list_info) >+ (integer 32) >+ (x (* t))) >+ >+;;; LIST_ELEM_PTR list_next (LIST_ELEM_PTR x) >+(sb-alien:define-alien-routine ("bdd___list_next" list_next) >+ (* t) >+ (x (* t))) >+ >+;;; This pretty much follows the bdd.doc sections. >+ >+;;; User settable program parameters >+;;; -------------------------------- >+;;; int bdd_do_gc; /* default 1 */ >+ >+(sb-alien:define-alien-variable "bdd_do_gc" (integer 32)) >+ >+;;; set_bdd_do_gc (int flag) >+(declaim (inline set_bdd_do_gc)) >+(defun set_bdd_do_gc (flag) >+ (setf bdd-do-gc flag)) >+ >+;;; int bdd_do_dynamic_ordering;/* default 1 */ >+(sb-alien:define-alien-variable "bdd_do_dynamic_ordering" (integer 32)) >+ >+;;; set_bdd_do_dynamic_ordering (int flag) >+(declaim (inline set_bdd_do_dynamic_ordering)) >+(defun set_bdd_do_dynamic_ordering (flag) >+ (setf bdd-do-dynamic-ordering flag)) >+ >+;;; int bdd_verbose; /* default 0 */ >+(sb-alien:define-alien-variable "bdd_verbose" (integer 32)) >+ >+;;; set_bdd_verbose (int flag) >+(declaim (inline set_bdd_verbose)) >+(defun set_bdd_verbose (flag) >+ (setf bdd-verbose flag)) >+ >+;;; int bdd_use_neg_edges; /* default 1*/ >+(sb-alien:define-alien-variable "bdd_use_neg_edges" (integer 32)) >+ >+;;; set_bdd_use_neg_edges (int flag) >+(declaim (inline set_bdd_use_neg_edges)) >+(defun set_bdd_use_neg_edges (flag) >+ (setf bdd-use-neg-edges flag)) >+ >+;;; int bdd_use_inv_edges; /* default 1; 0 when bdd_do_dynamic_ordering = 1 */ >+(sb-alien:define-alien-variable "bdd_use_inv_edges" (integer 32)) >+ >+;;; set_bdd_use_inv_edges (int flag) >+(declaim (inline set_bdd_use_inv_edges)) >+(defun set_bdd_use_inv_edges (flag) >+ (setf bdd-use-inv-edges flag)) >+ >+;;; int bdd_sizeof_user_data; /* default 0 */ >+;;; int BDD_COMPUTED_TABLE_SIZE;/* default DEFAULT_BDD_COMPUTED_TABLE_SIZE */ >+;;; int BDD_HASHTAB_SIZE; /* default DEFAULT_BDD_HASHTAB_SIZE */ >+;;; int BDD_NR_RANKS; /* default DEFAULT_BDD_NR_RANKS */ >+;;; int BDD_LOAD_FACTOR; /* default DEFAULT_BDD_LOAD_FACTOR */ >+ >+ >+;;; C preprocessor macros: >+;;; ---------------------- >+ >+;;; Access to fields of BDD struct: >+ >+;;; BDD_VARID (F) >+;;; bdd_varid (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_varid" bdd_varid) >+ (sb-alien:unsigned 32) >+ (f (* t))) >+ >+;;; BDD_THEN (F) >+;;; BDD_ELSE (F) >+;;; BDD_REFCOUNT (F) >+;;; BDD_FLAG (F) >+;;; BDD_MARK (F) >+ >+ >+;;; Test on terminal nodes: >+;;; ----------------------- >+ >+;;; BDD_VOID_P (f) >+;;; int bdd_void_p (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_void_p" bdd_void_p) >+ (integer 32) >+ (f (* t))) >+ >+;;; BDD_1_P (f) >+;;; bdd_1_p (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_1_p" bdd_1_p) >+ (integer 32) >+ (f (* t))) >+ >+;;; BDD_0_P (f) >+;;; bdd_0_p (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_0_p" bdd_0_p) >+ (integer 32) >+ (f (* t))) >+ >+;;; BDD_X_P (f) >+;;; bdd_x_p (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_x_p" bdd_x_p) >+ (integer 32) >+ (f (* t))) >+ >+;;; BDD_CONST_P (f) >+;;; int bdd_const_p (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_const_p" bdd_const_p) >+ (integer 32) >+ (f (* t))) >+ >+;;; BDD_TERM_P (f) >+;;; bdd_term_p (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_term_p" bdd_term_p) >+ (integer 32) >+ (f (* t))) >+ >+;;; BDD_LIT_P (f) >+;;; bdd_lit_p (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_lit_p" bdd_lit_p) >+ (integer 32) >+ (f (* t))) >+ >+;;; BDD_POSLIT_P (f) >+;;; int bdd_poslit_p (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_poslit_p" bdd_poslit_p) >+ (integer 32) >+ (f (* t))) >+ >+;;; BDD_NEGLIT_P (f) >+;;; int bdd_neglit_p (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_neglit_p" bdd_neglit_p) >+ (integer 32) >+ (f (* t))) >+ >+;;; BDD_COFACTOR_POS (f) >+;;; BDDPTR bdd_cofactor_pos_ (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_cofactor_pos_" bdd_cofactor_pos_) >+ (* t) >+ (f (* t))) >+ >+;;; BDD_COFACTOR_NEG (f) >+;;; BDDPTR bdd_cofactor_neg_ (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_cofactor_neg_" bdd_cofactor_neg_) >+ (* t) >+ (f (* t))) >+ >+;;; void bdd_reset_marks (BDDPTR f) >+;;; 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) >+ (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) >+ sb-alien:void) >+ >+;;; void bdd_free (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_free" bdd_free) >+ sb-alien:void >+ (f (* t))) >+ >+;;; int bdd_gc (void) >+(sb-alien:define-alien-routine ("bdd___bdd_gc" bdd_gc) >+ (integer 32)) >+ >+;;; BDDPTR bdd_ite (BDDPTR F, BDDPTR G, BDDPTR H) >+(sb-alien:define-alien-routine ("bdd___bdd_ite" bdd_ite) >+ (* t) >+ (f (* t)) >+ (g (* t)) >+ (h (* t))) >+ >+;;; BDDPTR bdd_ite_const (BDDPTR F, BDDPTR G, BDDPTR H) >+(sb-alien:define-alien-routine ("bdd___bdd_ite_const" bdd_ite_const) >+ (* t) >+ (f (* t)) >+ (g (* t)) >+ (h (* t))) >+ >+;;; void bdd_cofactors (BDDPTR f, BDDPTR *vp, BDDPTR *Tp, BDDPTR *Ep) >+;;; BDDPTR bdd_invert_input_top (BDDPTR f) >+(sb-alien:define-alien-routine >+ ("bdd___bdd_invert_input_top" bdd_invert_input_top) >+ (* t) >+ (f (* t))) >+ >+;;; BDDPTR bdd_create_var (int v) >+(sb-alien:define-alien-routine ("bdd___bdd_create_var" bdd_create_var) >+ (* t) >+ (v (integer 32))) >+ >+;;; BDDPTR bdd_create_var_first (void) >+(sb-alien:define-alien-routine >+ ("bdd___bdd_create_var_first" bdd_create_var_first) >+ (* t)) >+ >+;;; BDDPTR bdd_create_var_before (BDDPTR v) >+(sb-alien:define-alien-routine >+ ("bdd___bdd_create_var_before" bdd_create_var_before) >+ (* t) >+ (v (* t))) >+ >+;;; BDDPTR bdd_create_var_after (BDDPTR v) >+(sb-alien:define-alien-routine >+ ("bdd___bdd_create_var_after" bdd_create_var_after) >+ (* t) >+ (v (* t))) >+ >+;;; BDDPTR bdd_create_var_last (void) >+(sb-alien:define-alien-routine >+ ("bdd___bdd_create_var_last" bdd_create_var_last) >+ (* t)) >+ >+;;; void bdd_print (FILE *fp, BDDPTR f, char *s) >+(sb-alien:define-alien-routine ("bdd___bdd_print" bdd_print) >+ sb-alien:void >+ (fp (* t)) >+ (f (* t)) >+ (s sb-alien:c-string)) >+ >+;;; void bdd_print_stats (FILE *fp) >+;;; void bdd_quit (void) >+(sb-alien:define-alien-routine ("bdd___bdd_quit" bdd_quit) >+ sb-alien:void) >+ >+;;; int bdd_memsize (void) >+;;; int bdd_memsize_limit (void) >+;;; void bdd_set_memsize_limit_and_handler (int limit, void (*handler) (void)) >+;;; int bdd_nodes_alive (void) >+(sb-alien:define-alien-routine ("bdd___bdd_nodes_alive" bdd_nodes_alive) >+ (integer 32)) >+ >+;;; int bdd_nodes_allocated (void) >+(sb-alien:define-alien-routine >+ ("bdd___bdd_nodes_allocated" bdd_nodes_allocated) >+ (integer 32)) >+ >+;;; int bdd_nr_occurs_var (int id) >+;;; int bdd_compl_p (BDDPTR f, BDDPTR g) >+;;; int bdd_equal_p (BDDPTR F, BDDPTR G) >+(sb-alien:define-alien-routine ("bdd___bdd_equal_p" bdd_equal_p) >+ (integer 32) >+ (f (* t)) >+ (g (* t))) >+ >+;;; int bdd_implies_taut (BDDPTR F, BDDPTR G) >+;;; BDDPTR bdd_not (BDDPTR F) >+(sb-alien:define-alien-routine ("bdd___bdd_not" bdd_not) >+ (* t) >+ (f (* t))) >+ >+;;; BDDPTR bdd_and (BDDPTR F, BDDPTR G) >+(sb-alien:define-alien-routine ("bdd___bdd_and" bdd_and) >+ (* t) >+ (f (* t)) >+ (g (* t))) >+ >+;;; BDDPTR bdd_greater (BDDPTR F, BDDPTR G) >+(sb-alien:define-alien-routine ("bdd___bdd_greater" bdd_greater) >+ (* t) >+ (f (* t)) >+ (g (* t))) >+ >+;;; BDDPTR bdd_less (BDDPTR F, BDDPTR G) >+(sb-alien:define-alien-routine ("bdd___bdd_less" bdd_less) >+ (* t) >+ (f (* t)) >+ (g (* t))) >+ >+;;; BDDPTR bdd_xor (BDDPTR F, BDDPTR G) >+(sb-alien:define-alien-routine ("bdd___bdd_xor" bdd_xor) >+ (* t) >+ (f (* t)) >+ (g (* t))) >+ >+;;; BDDPTR bdd_or (BDDPTR F, BDDPTR G) >+(sb-alien:define-alien-routine ("bdd___bdd_or" bdd_or) >+ (* t) >+ (f (* t)) >+ (g (* t))) >+ >+;;; BDDPTR bdd_nor (BDDPTR F, BDDPTR G) >+(sb-alien:define-alien-routine ("bdd___bdd_nor" bdd_nor) >+ (* t) >+ (f (* t)) >+ (g (* t))) >+ >+;;; BDDPTR bdd_equiv (BDDPTR F, BDDPTR G) >+(sb-alien:define-alien-routine ("bdd___bdd_equiv" bdd_equiv) >+ (* t) >+ (f (* t)) >+ (g (* t))) >+ >+;;; BDDPTR bdd_xnor (BDDPTR F, BDDPTR G) /* equivalent to bdd_equiv */ >+(sb-alien:define-alien-routine ("bdd___bdd_xnor" bdd_xnor) >+ (* t) >+ (f (* t)) >+ (g (* t))) >+ >+;;; BDDPTR bdd_implied (BDDPTR F, BDDPTR G) >+(sb-alien:define-alien-routine ("bdd___bdd_implied" bdd_implied) >+ (* t) >+ (f (* t)) >+ (g (* t))) >+ >+;;; BDDPTR bdd_implies (BDDPTR F, BDDPTR G) >+(sb-alien:define-alien-routine ("bdd___bdd_implies" bdd_implies) >+ (* t) >+ (f (* t)) >+ (g (* t))) >+ >+;;; BDDPTR bdd_nand (BDDPTR F, BDDPTR G) >+(sb-alien:define-alien-routine ("bdd___bdd_nand" bdd_nand) >+ (* t) >+ (f (* t)) >+ (g (* t))) >+ >+;;; BDDPTR bdd_0 (void) >+(sb-alien:define-alien-routine ("bdd___bdd_0" bdd_0) >+ (* t)) >+ >+;;; BDDPTR bdd_1 (void) >+(sb-alien:define-alien-routine ("bdd___bdd_1" bdd_1) >+ (* t)) >+ >+;;; BDDPTR bdd_X (void) >+(sb-alien:define-alien-routine ("bdd___bdd_X" bdd_X) >+ (* t)) >+ >+;;; BDDPTR bdd_assign (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_assign" bdd_assign) >+ (* t) >+ (f (* t))) >+ >+;;; 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) >+ (* t) >+ (f (* t))) >+ >+;;; BDDPTR bdd_else (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_else" bdd_else) >+ (* t) >+ (f (* t))) >+ >+;;; BDDPTR bdd_apply (BDDPTR (*f)(BDDPTR,BDDPTR),BDDPTR a,BDDPTR b) >+(sb-alien:define-alien-routine ("bdd___bdd_apply" bdd_apply) >+ (* t) >+ (f (* t)) >+ (a (* t)) >+ (b (* t))) >+ >+;;; BDDPTR bdd_constrain (BDDPTR f, BDDPTR c) >+(sb-alien:define-alien-routine ("bdd___bdd_constrain" bdd_constrain) >+ (* t) >+ (f (* t)) >+ (c (* t))) >+ >+;;; BDDPTR bdd_top_var (BDDPTR f) >+(sb-alien:define-alien-routine ("bdd___bdd_top_var" bdd_top_var) >+ (* t) >+ (f (* t))) >+ >+;;; BDD_LIST bdd_sum_of_cubes (BDDPTR f, int irredundant) >+(sb-alien:define-alien-routine ("bdd___bdd_sum_of_cubes" bdd_sum_of_cubes) >+ (* t) >+ (f (* t)) >+ (irredundant (integer 32))) >+ >+(sb-alien:define-alien-variable ("bdd_interrupted" bdd_interrupted) (integer 32)) >+ >+;;; The following were obtained by looking through mu.c and collecting >+;;; functions not mentioned above. >+ >+;;; int bdd_reorder_var (int var_id, int target_var_id) >+(sb-alien:define-alien-routine ("bdd___bdd_reorder_var" bdd_reorder_var) >+ (integer 32) >+ (var_id (integer 32)) >+ (target_var (integer 32))) >+ >+;;; BDDPTR bdd_and_smooth (BDDPTR f, BDDPTR g, BDD_LIST vars) >+(sb-alien:define-alien-routine ("bdd___bdd_and_smooth" bdd_and_smooth) >+ (* t) >+ (f (* t)) >+ (g (* t)) >+ (vars (* t))) >+ >+;;; BDD_LIST bdd_rank_order_vars (BDD_LIST vars) >+(sb-alien:define-alien-routine >+ ("bdd___bdd_rank_order_vars" bdd_rank_order_vars) >+ (* t) >+ (vars (* t))) >+ >+;;; BDDPTR bdd_quantify (int existential, BDDPTR f, BDD_LIST vars) >+(sb-alien:define-alien-routine ("bdd___bdd_quantify" bdd_quantify) >+ (* t) >+ (existential (integer 32)) >+ (f (* t)) >+ (vars (* t))) >+ >+;;; BDDPTR bdd_subst_par (BDDPTR *f_vec, BDD_LIST vars, BDDPTR g) >+(sb-alien:define-alien-routine ("bdd___bdd_subst_par" bdd_subst_par) >+ (* t) >+ (f_vec (array (* t))) >+ (vars (* t)) >+ (g (* t))) >+ >+;;; BDDPTR bdd_subst_par_list (BDD_LIST f_list, BDD_LIST vars, BDDPTR g) >+(sb-alien:define-alien-routine ("bdd___bdd_subst_par_list" bdd_subst_par_list) >+ (* t) >+ (f_list (* t)) >+ (vars (* t)) >+ (g (* t))) >+ >+;;; void bdd_free_vec (BDDPTR *f_vec, int size) >+(sb-alien:define-alien-routine ("bdd___bdd_free_vec" bdd_free_vec) >+ sb-alien:void >+ (f_vec (array (* t))) >+ (size (integer 32))) >+ >+;;; const char *bdd_get_output_string (int idx) >+(sb-alien:define-alien-routine >+ ("bdd___bdd_get_output_string" bdd_get_output_string) >+ sb-alien:c-string >+ (idx (integer 32))) >+ >+;;; void bdd_set_output_string (int idx, const char *str) >+(sb-alien:define-alien-routine >+ ("bdd___bdd_set_output_string" bdd_set_output_string) >+ sb-alien:void >+ (idx (integer 32)) >+ (str sb-alien:c-string)) >+ >+;;; void bdd_print_as_sum_of_cubes (FILE *fp, BDDPTR f, int irredundant) >+(sb-alien:define-alien-routine >+ ("bdd___bdd_print_as_sum_of_cubes" bdd_print_as_sum_of_cubes) >+ sb-alien:void >+ (fp (* t)) >+ (f (* t)) >+ (irredundant (integer 32))) >+ >+;;; BDDPTR bdd_diff (BDDPTR f, BDD_LIST vars) >+(sb-alien:define-alien-routine ("bdd___bdd_diff" bdd_diff) >+ (* t) >+ (f (* t)) >+ (vars (* t))) >+ >+;;; BDDPTR bdd_one_of_vec (BDDPTR *vec, int size) >+(sb-alien:define-alien-routine ("bdd___bdd_one_of_vec" bdd_one_of_vec) >+ (* t) >+ (vec (array (* t))) >+ (size (integer 32))) >+ >+;;; BDDPTR bdd_none_of_vec (BDDPTR *args, int size) >+(sb-alien:define-alien-routine ("bdd___bdd_none_of_vec" bdd_none_of_vec) >+ (* t) >+ (args (array (* t))) >+ (size (integer 32))) >+ >+;;; BDDPTR bdd_subst (BDDPTR f, int var, BDDPTR g) >+(sb-alien:define-alien-routine ("bdd___bdd_subst" bdd_subst) >+ (* t) >+ (f (* t)) >+ (var (integer 32)) >+ (g (* t))) >+ >+;;; BDD_LIST bdd_sum_of_cubes_as_list (BDDPTR f) >+(sb-alien:define-alien-routine >+ ("bdd___bdd_sum_of_cubes_as_list" bdd_sum_of_cubes_as_list) >+ (* t) >+ (f (* t))) >+ >+;;; int bdd_traverse_cube (BDDPTR cube, >+;;; void (*action) (int index, int neg, int first)) >+(sb-alien:define-alien-routine ("bdd___bdd_traverse_cube" bdd_traverse_cube) >+ (integer 32) >+ (cube (* t)) >+ (action (* t))) >+ >+;;; BDD_LIST bdd_support_as_list_of_vars (BDDPTR f) >+(sb-alien:define-alien-routine >+ ("bdd___bdd_support_as_list_of_vars" bdd_support_as_list_of_vars) >+ (* t) >+ (f (* t))) >+ >+(defun bdd-interrupted? () >+ (not (zerop 'bdd_interrupted))) >+ >+(bdd_init) >diff -Naur pvs4.2-orig/BDD/bdd_table.c pvs4.2-sbcl/BDD/bdd_table.c >--- pvs4.2-orig/BDD/bdd_table.c 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/BDD/bdd_table.c 2009-03-24 18:56:17.000000000 +0000 >@@ -8,6 +8,8 @@ > > int bdd___bdd_equal_p (BDDPTR F, BDDPTR G) {return bdd_equal_p (F, G);} > >+int bdd___null_list_p (LIST x) {return null_list_p (x);} >+ > void bdd___elem_contents (LIST_ELEM_PTR x) {elem_contents (x);} > > LIST_ELEM_PTR bdd___list_first (LIST x) { >diff -Naur pvs4.2-orig/BDD/ix86_64-Linux/Makefile pvs4.2-sbcl/BDD/ix86_64-Linux/Makefile >--- pvs4.2-orig/BDD/ix86_64-Linux/Makefile 1970-01-01 00:00:00.000000000 +0000 >+++ pvs4.2-sbcl/BDD/ix86_64-Linux/Makefile 2009-03-24 18:56:17.000000000 +0000 >@@ -0,0 +1,48 @@ >+BDD = ../bdd/src >+MU = ../mu/src >+UTILS = ../bdd/utils >+INCLUDES = -I/usr/include -I$(BDD) -I$(UTILS) -I$(MU) >+LD = ld >+LDFLAGS = -Bsymbolic -shared -warn-once -L./ >+CC = gcc >+CFLAGS = -D_POSIX_SOURCE -DSYSV $(INCLUDES) -DLINUX -DLINUX_REDHAT5 -DSIGNALS_LINUX -fPIC >+XCFLAGS = -O >+SHELL = /bin/sh >+VPATH = ..:../bdd/utils:../bdd/src:../mu/src >+ >+muobj = bdd_interface.o bdd.o bdd_factor.o bdd_quant.o bdd_fns.o bdd_vfns.o \ >+ appl.o mu_interface.o mu.o >+ >+utilobj = double.o list.o hash.o alloc.o >+ >+.SUFFIXES: >+.SUFFIXES: .c .o >+.c.o : ; $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@ >+ >+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 >+ >+libutils.a : ${utilobj} >+ ar r libutils.a ${utilobj} >+ ranlib libutils.a >+ >+bdd_interface.o : bdd_interface.c bdd_fns.h >+bdd_factor.o : bdd_factor.c bdd_factor.h >+bdd.o : bdd.c bdd.h bdd_extern.h >+bdd_fns.o : bdd_fns.c bdd_fns.h bdd.h bdd_extern.h >+bdd_quant.o : bdd_quant.c bdd_fns.h bdd.h bdd_extern.h >+bdd_vfns.o : bdd_vfns.c bdd_vfns.h bdd_fns.h bdd.h bdd_extern.h >+ >+mu_interface.o : mu_interface.c mu.h >+mu.o : mu.c mu.h >+ >+double.o : double.c double.h >+list.o : list.c list.h alloc.h >+hash.o : hash.c hash.h alloc.h >+alloc.o : alloc.c >+ >+clean : >+ rm -f *.o *.a *.so >+ >diff -Naur pvs4.2-orig/BDD/mu-sbcl.lisp pvs4.2-sbcl/BDD/mu-sbcl.lisp >--- pvs4.2-orig/BDD/mu-sbcl.lisp 1970-01-01 00:00:00.000000000 +0000 >+++ pvs4.2-sbcl/BDD/mu-sbcl.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -0,0 +1,248 @@ >+;; -------------------------------------------------------------------- >+;; 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) >+ >+ >+;;;;;;;;;;;;;;;;; >+;;; Formula ;;; >+;;;;;;;;;;;;;;;;; >+ >+;;; Formula mu_mk_false_formula (void) >+(sb-alien:define-alien-routine ("mu___mu_mk_false_formula" mu_mk_false_formula) >+ (* t)) >+ >+;;; Formula mu_mk_true_formula (void) >+(sb-alien:define-alien-routine ("mu___mu_mk_true_formula" mu_mk_true_formula) >+ (* t)) >+ >+;;; Formula mu_mk_bool_var (char *name) >+(sb-alien:define-alien-routine ("mu___mu_mk_bool_var" mu_mk_bool_var) >+ (* t) >+ (name sb-alien:c-string)) >+ >+;;; int mu_check_bool_var (char *name) >+(sb-alien:define-alien-routine ("mu___mu_check_bool_var" mu_check_bool_var) >+ (integer 32) >+ (var sb-alien:c-string)) >+ >+;;; Formula mu_check_mk_bool_var (char *name) >+(sb-alien:define-alien-routine >+ ("mu___mu_check_mk_bool_var" mu_check_mk_bool_var) >+ (* t) >+ (name sb-alien:c-string)) >+ >+;;; Formula mu_mk_ite_formula (Formula cond, Formula then_part, Formula else_part) >+(sb-alien:define-alien-routine ("mu___mu_mk_ite_formula" mu_mk_ite_formula) >+ (* t) >+ (cnd (* t)) >+ (then_part (* t)) >+ (else_part (* t))) >+ >+;;; Formula mu_mk_curry_application (Term R, LIST subs) >+(sb-alien:define-alien-routine >+ ("mu___mu_mk_curry_application" mu_mk_curry_application) >+ (* t) >+ (R (* t)) >+ (subs (* t))) >+ >+;;; Formula mu_mk_application (Term R, LIST subs, int curried) >+(sb-alien:define-alien-routine ("mu___mu_mk_application" mu_mk_application) >+ (* t) >+ (R (* t)) >+ (subs (* t)) >+ (curried (integer 32))) >+ >+;;; Formula mu_mk_forall (LIST listvars, Formula fml) >+(sb-alien:define-alien-routine ("mu___mu_mk_forall" mu_mk_forall) >+ (* t) >+ (listvars (* t)) >+ (fml (* t))) >+ >+;;; Formula mu_mk_exists (LIST listvars, Formula fml) >+(sb-alien:define-alien-routine ("mu___mu_mk_exists" mu_mk_exists) >+ (* t) >+ (listvars (* t)) >+ (fml (* t))) >+ >+;;; Formula mu_mk_implies_formula (Formula fml1, Formula fml2) >+(sb-alien:define-alien-routine >+ ("mu___mu_mk_implies_formula" mu_mk_implies_formula) >+ (* t) >+ (fml1 (* t)) >+ (fml2 (* t))) >+ >+;;; Formula mu_mk_equiv_formula (Formula fml1, Formula fml2) >+(sb-alien:define-alien-routine ("mu___mu_mk_equiv_formula" mu_mk_equiv_formula) >+ (* t) >+ (fml1 (* t)) >+ (fml2 (* t))) >+ >+;;; Formula mu_mk_or_formula (Formula fml1, Formula fml2) >+(sb-alien:define-alien-routine ("mu___mu_mk_or_formula" mu_mk_or_formula) >+ (* t) >+ (fml1 (* t)) >+ (fml2 (* t))) >+ >+;;; Formula mu_mk_and_formula (Formula fml1, Formula fml2) >+(sb-alien:define-alien-routine ("mu___mu_mk_and_formula" mu_mk_and_formula) >+ (* t) >+ (fml1 (* t)) >+ (fml2 (* t))) >+ >+;;; Formula mu_mk_not_formula (Formula fml) >+(sb-alien:define-alien-routine ("mu___mu_mk_not_formula" mu_mk_not_formula) >+ (* t) >+ (fml (* t))) >+ >+;;; Formula mu_mk_cofactor (Formula fml1, Formula fml2) >+(sb-alien:define-alien-routine ("mu___mu_mk_cofactor" mu_mk_cofactor) >+ (* t) >+ (fml1 (* t)) >+ (fml2 (* t))) >+ >+;;;;;;;;;;;;;;; >+;;; Term ;;; >+;;;;;;;;;;;;;;; >+;;; Term mu_mk_abstraction (LIST vars, Formula f1) >+(sb-alien:define-alien-routine ("mu___mu_mk_abstraction" mu_mk_abstraction) >+ (* t) >+ (vars (* t)) >+ (f1 (* t))) >+;;; Term mu_mk_l_fixed_point (int relvar, Term fml1) >+(sb-alien:define-alien-routine ("mu___mu_mk_l_fixed_point" mu_mk_l_fixed_point) >+ (* t) >+ (relvar (integer 32)) >+ (fml1 (* t))) >+;;; Term mu_mk_g_fixed_point (int relvar, Term fml1) >+(sb-alien:define-alien-routine ("mu___mu_mk_g_fixed_point" mu_mk_g_fixed_point) >+ (* t) >+ (relvar (integer 32)) >+ (fml1 (* t))) >+;;; Term mu_mk_reach (Term Next, Term S0, Term Inv) >+(sb-alien:define-alien-routine ("mu___mu_mk_reach" mu_mk_reach) >+ (* t) >+ (Next (* t)) >+ (S0 (* t)) >+ (Inv (* t))) >+;;; Term mu_mk_rel_var_dcl (char *name) >+(sb-alien:define-alien-routine ("mu___mu_mk_rel_var_dcl" mu_mk_rel_var_dcl) >+ (* t) >+ (name sb-alien:c-string)) >+;;; Term mu_mk_rel_var_ (char *name) >+(sb-alien:define-alien-routine ("mu___mu_mk_rel_var_" mu_mk_rel_var_) >+ (* t) >+ (name sb-alien:c-string)) >+;;; Term mu_mk_true_term (void) >+(sb-alien:define-alien-routine ("mu___mu_mk_true_term" mu_mk_true_term) >+ (* t)) >+;;; Term mu_mk_false_term (void) >+(sb-alien:define-alien-routine ("mu___mu_mk_false_term" mu_mk_false_term) >+ (* t)) >+;;; Term mu_mk_not_term (Term fml1) >+(sb-alien:define-alien-routine ("mu___mu_mk_not_term" mu_mk_not_term) >+ (* t) >+ (fml1 (* t))) >+;;; Term mu_mk_and_term (Term fml1, Term fml2) >+(sb-alien:define-alien-routine ("mu___mu_mk_and_term" mu_mk_and_term) >+ (* t) >+ (fml1 (* t)) >+ (fml2 (* t))) >+;;; Term mu_mk_or_term (Term fml1, Term fml2) >+(sb-alien:define-alien-routine ("mu___mu_mk_or_term" mu_mk_or_term) >+ (* t) >+ (fml1 (* t)) >+ (fml2 (* t))) >+;;; Term mu_mk_equiv_term (Term fml1, Term fml2) >+(sb-alien:define-alien-routine ("mu___mu_mk_equiv_term" mu_mk_equiv_term) >+ (* t) >+ (fml1 (* t)) >+ (fml2 (* t))) >+;;; Term mu_mk_implies_term (Term fml1, Term fml2) >+(sb-alien:define-alien-routine ("mu___mu_mk_implies_term" mu_mk_implies_term) >+ (* t) >+ (fml1 (* t)) >+ (fml2 (* t))) >+;;; const char *get_mu_bool_var_name (int bdd_idx) >+(sb-alien:define-alien-routine >+ ("mu___get_mu_bool_var_name" get_mu_bool_var_name) >+ sb-alien:c-string >+ (bdd_idx (integer 32))) >+ >+;;;;;;;;;;;;;;;;;;; >+;;; Lists ;;; >+;;;;;;;;;;;;;;;;;;; >+ >+;;; LIST append_cont (void *p, LIST list) >+(sb-alien:define-alien-routine ("mu___append_cont" append_cont) >+ (* t) >+ (p (* t)) >+ (list (* t))) >+;;; LIST empty_list (void) >+(sb-alien:define-alien-routine ("mu___empty_list" empty_list) >+ (* t)) >+ >+;;; >+;;; Flags >+ >+;;; int set_mu_warnings (int flag) >+(sb-alien:define-alien-routine ("mu___set_mu_warnings" set_mu_warnings) >+ (integer 32) >+ (flag (integer 32))) >+;;; int set_mu_simplify_frontier (int flag) >+(sb-alien:define-alien-routine >+ ("mu___set_mu_simplify_frontier" set_mu_simplify_frontier) >+ (integer 32) >+ (flag (integer 32))) >+;;; int set_mu_verbose (int flag) >+(sb-alien:define-alien-routine ("mu___set_mu_verbose" set_mu_verbose) >+ (integer 32) >+ (flag (integer 32))) >+ >+;; >+;; >+;; GC management: not needed, "modelcheck_formula" takes care of it. >+;; >+ >+;;;;;;;;;;;;;;;;;;; >+;;; print ;;; >+;;;;;;;;;;;;;;;;;;; >+ >+;;; void pvs_mu_print_formula (Formula fml) >+(sb-alien:define-alien-routine >+ ("mu___pvs_mu_print_formula" pvs_mu_print_formula) >+ sb-alien:void >+ (fml (* t))) >+;;; void pvs_mu_print_term (Term t) >+(sb-alien:define-alien-routine ("mu___pvs_mu_print_term" pvs_mu_print_term) >+ sb-alien:void >+ (term (* t))) >+ >+;;;;;;;;;;;;;;;;;;;;;;;;; >+;;; Main function ;;;;; >+;;;;;;;;;;;;;;;;;;;;;;;;; >+ >+;;; void mu_init (void) >+(sb-alien:define-alien-routine ("mu___mu_init" mu_init) >+ sb-alien:void) >+(sb-alien:define-alien-routine ("mu___mu_quit" mu_quit) >+ sb-alien:void) >+;;; BDDPTR mu___modelcheck_formula (Formula fml) >+(sb-alien:define-alien-routine ("mu___modelcheck_formula" modelcheck_formula) >+ (* t) >+ (fml (* t))) >diff -Naur pvs4.2-orig/bin/make-dist pvs4.2-sbcl/bin/make-dist >--- pvs4.2-orig/bin/make-dist 2008-07-19 21:49:18.000000000 +0000 >+++ pvs4.2-sbcl/bin/make-dist 2009-03-24 18:56:17.000000000 +0000 >@@ -91,16 +91,18 @@ > src/groundeval/*.lisp \ > src/utils/*.lisp \ > src/utils/ix86-Linux/Makefile src/utils/ix86-MacOSX/Makefile \ >+ src/utils/ix86_64-Linux/Makefile \ > src/utils/powerpc-MacOSX/Makefile \ > src/utils/sun4-SunOS5/Makefile \ > BDD/bdd-ld-table BDD/mu-ld-table \ > BDD/*.c \ > BDD/*.lisp \ >- BDD/ix86-Linux/Makefile BDD/sun4-SunOS5/Makefile \ >+ BDD/ix86-Linux/Makefile BDD/ix86_64-Linux/Makefile BDD/sun4-SunOS5/Makefile \ > BDD/ix86-MacOSX/Makefile BDD/powerpc-MacOSX/Makefile \ > BDD/bdd BDD/mu \ > src/WS1S/README src/WS1S/ws1s-ld-table \ > src/WS1S/*.c src/WS1S/mona-1.4 \ >+ src/WS1S/ix86_64-Linux/Makefile > src/WS1S/ix86-Linux/Makefile src/WS1S/sun4-SunOS5/Makefile \ > src/WS1S/ix86-MacOSX/Makefile src/WS1S/powerpc-MacOSX/Makefile \ > doc/pvs.bib doc/makebnf.sty doc/pvstex.tex doc/release-notes \ >@@ -155,7 +157,7 @@ > # echo "pvs-libraries.tgz not created - need to typecheck finite_sets and bitvectors" > # fi > >-for platform in ix86-Linux ix86-MacOSX powerpc-MacOSX \ >+for platform in ix86-Linux ix86_64-Linux ix86-MacOSX powerpc-MacOSX \ > sun4-SunOS5 > do > for subdir in runtime devel >@@ -199,5 +201,22 @@ > else > echo "CMU Lisp ${subdir} not available for ${platform}" > fi >+ if [ -e bin/${platform}/${subdir}/pvs-sbclisp -a "$subdir" = "runtime" ] >+ then >+ echo Creating pvs-${version}-${platform}-sbclisp${kind}.tgz >+ tar ${TARFLAGS} -f pvs-${version}-${platform}-sbclisp${kind}.tgz \ >+ ${pvssystemfiles} \ >+ bin/${platform}/b64 bin/relocate \ >+ bin/pvs-platform bin/tar-b64-mail \ >+ bin/${platform}/${subdir}/mu.* \ >+ bin/${platform}/${subdir}/file_utils.* \ >+ bin/${platform}/${subdir}/ws1s.* \ >+ bin/${platform}/${subdir}/*-sbcl.* \ >+ bin/${platform}/${subdir}/lisp \ >+ bin/${platform}/${subdir}/pvs-sbclisp* >+ ls -l pvs-${version}-${platform}-sbclisp${kind}.tgz >+ else >+ echo "SBCL ${subdir} not available for ${platform}" >+ fi > done > done >diff -Naur pvs4.2-orig/bin/pvs-platform pvs4.2-sbcl/bin/pvs-platform >--- pvs4.2-orig/bin/pvs-platform 2007-07-16 06:28:06.000000000 +0000 >+++ pvs4.2-sbcl/bin/pvs-platform 2009-03-24 18:56:17.000000000 +0000 >@@ -33,7 +33,11 @@ > esac > os=SunOS > os_version=`uname -r | cut -d"." -f1`;; >- Linux) arch=ix86 >+ Linux) case `uname -m` in >+ x86_64) arch=ix86_64;; >+ i*86) arch=ix86;; >+ x86*) arch=ix86;; >+ esac > os=Linux;; > AIX) arch=powerpc-ibm > os=AIX >diff -Naur pvs4.2-orig/config.guess pvs4.2-sbcl/config.guess >--- pvs4.2-orig/config.guess 2007-07-02 20:07:43.000000000 +0000 >+++ pvs4.2-sbcl/config.guess 2009-03-24 18:56:17.000000000 +0000 >@@ -1,9 +1,10 @@ > #! /bin/sh > # Attempt to guess a canonical system name. > # Copyright (C) 1992, 1993, 1994, 1995, 1996, 1997, 1998, 1999, >-# 2000, 2001, 2002, 2003 Free Software Foundation, Inc. >+# 2000, 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008 >+# Free Software Foundation, Inc. > >-timestamp='2003-06-17' >+timestamp='2008-12-19' > > # This file is free software; you can redistribute it and/or modify it > # under the terms of the GNU General Public License as published by >@@ -17,13 +18,15 @@ > # > # 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. >+# Foundation, Inc., 51 Franklin Street - Fifth Floor, Boston, MA >+# 02110-1301, USA. > # > # As a special exception to the GNU General Public License, if you > # distribute this file as part of a program that contains a > # configuration script generated by Autoconf, you may include it under > # the same distribution terms that you use for the rest of that program. > >+ > # Originally written by Per Bothner <per@bothner.com>. > # Please send patches to <config-patches@gnu.org>. Submit a context > # diff and a properly formatted ChangeLog entry. >@@ -53,8 +56,8 @@ > GNU config.guess ($timestamp) > > Originally written by Per Bothner. >-Copyright (C) 1992, 1993, 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001 >-Free Software Foundation, Inc. >+Copyright (C) 1992, 1993, 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, >+2002, 2003, 2004, 2005, 2006, 2007, 2008 Free Software Foundation, Inc. > > This is free software; see the source for copying conditions. There is NO > warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE." >@@ -66,11 +69,11 @@ > while test $# -gt 0 ; do > case $1 in > --time-stamp | --time* | -t ) >- echo "$timestamp" ; exit 0 ;; >+ echo "$timestamp" ; exit ;; > --version | -v ) >- echo "$version" ; exit 0 ;; >+ echo "$version" ; exit ;; > --help | --h* | -h ) >- echo "$usage"; exit 0 ;; >+ echo "$usage"; exit ;; > -- ) # Stop option processing > shift; break ;; > - ) # Use stdin as input. >@@ -104,7 +107,7 @@ > trap "exitcode=\$?; (rm -f \$tmpfiles 2>/dev/null; rmdir \$tmp 2>/dev/null) && exit \$exitcode" 0 ; > trap "rm -f \$tmpfiles 2>/dev/null; rmdir \$tmp 2>/dev/null; exit 1" 1 2 13 15 ; > : ${TMPDIR=/tmp} ; >- { tmp=`(umask 077 && mktemp -d -q "$TMPDIR/cgXXXXXX") 2>/dev/null` && test -n "$tmp" && test -d "$tmp" ; } || >+ { tmp=`(umask 077 && mktemp -d "$TMPDIR/cgXXXXXX") 2>/dev/null` && test -n "$tmp" && test -d "$tmp" ; } || > { test -n "$RANDOM" && tmp=$TMPDIR/cg$$-$RANDOM && (umask 077 && mkdir $tmp) ; } || > { tmp=$TMPDIR/cg-$$ && (umask 077 && mkdir $tmp) && echo "Warning: creating insecure temp directory" >&2 ; } || > { echo "$me: cannot create a temporary directory in $TMPDIR" >&2 ; exit 1 ; } ; >@@ -123,7 +126,7 @@ > ;; > ,,*) CC_FOR_BUILD=$CC ;; > ,*,*) CC_FOR_BUILD=$HOST_CC ;; >-esac ;' >+esac ; set_cc_for_build= ;' > > # This is needed to find uname on a Pyramid OSx when run in the BSD universe. > # (ghazi@noc.rutgers.edu 1994-08-24) >@@ -136,13 +139,6 @@ > UNAME_SYSTEM=`(uname -s) 2>/dev/null` || UNAME_SYSTEM=unknown > UNAME_VERSION=`(uname -v) 2>/dev/null` || UNAME_VERSION=unknown > >-## for Red Hat Linux >-if test -f /etc/redhat-release ; then >- VENDOR=redhat ; >-else >- VENDOR= ; >-fi >- > # Note: order is significant - the case branches are not exclusive. > > case "${UNAME_MACHINE}:${UNAME_SYSTEM}:${UNAME_RELEASE}:${UNAME_VERSION}" in >@@ -165,6 +161,7 @@ > arm*) machine=arm-unknown ;; > sh3el) machine=shl-unknown ;; > sh3eb) machine=sh-unknown ;; >+ sh5el) machine=sh5le-unknown ;; > *) machine=${UNAME_MACHINE_ARCH}-unknown ;; > esac > # The Operating System including object format, if it has switched >@@ -203,50 +200,32 @@ > # contains redundant information, the shorter form: > # CPU_TYPE-MANUFACTURER-OPERATING_SYSTEM is used. > echo "${machine}-${os}${release}" >- exit 0 ;; >- amiga:OpenBSD:*:*) >- echo m68k-unknown-openbsd${UNAME_RELEASE} >- exit 0 ;; >- arc:OpenBSD:*:*) >- echo mipsel-unknown-openbsd${UNAME_RELEASE} >- exit 0 ;; >- hp300:OpenBSD:*:*) >- echo m68k-unknown-openbsd${UNAME_RELEASE} >- exit 0 ;; >- mac68k:OpenBSD:*:*) >- echo m68k-unknown-openbsd${UNAME_RELEASE} >- exit 0 ;; >- macppc:OpenBSD:*:*) >- echo powerpc-unknown-openbsd${UNAME_RELEASE} >- exit 0 ;; >- mvme68k:OpenBSD:*:*) >- echo m68k-unknown-openbsd${UNAME_RELEASE} >- exit 0 ;; >- mvme88k:OpenBSD:*:*) >- echo m88k-unknown-openbsd${UNAME_RELEASE} >- exit 0 ;; >- mvmeppc:OpenBSD:*:*) >- echo powerpc-unknown-openbsd${UNAME_RELEASE} >- exit 0 ;; >- pmax:OpenBSD:*:*) >- echo mipsel-unknown-openbsd${UNAME_RELEASE} >- exit 0 ;; >- sgi:OpenBSD:*:*) >- echo mipseb-unknown-openbsd${UNAME_RELEASE} >- exit 0 ;; >- sun3:OpenBSD:*:*) >- echo m68k-unknown-openbsd${UNAME_RELEASE} >- exit 0 ;; >- wgrisc:OpenBSD:*:*) >- echo mipsel-unknown-openbsd${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > *:OpenBSD:*:*) >- echo ${UNAME_MACHINE}-unknown-openbsd${UNAME_RELEASE} >- exit 0 ;; >+ UNAME_MACHINE_ARCH=`arch | sed 's/OpenBSD.//'` >+ echo ${UNAME_MACHINE_ARCH}-unknown-openbsd${UNAME_RELEASE} >+ exit ;; >+ *:ekkoBSD:*:*) >+ echo ${UNAME_MACHINE}-unknown-ekkobsd${UNAME_RELEASE} >+ exit ;; >+ *:SolidBSD:*:*) >+ echo ${UNAME_MACHINE}-unknown-solidbsd${UNAME_RELEASE} >+ exit ;; >+ macppc:MirBSD:*:*) >+ echo powerpc-unknown-mirbsd${UNAME_RELEASE} >+ exit ;; >+ *:MirBSD:*:*) >+ echo ${UNAME_MACHINE}-unknown-mirbsd${UNAME_RELEASE} >+ exit ;; > alpha:OSF1:*:*) >- if test $UNAME_RELEASE = "V4.0"; then >+ case $UNAME_RELEASE in >+ *4.0) > UNAME_RELEASE=`/usr/sbin/sizer -v | awk '{print $3}'` >- fi >+ ;; >+ *5.*) >+ UNAME_RELEASE=`/usr/sbin/sizer -v | awk '{print $4}'` >+ ;; >+ esac > # According to Compaq, /usr/sbin/psrinfo has been available on > # OSF/1 and Tru64 systems produced since 1995. I hope that > # covers most systems running today. This code pipes the CPU >@@ -284,42 +263,49 @@ > "EV7.9 (21364A)") > UNAME_MACHINE="alphaev79" ;; > esac >+ # A Pn.n version is a patched version. > # A Vn.n version is a released version. > # A Tn.n version is a released field test version. > # A Xn.n version is an unreleased experimental baselevel. > # 1.2 uses "1.2" for uname -r. >- echo ${UNAME_MACHINE}-dec-osf`echo ${UNAME_RELEASE} | sed -e 's/^[VTX]//' | tr 'ABCDEFGHIJKLMNOPQRSTUVWXYZ' 'abcdefghijklmnopqrstuvwxyz'` >- exit 0 ;; >- Alpha*:OpenVMS:*:*) >- echo alpha-hp-vms >- exit 0 ;; >+ echo ${UNAME_MACHINE}-dec-osf`echo ${UNAME_RELEASE} | sed -e 's/^[PVTX]//' | tr 'ABCDEFGHIJKLMNOPQRSTUVWXYZ' 'abcdefghijklmnopqrstuvwxyz'` >+ exit ;; > Alpha\ *:Windows_NT*:*) > # How do we know it's Interix rather than the generic POSIX subsystem? > # Should we change UNAME_MACHINE based on the output of uname instead > # of the specific Alpha model? > echo alpha-pc-interix >- exit 0 ;; >+ exit ;; > 21064:Windows_NT:50:3) > echo alpha-dec-winnt3.5 >- exit 0 ;; >+ exit ;; > Amiga*:UNIX_System_V:4.0:*) > echo m68k-unknown-sysv4 >- exit 0;; >+ exit ;; > *:[Aa]miga[Oo][Ss]:*:*) > echo ${UNAME_MACHINE}-unknown-amigaos >- exit 0 ;; >+ exit ;; > *:[Mm]orph[Oo][Ss]:*:*) > echo ${UNAME_MACHINE}-unknown-morphos >- exit 0 ;; >+ exit ;; > *:OS/390:*:*) > echo i370-ibm-openedition >- exit 0 ;; >+ exit ;; >+ *:z/VM:*:*) >+ echo s390-ibm-zvmoe >+ exit ;; >+ *:OS400:*:*) >+ echo powerpc-ibm-os400 >+ exit ;; > arm:RISC*:1.[012]*:*|arm:riscix:1.[012]*:*) > echo arm-acorn-riscix${UNAME_RELEASE} >- exit 0;; >+ exit ;; >+ arm:riscos:*:*|arm:RISCOS:*:*) >+ echo arm-unknown-riscos >+ exit ;; > SR2?01:HI-UX/MPP:*:* | SR8000:HI-UX/MPP:*:*) > echo hppa1.1-hitachi-hiuxmpp >- exit 0;; >+ exit ;; > Pyramid*:OSx*:*:* | MIS*:OSx*:*:* | MIS*:SMP_DC-OSx*:*:*) > # akee@wpdis03.wpafb.af.mil (Earle F. Ake) contributed MIS and NILE. > if test "`(/bin/universe) 2>/dev/null`" = att ; then >@@ -327,32 +313,45 @@ > else > echo pyramid-pyramid-bsd > fi >- exit 0 ;; >+ exit ;; > NILE*:*:*:dcosx) > echo pyramid-pyramid-svr4 >- exit 0 ;; >+ exit ;; > DRS?6000:unix:4.0:6*) > echo sparc-icl-nx6 >- exit 0 ;; >- DRS?6000:UNIX_SV:4.2*:7*) >+ exit ;; >+ DRS?6000:UNIX_SV:4.2*:7* | DRS?6000:isis:4.2*:7*) > case `/usr/bin/uname -p` in >- sparc) echo sparc-icl-nx7 && exit 0 ;; >+ sparc) echo sparc-icl-nx7; exit ;; > esac ;; > sun4H:SunOS:5.*:*) > echo sparc-hal-solaris2`echo ${UNAME_RELEASE}|sed -e 's/[^.]*//'` >- exit 0 ;; >+ exit ;; > sun4*:SunOS:5.*:* | tadpole*:SunOS:5.*:*) > echo sparc-sun-solaris2`echo ${UNAME_RELEASE}|sed -e 's/[^.]*//'` >- exit 0 ;; >- i86pc:SunOS:5.*:*) >- echo i386-pc-solaris2`echo ${UNAME_RELEASE}|sed -e 's/[^.]*//'` >- exit 0 ;; >+ exit ;; >+ i86pc:SunOS:5.*:* | i86xen:SunOS:5.*:*) >+ eval $set_cc_for_build >+ SUN_ARCH="i386" >+ # If there is a compiler, see if it is configured for 64-bit objects. >+ # Note that the Sun cc does not turn __LP64__ into 1 like gcc does. >+ # This test works for both compilers. >+ if [ "$CC_FOR_BUILD" != 'no_compiler_found' ]; then >+ if (echo '#ifdef __amd64'; echo IS_64BIT_ARCH; echo '#endif') | \ >+ (CCOPTS= $CC_FOR_BUILD -E - 2>/dev/null) | \ >+ grep IS_64BIT_ARCH >/dev/null >+ then >+ SUN_ARCH="x86_64" >+ fi >+ fi >+ echo ${SUN_ARCH}-pc-solaris2`echo ${UNAME_RELEASE}|sed -e 's/[^.]*//'` >+ exit ;; > sun4*:SunOS:6*:*) > # According to config.sub, this is the proper way to canonicalize > # SunOS6. Hard to guess exactly what SunOS6 will be like, but > # it's likely to be more like Solaris than SunOS4. > echo sparc-sun-solaris3`echo ${UNAME_RELEASE}|sed -e 's/[^.]*//'` >- exit 0 ;; >+ exit ;; > sun4*:SunOS:*:*) > case "`/usr/bin/arch -k`" in > Series*|S4*) >@@ -361,10 +360,10 @@ > esac > # Japanese Language versions have a version number like `4.1.3-JL'. > echo sparc-sun-sunos`echo ${UNAME_RELEASE}|sed -e 's/-/_/'` >- exit 0 ;; >+ exit ;; > sun3*:SunOS:*:*) > echo m68k-sun-sunos${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > sun*:*:4.2BSD:*) > UNAME_RELEASE=`(sed 1q /etc/motd | awk '{print substr($5,1,3)}') 2>/dev/null` > test "x${UNAME_RELEASE}" = "x" && UNAME_RELEASE=3 >@@ -376,10 +375,10 @@ > echo sparc-sun-sunos${UNAME_RELEASE} > ;; > esac >- exit 0 ;; >+ exit ;; > aushp:SunOS:*:*) > echo sparc-auspex-sunos${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > # The situation for MiNT is a little confusing. The machine name > # can be virtually everything (everything which is not > # "atarist" or "atariste" at least should have a processor >@@ -390,37 +389,40 @@ > # be no problem. > atarist[e]:*MiNT:*:* | atarist[e]:*mint:*:* | atarist[e]:*TOS:*:*) > echo m68k-atari-mint${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > atari*:*MiNT:*:* | atari*:*mint:*:* | atarist[e]:*TOS:*:*) > echo m68k-atari-mint${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > *falcon*:*MiNT:*:* | *falcon*:*mint:*:* | *falcon*:*TOS:*:*) > echo m68k-atari-mint${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > milan*:*MiNT:*:* | milan*:*mint:*:* | *milan*:*TOS:*:*) > echo m68k-milan-mint${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > hades*:*MiNT:*:* | hades*:*mint:*:* | *hades*:*TOS:*:*) > echo m68k-hades-mint${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > *:*MiNT:*:* | *:*mint:*:* | *:*TOS:*:*) > echo m68k-unknown-mint${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; >+ m68k:machten:*:*) >+ echo m68k-apple-machten${UNAME_RELEASE} >+ exit ;; > powerpc:machten:*:*) > echo powerpc-apple-machten${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > RISC*:Mach:*:*) > echo mips-dec-mach_bsd4.3 >- exit 0 ;; >+ exit ;; > RISC*:ULTRIX:*:*) > echo mips-dec-ultrix${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > VAX*:ULTRIX*:*:*) > echo vax-dec-ultrix${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > 2020:CLIX:*:* | 2430:CLIX:*:*) > echo clipper-intergraph-clix${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > mips:*:*:UMIPS | mips:*:*:RISCos) > eval $set_cc_for_build > sed 's/^ //' << EOF >$dummy.c >@@ -444,32 +446,33 @@ > exit (-1); > } > EOF >- $CC_FOR_BUILD -o $dummy $dummy.c \ >- && $dummy `echo "${UNAME_RELEASE}" | sed -n 's/\([0-9]*\).*/\1/p'` \ >- && exit 0 >+ $CC_FOR_BUILD -o $dummy $dummy.c && >+ dummyarg=`echo "${UNAME_RELEASE}" | sed -n 's/\([0-9]*\).*/\1/p'` && >+ SYSTEM_NAME=`$dummy $dummyarg` && >+ { echo "$SYSTEM_NAME"; exit; } > echo mips-mips-riscos${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > Motorola:PowerMAX_OS:*:*) > echo powerpc-motorola-powermax >- exit 0 ;; >+ exit ;; > Motorola:*:4.3:PL8-*) > echo powerpc-harris-powermax >- exit 0 ;; >+ exit ;; > Night_Hawk:*:*:PowerMAX_OS | Synergy:PowerMAX_OS:*:*) > echo powerpc-harris-powermax >- exit 0 ;; >+ exit ;; > Night_Hawk:Power_UNIX:*:*) > echo powerpc-harris-powerunix >- exit 0 ;; >+ exit ;; > m88k:CX/UX:7*:*) > echo m88k-harris-cxux7 >- exit 0 ;; >+ exit ;; > m88k:*:4*:R4*) > echo m88k-motorola-sysv4 >- exit 0 ;; >+ exit ;; > m88k:*:3*:R3*) > echo m88k-motorola-sysv3 >- exit 0 ;; >+ exit ;; > AViiON:dgux:*:*) > # DG/UX returns AViiON for all architectures > UNAME_PROCESSOR=`/usr/bin/uname -p` >@@ -485,29 +488,29 @@ > else > echo i586-dg-dgux${UNAME_RELEASE} > fi >- exit 0 ;; >+ exit ;; > M88*:DolphinOS:*:*) # DolphinOS (SVR3) > echo m88k-dolphin-sysv3 >- exit 0 ;; >+ exit ;; > M88*:*:R3*:*) > # Delta 88k system running SVR3 > echo m88k-motorola-sysv3 >- exit 0 ;; >+ exit ;; > XD88*:*:*:*) # Tektronix XD88 system running UTekV (SVR3) > echo m88k-tektronix-sysv3 >- exit 0 ;; >+ exit ;; > Tek43[0-9][0-9]:UTek:*:*) # Tektronix 4300 system running UTek (BSD) > echo m68k-tektronix-bsd >- exit 0 ;; >+ exit ;; > *:IRIX*:*:*) > echo mips-sgi-irix`echo ${UNAME_RELEASE}|sed -e 's/-/_/g'` >- exit 0 ;; >+ exit ;; > ????????:AIX?:[12].1:2) # AIX 2.2.1 or AIX 2.1.1 is RT/PC AIX. >- echo romp-ibm-aix # uname -m gives an 8 hex-code CPU id >- exit 0 ;; # Note that: echo "'`uname -s`'" gives 'AIX ' >+ echo romp-ibm-aix # uname -m gives an 8 hex-code CPU id >+ exit ;; # Note that: echo "'`uname -s`'" gives 'AIX ' > i*86:AIX:*:*) > echo i386-ibm-aix >- exit 0 ;; >+ exit ;; > ia64:AIX:*:*) > if [ -x /usr/bin/oslevel ] ; then > IBM_REV=`/usr/bin/oslevel` >@@ -515,7 +518,7 @@ > IBM_REV=${UNAME_VERSION}.${UNAME_RELEASE} > fi > echo ${UNAME_MACHINE}-ibm-aix${IBM_REV} >- exit 0 ;; >+ exit ;; > *:AIX:2:3) > if grep bos325 /usr/include/stdio.h >/dev/null 2>&1; then > eval $set_cc_for_build >@@ -530,15 +533,19 @@ > exit(0); > } > EOF >- $CC_FOR_BUILD -o $dummy $dummy.c && $dummy && exit 0 >- echo rs6000-ibm-aix3.2.5 >+ if $CC_FOR_BUILD -o $dummy $dummy.c && SYSTEM_NAME=`$dummy` >+ then >+ echo "$SYSTEM_NAME" >+ else >+ echo rs6000-ibm-aix3.2.5 >+ fi > elif grep bos324 /usr/include/stdio.h >/dev/null 2>&1; then > echo rs6000-ibm-aix3.2.4 > else > echo rs6000-ibm-aix3.2 > fi >- exit 0 ;; >- *:AIX:*:[45]) >+ exit ;; >+ *:AIX:*:[456]) > IBM_CPU_ID=`/usr/sbin/lsdev -C -c processor -S available | sed 1q | awk '{ print $1 }'` > if /usr/sbin/lsattr -El ${IBM_CPU_ID} | grep ' POWER' >/dev/null 2>&1; then > IBM_ARCH=rs6000 >@@ -551,28 +558,28 @@ > IBM_REV=${UNAME_VERSION}.${UNAME_RELEASE} > fi > echo ${IBM_ARCH}-ibm-aix${IBM_REV} >- exit 0 ;; >+ exit ;; > *:AIX:*:*) > echo rs6000-ibm-aix >- exit 0 ;; >+ exit ;; > ibmrt:4.4BSD:*|romp-ibm:BSD:*) > echo romp-ibm-bsd4.4 >- exit 0 ;; >+ exit ;; > ibmrt:*BSD:*|romp-ibm:BSD:*) # covers RT/PC BSD and > echo romp-ibm-bsd${UNAME_RELEASE} # 4.3 with uname added to >- exit 0 ;; # report: romp-ibm BSD 4.3 >+ exit ;; # report: romp-ibm BSD 4.3 > *:BOSX:*:*) > echo rs6000-bull-bosx >- exit 0 ;; >+ exit ;; > DPX/2?00:B.O.S.:*:*) > echo m68k-bull-sysv3 >- exit 0 ;; >+ exit ;; > 9000/[34]??:4.3bsd:1.*:*) > echo m68k-hp-bsd >- exit 0 ;; >+ exit ;; > hp300:4.4BSD:*:* | 9000/[34]??:4.3bsd:2.*:*) > echo m68k-hp-bsd4.4 >- exit 0 ;; >+ exit ;; > 9000/[34678]??:HP-UX:*:*) > HPUX_REV=`echo ${UNAME_RELEASE}|sed -e 's/[^.]*.[0B]*//'` > case "${UNAME_MACHINE}" in >@@ -634,9 +641,19 @@ > esac > if [ ${HP_ARCH} = "hppa2.0w" ] > then >- # avoid double evaluation of $set_cc_for_build >- test -n "$CC_FOR_BUILD" || eval $set_cc_for_build >- if echo __LP64__ | (CCOPTS= $CC_FOR_BUILD -E -) | grep __LP64__ >/dev/null >+ eval $set_cc_for_build >+ >+ # hppa2.0w-hp-hpux* has a 64-bit kernel and a compiler generating >+ # 32-bit code. hppa64-hp-hpux* has the same kernel and a compiler >+ # generating 64-bit code. GNU and HP use different nomenclature: >+ # >+ # $ CC_FOR_BUILD=cc ./config.guess >+ # => hppa2.0w-hp-hpux11.23 >+ # $ CC_FOR_BUILD="cc +DA2.0w" ./config.guess >+ # => hppa64-hp-hpux11.23 >+ >+ if echo __LP64__ | (CCOPTS= $CC_FOR_BUILD -E - 2>/dev/null) | >+ grep __LP64__ >/dev/null > then > HP_ARCH="hppa2.0w" > else >@@ -644,11 +661,11 @@ > fi > fi > echo ${HP_ARCH}-hp-hpux${HPUX_REV} >- exit 0 ;; >+ exit ;; > ia64:HP-UX:*:*) > HPUX_REV=`echo ${UNAME_RELEASE}|sed -e 's/[^.]*.[0B]*//'` > echo ia64-hp-hpux${HPUX_REV} >- exit 0 ;; >+ exit ;; > 3050*:HI-UX:*:*) > eval $set_cc_for_build > sed 's/^ //' << EOF >$dummy.c >@@ -676,150 +693,192 @@ > exit (0); > } > EOF >- $CC_FOR_BUILD -o $dummy $dummy.c && $dummy && exit 0 >+ $CC_FOR_BUILD -o $dummy $dummy.c && SYSTEM_NAME=`$dummy` && >+ { echo "$SYSTEM_NAME"; exit; } > echo unknown-hitachi-hiuxwe2 >- exit 0 ;; >+ exit ;; > 9000/7??:4.3bsd:*:* | 9000/8?[79]:4.3bsd:*:* ) > echo hppa1.1-hp-bsd >- exit 0 ;; >+ exit ;; > 9000/8??:4.3bsd:*:*) > echo hppa1.0-hp-bsd >- exit 0 ;; >+ exit ;; > *9??*:MPE/iX:*:* | *3000*:MPE/iX:*:*) > echo hppa1.0-hp-mpeix >- exit 0 ;; >+ exit ;; > hp7??:OSF1:*:* | hp8?[79]:OSF1:*:* ) > echo hppa1.1-hp-osf >- exit 0 ;; >+ exit ;; > hp8??:OSF1:*:*) > echo hppa1.0-hp-osf >- exit 0 ;; >+ exit ;; > i*86:OSF1:*:*) > if [ -x /usr/sbin/sysversion ] ; then > echo ${UNAME_MACHINE}-unknown-osf1mk > else > echo ${UNAME_MACHINE}-unknown-osf1 > fi >- exit 0 ;; >+ exit ;; > parisc*:Lites*:*:*) > echo hppa1.1-hp-lites >- exit 0 ;; >+ exit ;; > C1*:ConvexOS:*:* | convex:ConvexOS:C1*:*) > echo c1-convex-bsd >- exit 0 ;; >+ exit ;; > C2*:ConvexOS:*:* | convex:ConvexOS:C2*:*) > if getsysinfo -f scalar_acc > then echo c32-convex-bsd > else echo c2-convex-bsd > fi >- exit 0 ;; >+ exit ;; > C34*:ConvexOS:*:* | convex:ConvexOS:C34*:*) > echo c34-convex-bsd >- exit 0 ;; >+ exit ;; > C38*:ConvexOS:*:* | convex:ConvexOS:C38*:*) > echo c38-convex-bsd >- exit 0 ;; >+ exit ;; > C4*:ConvexOS:*:* | convex:ConvexOS:C4*:*) > echo c4-convex-bsd >- exit 0 ;; >+ exit ;; > CRAY*Y-MP:*:*:*) > echo ymp-cray-unicos${UNAME_RELEASE} | sed -e 's/\.[^.]*$/.X/' >- exit 0 ;; >+ exit ;; > CRAY*[A-Z]90:*:*:*) > echo ${UNAME_MACHINE}-cray-unicos${UNAME_RELEASE} \ > | sed -e 's/CRAY.*\([A-Z]90\)/\1/' \ > -e y/ABCDEFGHIJKLMNOPQRSTUVWXYZ/abcdefghijklmnopqrstuvwxyz/ \ > -e 's/\.[^.]*$/.X/' >- exit 0 ;; >+ exit ;; > CRAY*TS:*:*:*) > echo t90-cray-unicos${UNAME_RELEASE} | sed -e 's/\.[^.]*$/.X/' >- exit 0 ;; >+ exit ;; > CRAY*T3E:*:*:*) > echo alphaev5-cray-unicosmk${UNAME_RELEASE} | sed -e 's/\.[^.]*$/.X/' >- exit 0 ;; >+ exit ;; > CRAY*SV1:*:*:*) > echo sv1-cray-unicos${UNAME_RELEASE} | sed -e 's/\.[^.]*$/.X/' >- exit 0 ;; >+ exit ;; > *:UNICOS/mp:*:*) >- echo nv1-cray-unicosmp${UNAME_RELEASE} | sed -e 's/\.[^.]*$/.X/' >- exit 0 ;; >+ echo craynv-cray-unicosmp${UNAME_RELEASE} | sed -e 's/\.[^.]*$/.X/' >+ exit ;; > F30[01]:UNIX_System_V:*:* | F700:UNIX_System_V:*:*) > FUJITSU_PROC=`uname -m | tr 'ABCDEFGHIJKLMNOPQRSTUVWXYZ' 'abcdefghijklmnopqrstuvwxyz'` > FUJITSU_SYS=`uname -p | tr 'ABCDEFGHIJKLMNOPQRSTUVWXYZ' 'abcdefghijklmnopqrstuvwxyz' | sed -e 's/\///'` > FUJITSU_REL=`echo ${UNAME_RELEASE} | sed -e 's/ /_/'` > echo "${FUJITSU_PROC}-fujitsu-${FUJITSU_SYS}${FUJITSU_REL}" >- exit 0 ;; >+ exit ;; >+ 5000:UNIX_System_V:4.*:*) >+ FUJITSU_SYS=`uname -p | tr 'ABCDEFGHIJKLMNOPQRSTUVWXYZ' 'abcdefghijklmnopqrstuvwxyz' | sed -e 's/\///'` >+ FUJITSU_REL=`echo ${UNAME_RELEASE} | tr 'ABCDEFGHIJKLMNOPQRSTUVWXYZ' 'abcdefghijklmnopqrstuvwxyz' | sed -e 's/ /_/'` >+ echo "sparc-fujitsu-${FUJITSU_SYS}${FUJITSU_REL}" >+ exit ;; > i*86:BSD/386:*:* | i*86:BSD/OS:*:* | *:Ascend\ Embedded/OS:*:*) > echo ${UNAME_MACHINE}-pc-bsdi${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > sparc*:BSD/OS:*:*) > echo sparc-unknown-bsdi${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > *:BSD/OS:*:*) > echo ${UNAME_MACHINE}-unknown-bsdi${UNAME_RELEASE} >- exit 0 ;; >- *:FreeBSD:*:*|*:GNU/FreeBSD:*:*) >- # Determine whether the default compiler uses glibc. >- eval $set_cc_for_build >- sed 's/^ //' << EOF >$dummy.c >- #include <features.h> >- #if __GLIBC__ >= 2 >- LIBC=gnu >- #else >- LIBC= >- #endif >-EOF >- eval `$CC_FOR_BUILD -E $dummy.c 2>/dev/null | grep ^LIBC=` >- echo ${UNAME_MACHINE}-unknown-freebsd`echo ${UNAME_RELEASE}|sed -e 's/[-(].*//'`${LIBC:+-$LIBC} >- exit 0 ;; >+ exit ;; >+ *:FreeBSD:*:*) >+ case ${UNAME_MACHINE} in >+ pc98) >+ echo i386-unknown-freebsd`echo ${UNAME_RELEASE}|sed -e 's/[-(].*//'` ;; >+ amd64) >+ echo x86_64-unknown-freebsd`echo ${UNAME_RELEASE}|sed -e 's/[-(].*//'` ;; >+ *) >+ echo ${UNAME_MACHINE}-unknown-freebsd`echo ${UNAME_RELEASE}|sed -e 's/[-(].*//'` ;; >+ esac >+ exit ;; > i*:CYGWIN*:*) > echo ${UNAME_MACHINE}-pc-cygwin >- exit 0 ;; >- i*:MINGW*:*) >+ exit ;; >+ *:MINGW*:*) > echo ${UNAME_MACHINE}-pc-mingw32 >- exit 0 ;; >+ exit ;; >+ i*:windows32*:*) >+ # uname -m includes "-pc" on this system. >+ echo ${UNAME_MACHINE}-mingw32 >+ exit ;; > i*:PW*:*) > echo ${UNAME_MACHINE}-pc-pw32 >- exit 0 ;; >- x86:Interix*:[34]*) >- echo i586-pc-interix${UNAME_RELEASE}|sed -e 's/\..*//' >- exit 0 ;; >+ exit ;; >+ *:Interix*:[3456]*) >+ case ${UNAME_MACHINE} in >+ x86) >+ echo i586-pc-interix${UNAME_RELEASE} >+ exit ;; >+ EM64T | authenticamd | genuineintel) >+ echo x86_64-unknown-interix${UNAME_RELEASE} >+ exit ;; >+ IA64) >+ echo ia64-unknown-interix${UNAME_RELEASE} >+ exit ;; >+ esac ;; > [345]86:Windows_95:* | [345]86:Windows_98:* | [345]86:Windows_NT:*) > echo i${UNAME_MACHINE}-pc-mks >- exit 0 ;; >+ exit ;; > i*:Windows_NT*:* | Pentium*:Windows_NT*:*) > # How do we know it's Interix rather than the generic POSIX subsystem? > # It also conflicts with pre-2.0 versions of AT&T UWIN. Should we > # UNAME_MACHINE based on the output of uname instead of i386? > echo i586-pc-interix >- exit 0 ;; >+ exit ;; > i*:UWIN*:*) > echo ${UNAME_MACHINE}-pc-uwin >- exit 0 ;; >+ exit ;; >+ amd64:CYGWIN*:*:* | x86_64:CYGWIN*:*:*) >+ echo x86_64-unknown-cygwin >+ exit ;; > p*:CYGWIN*:*) > echo powerpcle-unknown-cygwin >- exit 0 ;; >+ exit ;; > prep*:SunOS:5.*:*) > echo powerpcle-unknown-solaris2`echo ${UNAME_RELEASE}|sed -e 's/[^.]*//'` >- exit 0 ;; >+ exit ;; > *:GNU:*:*) >+ # the GNU system > echo `echo ${UNAME_MACHINE}|sed -e 's,[-/].*$,,'`-unknown-gnu`echo ${UNAME_RELEASE}|sed -e 's,/.*$,,'` >- exit 0 ;; >+ exit ;; >+ *:GNU/*:*:*) >+ # other systems with GNU libc and userland >+ echo ${UNAME_MACHINE}-unknown-`echo ${UNAME_SYSTEM} | sed 's,^[^/]*/,,' | tr '[A-Z]' '[a-z]'``echo ${UNAME_RELEASE}|sed -e 's/[-(].*//'`-gnu >+ exit ;; > i*86:Minix:*:*) > echo ${UNAME_MACHINE}-pc-minix >- exit 0 ;; >+ exit ;; > arm*:Linux:*:*) >+ eval $set_cc_for_build >+ if echo __ARM_EABI__ | $CC_FOR_BUILD -E - 2>/dev/null \ >+ | grep -q __ARM_EABI__ >+ then >+ echo ${UNAME_MACHINE}-unknown-linux-gnu >+ else >+ echo ${UNAME_MACHINE}-unknown-linux-gnueabi >+ fi >+ exit ;; >+ avr32*:Linux:*:*) > echo ${UNAME_MACHINE}-unknown-linux-gnu >- exit 0 ;; >+ exit ;; > cris:Linux:*:*) > echo cris-axis-linux-gnu >- exit 0 ;; >+ exit ;; >+ crisv32:Linux:*:*) >+ echo crisv32-axis-linux-gnu >+ exit ;; >+ frv:Linux:*:*) >+ echo frv-unknown-linux-gnu >+ exit ;; > ia64:Linux:*:*) >- echo ${UNAME_MACHINE}-${VENDOR:-unknown}-linux-gnu >- exit 0 ;; >+ echo ${UNAME_MACHINE}-unknown-linux-gnu >+ exit ;; >+ m32r*:Linux:*:*) >+ echo ${UNAME_MACHINE}-unknown-linux-gnu >+ exit ;; > m68*:Linux:*:*) > echo ${UNAME_MACHINE}-unknown-linux-gnu >- exit 0 ;; >+ exit ;; > mips:Linux:*:*) > eval $set_cc_for_build > sed 's/^ //' << EOF >$dummy.c >@@ -836,8 +895,12 @@ > #endif > #endif > EOF >- eval `$CC_FOR_BUILD -E $dummy.c 2>/dev/null | grep ^CPU=` >- test x"${CPU}" != x && echo "${CPU}-unknown-linux-gnu" && exit 0 >+ eval "`$CC_FOR_BUILD -E $dummy.c 2>/dev/null | sed -n ' >+ /^CPU/{ >+ s: ::g >+ p >+ }'`" >+ test x"${CPU}" != x && { echo "${CPU}-unknown-linux-gnu"; exit; } > ;; > mips64:Linux:*:*) > eval $set_cc_for_build >@@ -855,15 +918,22 @@ > #endif > #endif > EOF >- eval `$CC_FOR_BUILD -E $dummy.c 2>/dev/null | grep ^CPU=` >- test x"${CPU}" != x && echo "${CPU}-unknown-linux-gnu" && exit 0 >+ eval "`$CC_FOR_BUILD -E $dummy.c 2>/dev/null | sed -n ' >+ /^CPU/{ >+ s: ::g >+ p >+ }'`" >+ test x"${CPU}" != x && { echo "${CPU}-unknown-linux-gnu"; exit; } > ;; >+ or32:Linux:*:*) >+ echo or32-unknown-linux-gnu >+ exit ;; > ppc:Linux:*:*) >- echo powerpc-${VENDOR:-unknown}-linux-gnu >- exit 0 ;; >+ echo powerpc-unknown-linux-gnu >+ exit ;; > ppc64:Linux:*:*) >- echo powerpc64-${VENDOR:-unknown}-linux-gnu >- exit 0 ;; >+ echo powerpc64-unknown-linux-gnu >+ exit ;; > alpha:Linux:*:*) > case `sed -n '/^cpu model/s/^.*: \(.*\)/\1/p' < /proc/cpuinfo` in > EV5) UNAME_MACHINE=alphaev5 ;; >@@ -877,7 +947,10 @@ > objdump --private-headers /bin/sh | grep ld.so.1 >/dev/null > if test "$?" = 0 ; then LIBC="libc1" ; else LIBC="" ; fi > echo ${UNAME_MACHINE}-unknown-linux-gnu${LIBC} >- exit 0 ;; >+ exit ;; >+ padre:Linux:*:*) >+ echo sparc-unknown-linux-gnu >+ exit ;; > parisc:Linux:*:* | hppa:Linux:*:*) > # Look for CPU level > case `grep '^cpu[^a-z]*:' /proc/cpuinfo 2>/dev/null | cut -d' ' -f2` in >@@ -885,25 +958,31 @@ > PA8*) echo hppa2.0-unknown-linux-gnu ;; > *) echo hppa-unknown-linux-gnu ;; > esac >- exit 0 ;; >+ exit ;; > parisc64:Linux:*:* | hppa64:Linux:*:*) > echo hppa64-unknown-linux-gnu >- exit 0 ;; >+ exit ;; > s390:Linux:*:* | s390x:Linux:*:*) >- echo ${UNAME_MACHINE}-${VENDOR:-ibm}-linux-gnu >- exit 0 ;; >+ echo ${UNAME_MACHINE}-ibm-linux >+ exit ;; > sh64*:Linux:*:*) > echo ${UNAME_MACHINE}-unknown-linux-gnu >- exit 0 ;; >+ exit ;; > sh*:Linux:*:*) > echo ${UNAME_MACHINE}-unknown-linux-gnu >- exit 0 ;; >+ exit ;; > sparc:Linux:*:* | sparc64:Linux:*:*) > echo ${UNAME_MACHINE}-unknown-linux-gnu >- exit 0 ;; >+ exit ;; >+ vax:Linux:*:*) >+ echo ${UNAME_MACHINE}-dec-linux-gnu >+ exit ;; > x86_64:Linux:*:*) >- echo x86_64-${VENDOR:-unknown}-linux-gnu >- exit 0 ;; >+ echo x86_64-unknown-linux-gnu >+ exit ;; >+ xtensa*:Linux:*:*) >+ echo ${UNAME_MACHINE}-unknown-linux-gnu >+ exit ;; > i*86:Linux:*:*) > # The BFD linker knows what the default object file format is, so > # first see if it will tell us. cd to the root directory to prevent >@@ -921,15 +1000,12 @@ > ;; > a.out-i386-linux) > echo "${UNAME_MACHINE}-pc-linux-gnuaout" >- exit 0 ;; >- coff-i386) >- echo "${UNAME_MACHINE}-pc-linux-gnucoff" >- exit 0 ;; >+ exit ;; > "") > # Either a pre-BFD a.out linker (linux-gnuoldld) or > # one that does not give us useful --help. > echo "${UNAME_MACHINE}-pc-linux-gnuoldld" >- exit 0 ;; >+ exit ;; > esac > # Determine whether the default compiler is a.out or elf > eval $set_cc_for_build >@@ -946,23 +1022,33 @@ > LIBC=gnulibc1 > # endif > #else >- #ifdef __INTEL_COMPILER >+ #if defined(__INTEL_COMPILER) || defined(__PGI) || defined(__SUNPRO_C) || defined(__SUNPRO_CC) > LIBC=gnu > #else > LIBC=gnuaout > #endif > #endif >+ #ifdef __dietlibc__ >+ LIBC=dietlibc >+ #endif > EOF >- eval `$CC_FOR_BUILD -E $dummy.c 2>/dev/null | grep ^LIBC=` >- test x"${LIBC}" != x && echo "${UNAME_MACHINE}-${VENDOR:-pc}-linux-${LIBC}" && exit 0 >- test x"${TENTATIVE}" != x && echo "${TENTATIVE}" && exit 0 >+ eval "`$CC_FOR_BUILD -E $dummy.c 2>/dev/null | sed -n ' >+ /^LIBC/{ >+ s: ::g >+ p >+ }'`" >+ test x"${LIBC}" != x && { >+ echo "${UNAME_MACHINE}-pc-linux-${LIBC}" >+ exit >+ } >+ test x"${TENTATIVE}" != x && { echo "${TENTATIVE}"; exit; } > ;; > i*86:DYNIX/ptx:4*:*) > # ptx 4.0 does uname -s correctly, with DYNIX/ptx in there. > # earlier versions are messed up and put the nodename in both > # sysname and nodename. > echo i386-sequent-sysv4 >- exit 0 ;; >+ exit ;; > i*86:UNIX_SV:4.2MP:2.*) > # Unixware is an offshoot of SVR4, but it has its own version > # number series starting with 2... >@@ -970,24 +1056,27 @@ > # I just have to hope. -- rms. > # Use sysv4.2uw... so that sysv4* matches it. > echo ${UNAME_MACHINE}-pc-sysv4.2uw${UNAME_VERSION} >- exit 0 ;; >+ exit ;; > i*86:OS/2:*:*) > # If we were able to find `uname', then EMX Unix compatibility > # is probably installed. > echo ${UNAME_MACHINE}-pc-os2-emx >- exit 0 ;; >+ exit ;; > i*86:XTS-300:*:STOP) > echo ${UNAME_MACHINE}-unknown-stop >- exit 0 ;; >+ exit ;; > i*86:atheos:*:*) > echo ${UNAME_MACHINE}-unknown-atheos >- exit 0 ;; >+ exit ;; >+ i*86:syllable:*:*) >+ echo ${UNAME_MACHINE}-pc-syllable >+ exit ;; > i*86:LynxOS:2.*:* | i*86:LynxOS:3.[01]*:* | i*86:LynxOS:4.0*:*) > echo i386-unknown-lynxos${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > i*86:*DOS:*:*) > echo ${UNAME_MACHINE}-pc-msdosdjgpp >- exit 0 ;; >+ exit ;; > i*86:*:4.*:* | i*86:SYSTEM_V:4.*:*) > UNAME_REL=`echo ${UNAME_RELEASE} | sed 's/\/MP$//'` > if grep Novell /usr/include/link.h >/dev/null 2>/dev/null; then >@@ -995,15 +1084,16 @@ > else > echo ${UNAME_MACHINE}-pc-sysv${UNAME_REL} > fi >- exit 0 ;; >- i*86:*:5:[78]*) >+ exit ;; >+ i*86:*:5:[678]*) >+ # UnixWare 7.x, OpenUNIX and OpenServer 6. > case `/bin/uname -X | grep "^Machine"` in > *486*) UNAME_MACHINE=i486 ;; > *Pentium) UNAME_MACHINE=i586 ;; > *Pent*|*Celeron) UNAME_MACHINE=i686 ;; > esac > echo ${UNAME_MACHINE}-unknown-sysv${UNAME_RELEASE}${UNAME_SYSTEM}${UNAME_VERSION} >- exit 0 ;; >+ exit ;; > i*86:*:3.2:*) > if test -f /usr/options/cb.name; then > UNAME_REL=`sed -n 's/.*Version //p' </usr/options/cb.name` >@@ -1021,73 +1111,83 @@ > else > echo ${UNAME_MACHINE}-pc-sysv32 > fi >- exit 0 ;; >+ exit ;; > pc:*:*:*) > # Left here for compatibility: > # uname -m prints for DJGPP always 'pc', but it prints nothing about > # the processor, so we play safe by assuming i386. > echo i386-pc-msdosdjgpp >- exit 0 ;; >+ exit ;; > Intel:Mach:3*:*) > echo i386-pc-mach3 >- exit 0 ;; >+ exit ;; > paragon:*:*:*) > echo i860-intel-osf1 >- exit 0 ;; >+ exit ;; > i860:*:4.*:*) # i860-SVR4 > if grep Stardent /usr/include/sys/uadmin.h >/dev/null 2>&1 ; then > echo i860-stardent-sysv${UNAME_RELEASE} # Stardent Vistra i860-SVR4 > else # Add other i860-SVR4 vendors below as they are discovered. > echo i860-unknown-sysv${UNAME_RELEASE} # Unknown i860-SVR4 > fi >- exit 0 ;; >+ exit ;; > mini*:CTIX:SYS*5:*) > # "miniframe" > echo m68010-convergent-sysv >- exit 0 ;; >+ exit ;; > mc68k:UNIX:SYSTEM5:3.51m) > echo m68k-convergent-sysv >- exit 0 ;; >+ exit ;; > M680?0:D-NIX:5.3:*) > echo m68k-diab-dnix >- exit 0 ;; >- M68*:*:R3V[567]*:*) >- test -r /sysV68 && echo 'm68k-motorola-sysv' && exit 0 ;; >- 3[34]??:*:4.0:3.0 | 3[34]??A:*:4.0:3.0 | 3[34]??,*:*:4.0:3.0 | 3[34]??/*:*:4.0:3.0 | 4400:*:4.0:3.0 | 4850:*:4.0:3.0 | SKA40:*:4.0:3.0 | SDS2:*:4.0:3.0 | SHG2:*:4.0:3.0) >+ exit ;; >+ M68*:*:R3V[5678]*:*) >+ test -r /sysV68 && { echo 'm68k-motorola-sysv'; exit; } ;; >+ 3[345]??:*:4.0:3.0 | 3[34]??A:*:4.0:3.0 | 3[34]??,*:*:4.0:3.0 | 3[34]??/*:*:4.0:3.0 | 4400:*:4.0:3.0 | 4850:*:4.0:3.0 | SKA40:*:4.0:3.0 | SDS2:*:4.0:3.0 | SHG2:*:4.0:3.0 | S7501*:*:4.0:3.0) > OS_REL='' > test -r /etc/.relid \ > && OS_REL=.`sed -n 's/[^ ]* [^ ]* \([0-9][0-9]\).*/\1/p' < /etc/.relid` > /bin/uname -p 2>/dev/null | grep 86 >/dev/null \ >- && echo i486-ncr-sysv4.3${OS_REL} && exit 0 >+ && { echo i486-ncr-sysv4.3${OS_REL}; exit; } > /bin/uname -p 2>/dev/null | /bin/grep entium >/dev/null \ >- && echo i586-ncr-sysv4.3${OS_REL} && exit 0 ;; >+ && { echo i586-ncr-sysv4.3${OS_REL}; exit; } ;; > 3[34]??:*:4.0:* | 3[34]??,*:*:4.0:*) > /bin/uname -p 2>/dev/null | grep 86 >/dev/null \ >- && echo i486-ncr-sysv4 && exit 0 ;; >+ && { echo i486-ncr-sysv4; exit; } ;; >+ NCR*:*:4.2:* | MPRAS*:*:4.2:*) >+ OS_REL='.3' >+ test -r /etc/.relid \ >+ && OS_REL=.`sed -n 's/[^ ]* [^ ]* \([0-9][0-9]\).*/\1/p' < /etc/.relid` >+ /bin/uname -p 2>/dev/null | grep 86 >/dev/null \ >+ && { echo i486-ncr-sysv4.3${OS_REL}; exit; } >+ /bin/uname -p 2>/dev/null | /bin/grep entium >/dev/null \ >+ && { echo i586-ncr-sysv4.3${OS_REL}; exit; } >+ /bin/uname -p 2>/dev/null | /bin/grep pteron >/dev/null \ >+ && { echo i586-ncr-sysv4.3${OS_REL}; exit; } ;; > m68*:LynxOS:2.*:* | m68*:LynxOS:3.0*:*) > echo m68k-unknown-lynxos${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > mc68030:UNIX_System_V:4.*:*) > echo m68k-atari-sysv4 >- exit 0 ;; >+ exit ;; > TSUNAMI:LynxOS:2.*:*) > echo sparc-unknown-lynxos${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > rs6000:LynxOS:2.*:*) > echo rs6000-unknown-lynxos${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > PowerPC:LynxOS:2.*:* | PowerPC:LynxOS:3.[01]*:* | PowerPC:LynxOS:4.0*:*) > echo powerpc-unknown-lynxos${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > SM[BE]S:UNIX_SV:*:*) > echo mips-dde-sysv${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > RM*:ReliantUNIX-*:*:*) > echo mips-sni-sysv4 >- exit 0 ;; >+ exit ;; > RM*:SINIX-*:*:*) > echo mips-sni-sysv4 >- exit 0 ;; >+ exit ;; > *:SINIX-*:*:*) > if uname -p 2>/dev/null >/dev/null ; then > UNAME_MACHINE=`(uname -p) 2>/dev/null` >@@ -1095,68 +1195,84 @@ > else > echo ns32k-sni-sysv > fi >- exit 0 ;; >+ exit ;; > PENTIUM:*:4.0*:*) # Unisys `ClearPath HMP IX 4000' SVR4/MP effort > # says <Richard.M.Bartel@ccMail.Census.GOV> > echo i586-unisys-sysv4 >- exit 0 ;; >+ exit ;; > *:UNIX_System_V:4*:FTX*) > # From Gerald Hewes <hewes@openmarket.com>. > # How about differentiating between stratus architectures? -djm > echo hppa1.1-stratus-sysv4 >- exit 0 ;; >+ exit ;; > *:*:*:FTX*) > # From seanf@swdc.stratus.com. > echo i860-stratus-sysv4 >- exit 0 ;; >+ exit ;; >+ i*86:VOS:*:*) >+ # From Paul.Green@stratus.com. >+ echo ${UNAME_MACHINE}-stratus-vos >+ exit ;; > *:VOS:*:*) > # From Paul.Green@stratus.com. > echo hppa1.1-stratus-vos >- exit 0 ;; >+ exit ;; > mc68*:A/UX:*:*) > echo m68k-apple-aux${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > news*:NEWS-OS:6*:*) > echo mips-sony-newsos6 >- exit 0 ;; >+ exit ;; > R[34]000:*System_V*:*:* | R4000:UNIX_SYSV:*:* | R*000:UNIX_SV:*:*) > if [ -d /usr/nec ]; then > echo mips-nec-sysv${UNAME_RELEASE} > else > echo mips-unknown-sysv${UNAME_RELEASE} > fi >- exit 0 ;; >+ exit ;; > BeBox:BeOS:*:*) # BeOS running on hardware made by Be, PPC only. > echo powerpc-be-beos >- exit 0 ;; >+ exit ;; > BeMac:BeOS:*:*) # BeOS running on Mac or Mac clone, PPC only. > echo powerpc-apple-beos >- exit 0 ;; >+ exit ;; > BePC:BeOS:*:*) # BeOS running on Intel PC compatible. > echo i586-pc-beos >- exit 0 ;; >+ exit ;; >+ BePC:Haiku:*:*) # Haiku running on Intel PC compatible. >+ echo i586-pc-haiku >+ exit ;; > SX-4:SUPER-UX:*:*) > echo sx4-nec-superux${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > SX-5:SUPER-UX:*:*) > echo sx5-nec-superux${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > SX-6:SUPER-UX:*:*) > echo sx6-nec-superux${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; >+ SX-7:SUPER-UX:*:*) >+ echo sx7-nec-superux${UNAME_RELEASE} >+ exit ;; >+ SX-8:SUPER-UX:*:*) >+ echo sx8-nec-superux${UNAME_RELEASE} >+ exit ;; >+ SX-8R:SUPER-UX:*:*) >+ echo sx8r-nec-superux${UNAME_RELEASE} >+ exit ;; > Power*:Rhapsody:*:*) > echo powerpc-apple-rhapsody${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > *:Rhapsody:*:*) > echo ${UNAME_MACHINE}-apple-rhapsody${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > *:Darwin:*:*) >- case `uname -p` in >- *86) UNAME_PROCESSOR=i686 ;; >- powerpc) UNAME_PROCESSOR=powerpc ;; >+ UNAME_PROCESSOR=`uname -p` || UNAME_PROCESSOR=unknown >+ case $UNAME_PROCESSOR in >+ unknown) UNAME_PROCESSOR=powerpc ;; > esac > echo ${UNAME_PROCESSOR}-apple-darwin${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > *:procnto*:*:* | *:QNX:[0123456789]*:*) > UNAME_PROCESSOR=`uname -p` > if test "$UNAME_PROCESSOR" = "x86"; then >@@ -1164,22 +1280,25 @@ > UNAME_MACHINE=pc > fi > echo ${UNAME_PROCESSOR}-${UNAME_MACHINE}-nto-qnx${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > *:QNX:*:4*) > echo i386-pc-qnx >- exit 0 ;; >- NSR-[DGKLNPTVW]:NONSTOP_KERNEL:*:*) >+ exit ;; >+ NSE-?:NONSTOP_KERNEL:*:*) >+ echo nse-tandem-nsk${UNAME_RELEASE} >+ exit ;; >+ NSR-?:NONSTOP_KERNEL:*:*) > echo nsr-tandem-nsk${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > *:NonStop-UX:*:*) > echo mips-compaq-nonstopux >- exit 0 ;; >+ exit ;; > BS2000:POSIX*:*:*) > echo bs2000-siemens-sysv >- exit 0 ;; >+ exit ;; > DS/*:UNIX_System_V:*:*) > echo ${UNAME_MACHINE}-${UNAME_SYSTEM}-${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; > *:Plan9:*:*) > # "uname -m" is not consistent, so use $cputype instead. 386 > # is converted to i386 for consistency with other x86 >@@ -1190,28 +1309,47 @@ > UNAME_MACHINE="$cputype" > fi > echo ${UNAME_MACHINE}-unknown-plan9 >- exit 0 ;; >+ exit ;; > *:TOPS-10:*:*) > echo pdp10-unknown-tops10 >- exit 0 ;; >+ exit ;; > *:TENEX:*:*) > echo pdp10-unknown-tenex >- exit 0 ;; >+ exit ;; > KS10:TOPS-20:*:* | KL10:TOPS-20:*:* | TYPE4:TOPS-20:*:*) > echo pdp10-dec-tops20 >- exit 0 ;; >+ exit ;; > XKL-1:TOPS-20:*:* | TYPE5:TOPS-20:*:*) > echo pdp10-xkl-tops20 >- exit 0 ;; >+ exit ;; > *:TOPS-20:*:*) > echo pdp10-unknown-tops20 >- exit 0 ;; >+ exit ;; > *:ITS:*:*) > echo pdp10-unknown-its >- exit 0 ;; >+ exit ;; > SEI:*:*:SEIUX) > echo mips-sei-seiux${UNAME_RELEASE} >- exit 0 ;; >+ exit ;; >+ *:DragonFly:*:*) >+ echo ${UNAME_MACHINE}-unknown-dragonfly`echo ${UNAME_RELEASE}|sed -e 's/[-(].*//'` >+ exit ;; >+ *:*VMS:*:*) >+ UNAME_MACHINE=`(uname -p) 2>/dev/null` >+ case "${UNAME_MACHINE}" in >+ A*) echo alpha-dec-vms ; exit ;; >+ I*) echo ia64-dec-vms ; exit ;; >+ V*) echo vax-dec-vms ; exit ;; >+ esac ;; >+ *:XENIX:*:SysV) >+ echo i386-pc-xenix >+ exit ;; >+ i*86:skyos:*:*) >+ echo ${UNAME_MACHINE}-pc-skyos`echo ${UNAME_RELEASE}` | sed -e 's/ .*$//' >+ exit ;; >+ i*86:rdos:*:*) >+ echo ${UNAME_MACHINE}-pc-rdos >+ exit ;; > esac > > #echo '(No uname command or uname output not recognized.)' 1>&2 >@@ -1243,7 +1381,7 @@ > #endif > > #if defined (__arm) && defined (__acorn) && defined (__unix) >- printf ("arm-acorn-riscix"); exit (0); >+ printf ("arm-acorn-riscix\n"); exit (0); > #endif > > #if defined (hp300) && !defined (hpux) >@@ -1332,11 +1470,12 @@ > } > EOF > >-$CC_FOR_BUILD -o $dummy $dummy.c 2>/dev/null && $dummy && exit 0 >+$CC_FOR_BUILD -o $dummy $dummy.c 2>/dev/null && SYSTEM_NAME=`$dummy` && >+ { echo "$SYSTEM_NAME"; exit; } > > # Apollos put the system type in the environment. > >-test -d /usr/apollo && { echo ${ISP}-apollo-${SYSTYPE}; exit 0; } >+test -d /usr/apollo && { echo ${ISP}-apollo-${SYSTYPE}; exit; } > > # Convex versions that predate uname can use getsysinfo(1) > >@@ -1345,22 +1484,22 @@ > case `getsysinfo -f cpu_type` in > c1*) > echo c1-convex-bsd >- exit 0 ;; >+ exit ;; > c2*) > if getsysinfo -f scalar_acc > then echo c32-convex-bsd > else echo c2-convex-bsd > fi >- exit 0 ;; >+ exit ;; > c34*) > echo c34-convex-bsd >- exit 0 ;; >+ exit ;; > c38*) > echo c38-convex-bsd >- exit 0 ;; >+ exit ;; > c4*) > echo c4-convex-bsd >- exit 0 ;; >+ exit ;; > esac > fi > >@@ -1371,7 +1510,9 @@ > the operating system you are using. It is advised that you > download the most up to date version of the config scripts from > >- ftp://ftp.gnu.org/pub/gnu/config/ >+ http://git.savannah.gnu.org/gitweb/?p=config.git;a=blob_plain;f=config.guess;hb=HEAD >+and >+ http://git.savannah.gnu.org/gitweb/?p=config.git;a=blob_plain;f=config.sub;hb=HEAD > > If the version you run ($0) is already up to date, please > send the following data and any information you think might be >diff -Naur pvs4.2-orig/config.sub pvs4.2-sbcl/config.sub >--- pvs4.2-orig/config.sub 2007-07-02 20:07:43.000000000 +0000 >+++ pvs4.2-sbcl/config.sub 2009-03-24 18:56:17.000000000 +0000 >@@ -1,9 +1,10 @@ > #! /bin/sh > # Configuration validation subroutine script. > # Copyright (C) 1992, 1993, 1994, 1995, 1996, 1997, 1998, 1999, >-# 2000, 2001, 2002, 2003 Free Software Foundation, Inc. >+# 2000, 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008 >+# Free Software Foundation, Inc. > >-timestamp='2003-06-18' >+timestamp='2009-01-19' > > # This file is (in principle) common to ALL GNU software. > # The presence of a machine in this file suggests that SOME GNU software >@@ -21,14 +22,15 @@ > # > # 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. >- >+# Foundation, Inc., 51 Franklin Street - Fifth Floor, Boston, MA >+# 02110-1301, USA. >+# > # As a special exception to the GNU General Public License, if you > # distribute this file as part of a program that contains a > # configuration script generated by Autoconf, you may include it under > # the same distribution terms that you use for the rest of that program. > >+ > # Please send patches to <config-patches@gnu.org>. Submit a context > # diff and a properly formatted ChangeLog entry. > # >@@ -70,8 +72,8 @@ > version="\ > GNU config.sub ($timestamp) > >-Copyright (C) 1992, 1993, 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001 >-Free Software Foundation, Inc. >+Copyright (C) 1992, 1993, 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, >+2002, 2003, 2004, 2005, 2006, 2007, 2008 Free Software Foundation, Inc. > > This is free software; see the source for copying conditions. There is NO > warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE." >@@ -83,11 +85,11 @@ > while test $# -gt 0 ; do > case $1 in > --time-stamp | --time* | -t ) >- echo "$timestamp" ; exit 0 ;; >+ echo "$timestamp" ; exit ;; > --version | -v ) >- echo "$version" ; exit 0 ;; >+ echo "$version" ; exit ;; > --help | --h* | -h ) >- echo "$usage"; exit 0 ;; >+ echo "$usage"; exit ;; > -- ) # Stop option processing > shift; break ;; > - ) # Use stdin as input. >@@ -99,7 +101,7 @@ > *local*) > # First pass through any local machine types. > echo $1 >- exit 0;; >+ exit ;; > > * ) > break ;; >@@ -118,7 +120,10 @@ > # Here we must recognize all the valid KERNEL-OS combinations. > maybe_os=`echo $1 | sed 's/^\(.*\)-\([^-]*-[^-]*\)$/\2/'` > case $maybe_os in >- nto-qnx* | linux-gnu* | freebsd*-gnu* | netbsd*-gnu* | storm-chaos* | os2-emx* | rtmk-nova*) >+ nto-qnx* | linux-gnu* | linux-dietlibc | linux-newlib* | linux-uclibc* | \ >+ uclinux-uclibc* | uclinux-gnu* | kfreebsd*-gnu* | knetbsd*-gnu* | netbsd*-gnu* | \ >+ kopensolaris*-gnu* | \ >+ storm-chaos* | os2-emx* | rtmk-nova*) > os=-$maybe_os > basic_machine=`echo $1 | sed 's/^\(.*\)-\([^-]*-[^-]*\)$/\1/'` > ;; >@@ -144,7 +149,7 @@ > -convergent* | -ncr* | -news | -32* | -3600* | -3100* | -hitachi* |\ > -c[123]* | -convex* | -sun | -crds | -omron* | -dg | -ultra | -tti* | \ > -harris | -dolphin | -highlevel | -gould | -cbm | -ns | -masscomp | \ >- -apple | -axis) >+ -apple | -axis | -knuth | -cray) > os= > basic_machine=$1 > ;; >@@ -169,6 +174,10 @@ > -hiux*) > os=-hiuxwe2 > ;; >+ -sco6) >+ os=-sco5v6 >+ basic_machine=`echo $1 | sed -e 's/86-.*/86-pc/'` >+ ;; > -sco5) > os=-sco3.2v5 > basic_machine=`echo $1 | sed -e 's/86-.*/86-pc/'` >@@ -185,6 +194,10 @@ > # Don't forget version if it is 3.2v4 or newer. > basic_machine=`echo $1 | sed -e 's/86-.*/86-pc/'` > ;; >+ -sco5v6*) >+ # Don't forget version if it is 3.2v4 or newer. >+ basic_machine=`echo $1 | sed -e 's/86-.*/86-pc/'` >+ ;; > -sco*) > os=-sco3.2v2 > basic_machine=`echo $1 | sed -e 's/86-.*/86-pc/'` >@@ -228,45 +241,56 @@ > | a29k \ > | alpha | alphaev[4-8] | alphaev56 | alphaev6[78] | alphapca5[67] \ > | alpha64 | alpha64ev[4-8] | alpha64ev56 | alpha64ev6[78] | alpha64pca5[67] \ >- | arc | arm | arm[bl]e | arme[lb] | armv[2345] | armv[345][lb] | avr \ >+ | am33_2.0 \ >+ | arc | arm | arm[bl]e | arme[lb] | armv[2345] | armv[345][lb] | avr | avr32 \ >+ | bfin \ > | c4x | clipper \ > | d10v | d30v | dlx | dsp16xx \ >- | fr30 | frv \ >+ | fido | fr30 | frv \ > | h8300 | h8500 | hppa | hppa1.[01] | hppa2.0 | hppa2.0[nw] | hppa64 \ > | i370 | i860 | i960 | ia64 \ >- | ip2k \ >- | m32r | m68000 | m68k | m88k | mcore \ >+ | ip2k | iq2000 \ >+ | lm32 \ >+ | m32c | m32r | m32rle | m68000 | m68k | m88k \ >+ | maxq | mb | microblaze | mcore | mep | metag \ > | mips | mipsbe | mipseb | mipsel | mipsle \ > | mips16 \ > | mips64 | mips64el \ >- | mips64vr | mips64vrel \ >+ | mips64octeon | mips64octeonel \ > | mips64orion | mips64orionel \ >+ | mips64r5900 | mips64r5900el \ >+ | mips64vr | mips64vrel \ > | mips64vr4100 | mips64vr4100el \ > | mips64vr4300 | mips64vr4300el \ > | mips64vr5000 | mips64vr5000el \ >+ | mips64vr5900 | mips64vr5900el \ > | mipsisa32 | mipsisa32el \ > | mipsisa32r2 | mipsisa32r2el \ > | mipsisa64 | mipsisa64el \ >+ | mipsisa64r2 | mipsisa64r2el \ > | mipsisa64sb1 | mipsisa64sb1el \ > | mipsisa64sr71k | mipsisa64sr71kel \ > | mipstx39 | mipstx39el \ > | mn10200 | mn10300 \ >+ | mt \ > | msp430 \ >+ | nios | nios2 \ > | ns16k | ns32k \ >- | openrisc | or32 \ >+ | or32 \ > | pdp10 | pdp11 | pj | pjl \ > | powerpc | powerpc64 | powerpc64le | powerpcle | ppcbe \ > | pyramid \ >- | s390 | s390x \ >- | sh | sh[1234] | sh[23]e | sh[34]eb | shbe | shle | sh[1234]le | sh3ele \ >+ | score \ >+ | sh | sh[1234] | sh[24]a | sh[24]aeb | sh[23]e | sh[34]eb | sheb | shbe | shle | sh[1234]le | sh3ele \ > | sh64 | sh64le \ >- | sparc | sparc64 | sparc86x | sparclet | sparclite | sparcv8 | sparcv9 | sparcv9b \ >- | strongarm \ >+ | sparc | sparc64 | sparc64b | sparc64v | sparc86x | sparclet | sparclite \ >+ | sparcv8 | sparcv9 | sparcv9b | sparcv9v \ >+ | spu | strongarm \ > | tahoe | thumb | tic4x | tic80 | tron \ > | v850 | v850e \ > | we32k \ >- | x86 | xscale | xstormy16 | xtensa \ >- | z8k) >+ | x86 | xc16x | xscale | xscalee[bl] | xstormy16 | xtensa \ >+ | z8k | z80) > basic_machine=$basic_machine-unknown > ;; > m6811 | m68hc11 | m6812 | m68hc12) >@@ -276,6 +300,9 @@ > ;; > m88110 | m680[12346]0 | m683?2 | m68360 | m5200 | v70 | w65 | z8k) > ;; >+ ms1) >+ basic_machine=mt-unknown >+ ;; > > # We use `pc' rather than `unknown' > # because (1) that's what they normally are, and >@@ -295,55 +322,67 @@ > | alpha64-* | alpha64ev[4-8]-* | alpha64ev56-* | alpha64ev6[78]-* \ > | alphapca5[67]-* | alpha64pca5[67]-* | arc-* \ > | arm-* | armbe-* | armle-* | armeb-* | armv*-* \ >- | avr-* \ >- | bs2000-* \ >+ | avr-* | avr32-* \ >+ | bfin-* | bs2000-* \ > | c[123]* | c30-* | [cjt]90-* | c4x-* | c54x-* | c55x-* | c6x-* \ >- | clipper-* | cydra-* \ >+ | clipper-* | craynv-* | cydra-* \ > | d10v-* | d30v-* | dlx-* \ > | elxsi-* \ >- | f30[01]-* | f700-* | fr30-* | frv-* | fx80-* \ >+ | f30[01]-* | f700-* | fido-* | fr30-* | frv-* | fx80-* \ > | h8300-* | h8500-* \ > | hppa-* | hppa1.[01]-* | hppa2.0-* | hppa2.0[nw]-* | hppa64-* \ > | i*86-* | i860-* | i960-* | ia64-* \ >- | ip2k-* \ >- | m32r-* \ >+ | ip2k-* | iq2000-* \ >+ | lm32-* \ >+ | m32c-* | m32r-* | m32rle-* \ > | m68000-* | m680[012346]0-* | m68360-* | m683?2-* | m68k-* \ >- | m88110-* | m88k-* | mcore-* \ >+ | m88110-* | m88k-* | maxq-* | mcore-* | metag-* \ > | mips-* | mipsbe-* | mipseb-* | mipsel-* | mipsle-* \ > | mips16-* \ > | mips64-* | mips64el-* \ >- | mips64vr-* | mips64vrel-* \ >+ | mips64octeon-* | mips64octeonel-* \ > | mips64orion-* | mips64orionel-* \ >+ | mips64r5900-* | mips64r5900el-* \ >+ | mips64vr-* | mips64vrel-* \ > | mips64vr4100-* | mips64vr4100el-* \ > | mips64vr4300-* | mips64vr4300el-* \ > | mips64vr5000-* | mips64vr5000el-* \ >+ | mips64vr5900-* | mips64vr5900el-* \ > | mipsisa32-* | mipsisa32el-* \ > | mipsisa32r2-* | mipsisa32r2el-* \ > | mipsisa64-* | mipsisa64el-* \ >+ | mipsisa64r2-* | mipsisa64r2el-* \ > | mipsisa64sb1-* | mipsisa64sb1el-* \ > | mipsisa64sr71k-* | mipsisa64sr71kel-* \ > | mipstx39-* | mipstx39el-* \ >+ | mmix-* \ >+ | mt-* \ > | msp430-* \ >- | none-* | np1-* | nv1-* | ns16k-* | ns32k-* \ >+ | nios-* | nios2-* \ >+ | none-* | np1-* | ns16k-* | ns32k-* \ > | orion-* \ > | pdp10-* | pdp11-* | pj-* | pjl-* | pn-* | power-* \ > | powerpc-* | powerpc64-* | powerpc64le-* | powerpcle-* | ppcbe-* \ > | pyramid-* \ > | romp-* | rs6000-* \ >- | s390-* | s390x-* \ >- | sh-* | sh[1234]-* | sh[23]e-* | sh[34]eb-* | shbe-* \ >+ | sh-* | sh[1234]-* | sh[24]a-* | sh[24]aeb-* | sh[23]e-* | sh[34]eb-* | sheb-* | shbe-* \ > | shle-* | sh[1234]le-* | sh3ele-* | sh64-* | sh64le-* \ >- | sparc-* | sparc64-* | sparc86x-* | sparclet-* | sparclite-* \ >- | sparcv8-* | sparcv9-* | sparcv9b-* | strongarm-* | sv1-* | sx?-* \ >+ | sparc-* | sparc64-* | sparc64b-* | sparc64v-* | sparc86x-* | sparclet-* \ >+ | sparclite-* \ >+ | sparcv8-* | sparcv9-* | sparcv9b-* | sparcv9v-* | strongarm-* | sv1-* | sx?-* \ > | tahoe-* | thumb-* \ >- | tic30-* | tic4x-* | tic54x-* | tic55x-* | tic6x-* | tic80-* \ >+ | tic30-* | tic4x-* | tic54x-* | tic55x-* | tic6x-* | tic80-* | tile-* \ > | tron-* \ > | v850-* | v850e-* | vax-* \ > | we32k-* \ >- | x86-* | x86_64-* | xps100-* | xscale-* | xstormy16-* \ >- | xtensa-* \ >+ | x86-* | x86_64-* | xc16x-* | xps100-* | xscale-* | xscalee[bl]-* \ >+ | xstormy16-* | xtensa*-* \ > | ymp-* \ >- | z8k-*) >+ | z8k-* | z80-*) >+ ;; >+ # Recognize the basic CPU types without company name, with glob match. >+ xtensa*) >+ basic_machine=$basic_machine-unknown > ;; > # Recognize the various machine names and aliases which stand > # for a CPU type and a company and sometimes even an OS. >@@ -361,6 +400,9 @@ > basic_machine=a29k-amd > os=-udi > ;; >+ abacus) >+ basic_machine=abacus-unknown >+ ;; > adobe68k) > basic_machine=m68010-adobe > os=-scout >@@ -378,6 +420,9 @@ > amd64) > basic_machine=x86_64-pc > ;; >+ amd64-*) >+ basic_machine=x86_64-`echo $basic_machine | sed 's/^[^-]*-//'` >+ ;; > amdahl) > basic_machine=580-amdahl > os=-sysv >@@ -409,10 +454,22 @@ > basic_machine=ns32k-sequent > os=-dynix > ;; >+ blackfin) >+ basic_machine=bfin-unknown >+ os=-linux >+ ;; >+ blackfin-*) >+ basic_machine=bfin-`echo $basic_machine | sed 's/^[^-]*-//'` >+ os=-linux >+ ;; > c90) > basic_machine=c90-cray > os=-unicos > ;; >+ cegcc) >+ basic_machine=arm-unknown >+ os=-cegcc >+ ;; > convex-c1) > basic_machine=c1-convex > os=-bsd >@@ -437,12 +494,27 @@ > basic_machine=j90-cray > os=-unicos > ;; >+ craynv) >+ basic_machine=craynv-cray >+ os=-unicosmp >+ ;; >+ cr16) >+ basic_machine=cr16-unknown >+ os=-elf >+ ;; > crds | unos) > basic_machine=m68k-crds > ;; >+ crisv32 | crisv32-* | etraxfs*) >+ basic_machine=crisv32-axis >+ ;; > cris | cris-* | etrax*) > basic_machine=cris-axis > ;; >+ crx) >+ basic_machine=crx-unknown >+ os=-elf >+ ;; > da30 | da30-*) > basic_machine=m68k-da30 > ;; >@@ -465,6 +537,14 @@ > basic_machine=m88k-motorola > os=-sysv3 > ;; >+ dicos) >+ basic_machine=i686-pc >+ os=-dicos >+ ;; >+ djgpp) >+ basic_machine=i586-pc >+ os=-msdosdjgpp >+ ;; > dpx20 | dpx20-*) > basic_machine=rs6000-bull > os=-bosx >@@ -615,6 +695,14 @@ > basic_machine=m68k-isi > os=-sysv > ;; >+ m68knommu) >+ basic_machine=m68k-unknown >+ os=-linux >+ ;; >+ m68knommu-*) >+ basic_machine=m68k-`echo $basic_machine | sed 's/^[^-]*-//'` >+ os=-linux >+ ;; > m88k-omron*) > basic_machine=m88k-omron > ;; >@@ -630,6 +718,10 @@ > basic_machine=i386-pc > os=-mingw32 > ;; >+ mingw32ce) >+ basic_machine=arm-unknown >+ os=-mingw32ce >+ ;; > miniframe) > basic_machine=m68000-convergent > ;; >@@ -643,10 +735,6 @@ > mips3*) > basic_machine=`echo $basic_machine | sed -e 's/mips3/mips64/'`-unknown > ;; >- mmix*) >- basic_machine=mmix-knuth >- os=-mmixware >- ;; > monitor) > basic_machine=m68k-rom68k > os=-coff >@@ -659,6 +747,9 @@ > basic_machine=i386-pc > os=-msdos > ;; >+ ms1-*) >+ basic_machine=`echo $basic_machine | sed -e 's/ms1-/mt-/'` >+ ;; > mvs) > basic_machine=i370-ibm > os=-mvs >@@ -727,10 +818,6 @@ > np1) > basic_machine=np1-gould > ;; >- nv1) >- basic_machine=nv1-cray >- os=-unicosmp >- ;; > nsr-tandem) > basic_machine=nsr-tandem > ;; >@@ -738,9 +825,12 @@ > basic_machine=hppa1.1-oki > os=-proelf > ;; >- or32 | or32-*) >+ openrisc | openrisc-*) > basic_machine=or32-unknown >- os=-coff >+ ;; >+ os400) >+ basic_machine=powerpc-ibm >+ os=-os400 > ;; > OSE68000 | ose68000) > basic_machine=m68000-ericsson >@@ -758,6 +848,14 @@ > basic_machine=i860-intel > os=-osf > ;; >+ parisc) >+ basic_machine=hppa-unknown >+ os=-linux >+ ;; >+ parisc-*) >+ basic_machine=hppa-`echo $basic_machine | sed 's/^[^-]*-//'` >+ os=-linux >+ ;; > pbd) > basic_machine=sparc-tti > ;; >@@ -767,6 +865,12 @@ > pc532 | pc532-*) > basic_machine=ns32k-pc532 > ;; >+ pc98) >+ basic_machine=i386-pc >+ ;; >+ pc98-*) >+ basic_machine=i386-`echo $basic_machine | sed 's/^[^-]*-//'` >+ ;; > pentium | p5 | k5 | k6 | nexgen | viac3) > basic_machine=i586-pc > ;; >@@ -823,6 +927,10 @@ > basic_machine=i586-unknown > os=-pw32 > ;; >+ rdos) >+ basic_machine=i386-pc >+ os=-rdos >+ ;; > rom68k) > basic_machine=m68k-rom68k > os=-coff >@@ -833,6 +941,12 @@ > rtpc | rtpc-*) > basic_machine=romp-ibm > ;; >+ s390 | s390-*) >+ basic_machine=s390-ibm >+ ;; >+ s390x | s390x-*) >+ basic_machine=s390x-ibm >+ ;; > sa29200) > basic_machine=a29k-amd > os=-udi >@@ -843,6 +957,10 @@ > sb1el) > basic_machine=mipsisa64sb1el-unknown > ;; >+ sde) >+ basic_machine=mipsisa32-sde >+ os=-elf >+ ;; > sei) > basic_machine=mips-sei > os=-seiux >@@ -854,6 +972,9 @@ > basic_machine=sh-hitachi > os=-hms > ;; >+ sh5el) >+ basic_machine=sh5le-unknown >+ ;; > sh64) > basic_machine=sh64-unknown > ;; >@@ -943,6 +1064,10 @@ > basic_machine=tic6x-unknown > os=-coff > ;; >+ tile*) >+ basic_machine=tile-unknown >+ os=-linux-gnu >+ ;; > tx39) > basic_machine=mipstx39-unknown > ;; >@@ -956,6 +1081,10 @@ > tower | tower-32) > basic_machine=m68k-ncr > ;; >+ tpf) >+ basic_machine=s390x-ibm >+ os=-tpf >+ ;; > udi29k) > basic_machine=a29k-amd > os=-udi >@@ -999,6 +1128,10 @@ > basic_machine=hppa1.1-winbond > os=-proelf > ;; >+ xbox) >+ basic_machine=i686-pc >+ os=-mingw32 >+ ;; > xps | xps100) > basic_machine=xps100-honeywell > ;; >@@ -1010,6 +1143,10 @@ > basic_machine=z8k-unknown > os=-sim > ;; >+ z80-*-coff) >+ basic_machine=z80-unknown >+ os=-sim >+ ;; > none) > basic_machine=none-none > os=-none >@@ -1029,6 +1166,9 @@ > romp) > basic_machine=romp-ibm > ;; >+ mmix) >+ basic_machine=mmix-knuth >+ ;; > rs6000) > basic_machine=rs6000-ibm > ;; >@@ -1045,13 +1185,10 @@ > we32k) > basic_machine=we32k-att > ;; >- sh3 | sh4 | sh[34]eb | sh[1234]le | sh[23]ele) >+ sh[1234] | sh[24]a | sh[24]aeb | sh[34]eb | sh[1234]le | sh[23]ele) > basic_machine=sh-unknown > ;; >- sh64) >- basic_machine=sh64-unknown >- ;; >- sparc | sparcv8 | sparcv9 | sparcv9b) >+ sparc | sparcv8 | sparcv9 | sparcv9b | sparcv9v) > basic_machine=sparc-sun > ;; > cydra) >@@ -1120,23 +1257,28 @@ > -gnu* | -bsd* | -mach* | -minix* | -genix* | -ultrix* | -irix* \ > | -*vms* | -sco* | -esix* | -isc* | -aix* | -sunos | -sunos[34]*\ > | -hpux* | -unos* | -osf* | -luna* | -dgux* | -solaris* | -sym* \ >+ | -kopensolaris* \ > | -amigaos* | -amigados* | -msdos* | -newsos* | -unicos* | -aof* \ > | -aos* \ > | -nindy* | -vxsim* | -vxworks* | -ebmon* | -hms* | -mvs* \ > | -clix* | -riscos* | -uniplus* | -iris* | -rtu* | -xenix* \ >- | -hiux* | -386bsd* | -netbsd* | -openbsd* | -freebsd* | -riscix* \ >- | -lynxos* | -bosx* | -nextstep* | -cxux* | -aout* | -elf* | -oabi* \ >+ | -hiux* | -386bsd* | -knetbsd* | -mirbsd* | -netbsd* \ >+ | -openbsd* | -solidbsd* \ >+ | -ekkobsd* | -kfreebsd* | -freebsd* | -riscix* | -lynxos* \ >+ | -bosx* | -nextstep* | -cxux* | -aout* | -elf* | -oabi* \ > | -ptx* | -coff* | -ecoff* | -winnt* | -domain* | -vsta* \ > | -udi* | -eabi* | -lites* | -ieee* | -go32* | -aux* \ >- | -chorusos* | -chorusrdb* \ >+ | -chorusos* | -chorusrdb* | -cegcc* \ > | -cygwin* | -pe* | -psos* | -moss* | -proelf* | -rtems* \ >- | -mingw32* | -linux-gnu* | -uxpv* | -beos* | -mpeix* | -udk* \ >+ | -mingw32* | -linux-gnu* | -linux-newlib* | -linux-uclibc* \ >+ | -uxpv* | -beos* | -mpeix* | -udk* \ > | -interix* | -uwin* | -mks* | -rhapsody* | -darwin* | -opened* \ > | -openstep* | -oskit* | -conix* | -pw32* | -nonstopux* \ > | -storm-chaos* | -tops10* | -tenex* | -tops20* | -its* \ > | -os2* | -vos* | -palmos* | -uclinux* | -nucleus* \ > | -morphos* | -superux* | -rtmk* | -rtmk-nova* | -windiss* \ >- | -powermax* | -dnix* | -nx6 | -nx7 | -sei*) >+ | -powermax* | -dnix* | -nx6 | -nx7 | -sei* | -dragonfly* \ >+ | -skyos* | -haiku* | -rdos* | -toppers* | -drops*) > # Remember, each alternative MUST END IN *, to match a version number. > ;; > -qnx*) >@@ -1154,12 +1296,15 @@ > os=`echo $os | sed -e 's|nto|nto-qnx|'` > ;; > -sim | -es1800* | -hms* | -xray | -os68k* | -none* | -v88r* \ >- | -windows* | -osx | -abug | -netware* | -os9* | -beos* \ >+ | -windows* | -osx | -abug | -netware* | -os9* | -beos* | -haiku* \ > | -macos* | -mpw* | -magic* | -mmixware* | -mon960* | -lnews*) > ;; > -mac*) > os=`echo $os | sed -e 's|mac|macos|'` > ;; >+ -linux-dietlibc) >+ os=-linux-dietlibc >+ ;; > -linux*) > os=`echo $os | sed -e 's|linux|linux-gnu|'` > ;; >@@ -1172,6 +1317,9 @@ > -opened*) > os=-openedition > ;; >+ -os400*) >+ os=-os400 >+ ;; > -wince*) > os=-wince > ;; >@@ -1193,6 +1341,9 @@ > -atheos*) > os=-atheos > ;; >+ -syllable*) >+ os=-syllable >+ ;; > -386bsd) > os=-bsd > ;; >@@ -1215,6 +1366,9 @@ > -sinix*) > os=-sysv4 > ;; >+ -tpf*) >+ os=-tpf >+ ;; > -triton*) > os=-sysv3 > ;; >@@ -1251,6 +1405,12 @@ > -kaos*) > os=-kaos > ;; >+ -zvmoe) >+ os=-zvmoe >+ ;; >+ -dicos*) >+ os=-dicos >+ ;; > -none) > ;; > *) >@@ -1273,6 +1433,12 @@ > # system, and we'll never get to this point. > > case $basic_machine in >+ score-*) >+ os=-elf >+ ;; >+ spu-*) >+ os=-elf >+ ;; > *-acorn) > os=-riscix1.2 > ;; >@@ -1282,8 +1448,8 @@ > arm*-semi) > os=-aout > ;; >- c4x-* | tic4x-*) >- os=-coff >+ c4x-* | tic4x-*) >+ os=-coff > ;; > # This must come before the *-dec entry. > pdp10-*) >@@ -1310,6 +1476,9 @@ > m68*-cisco) > os=-aout > ;; >+ mep-*) >+ os=-elf >+ ;; > mips*-cisco) > os=-elf > ;; >@@ -1328,9 +1497,15 @@ > *-be) > os=-beos > ;; >+ *-haiku) >+ os=-haiku >+ ;; > *-ibm) > os=-aix > ;; >+ *-knuth) >+ os=-mmixware >+ ;; > *-wec) > os=-proelf > ;; >@@ -1463,9 +1638,15 @@ > -mvs* | -opened*) > vendor=ibm > ;; >+ -os400*) >+ vendor=ibm >+ ;; > -ptx*) > vendor=sequent > ;; >+ -tpf*) >+ vendor=ibm >+ ;; > -vxsim* | -vxworks* | -windiss*) > vendor=wrs > ;; >@@ -1490,7 +1671,7 @@ > esac > > echo $basic_machine$os >-exit 0 >+exit > > # Local variables: > # eval: (add-hook 'write-file-hooks 'time-stamp) >diff -Naur pvs4.2-orig/doc/language/language.tex pvs4.2-sbcl/doc/language/language.tex >--- pvs4.2-orig/doc/language/language.tex 2007-07-02 20:07:42.000000000 +0000 >+++ pvs4.2-sbcl/doc/language/language.tex 2009-03-24 18:56:17.000000000 +0000 >@@ -6,7 +6,7 @@ > \usepackage{makeidx} > \usepackage{relsize} > \usepackage{boxedminipage} >-\usepackage{fancyheadings} >+\usepackage{fancyhdr} > %\usepackage{../../pvs} > \usepackage{url} > \usepackage{../makebnf} >diff -Naur pvs4.2-orig/doc/prover/prover.tex pvs4.2-sbcl/doc/prover/prover.tex >--- pvs4.2-orig/doc/prover/prover.tex 2007-07-02 20:07:42.000000000 +0000 >+++ pvs4.2-sbcl/doc/prover/prover.tex 2009-03-24 18:56:17.000000000 +0000 >@@ -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 -Naur pvs4.2-orig/doc/user-guide/user-guide.tex pvs4.2-sbcl/doc/user-guide/user-guide.tex >--- pvs4.2-orig/doc/user-guide/user-guide.tex 2007-07-02 20:07:42.000000000 +0000 >+++ pvs4.2-sbcl/doc/user-guide/user-guide.tex 2009-03-24 18:56:17.000000000 +0000 >@@ -7,7 +7,7 @@ > %\usepackage{showidx} % use for index debugging > \usepackage{relsize} > \usepackage{boxedminipage} >-\usepackage{fancyheadings} >+\usepackage{fancyhdr} > \usepackage{graphicx} > \usepackage{../../pvs} > \usepackage{url} >diff -Naur pvs4.2-orig/emacs/emacs-src/ilisp/completer.el pvs4.2-sbcl/emacs/emacs-src/ilisp/completer.el >--- pvs4.2-orig/emacs/emacs-src/ilisp/completer.el 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/emacs/emacs-src/ilisp/completer.el 2009-03-24 18:56:17.000000000 +0000 >@@ -181,8 +181,8 @@ > (not (memq +ilisp-emacs-version-id+ > '(xemacs lucid-19 lucid-19-new))) > ) >- (setq quit-flag nil >- unread-command-char 7)))) >+ (setq quit-flag nil) >+ (push 7 unread-command-events)))) > > ;;; > (defun completer-deleter (regexp choices &optional keep) >diff -Naur pvs4.2-orig/emacs/emacs-src/ilisp/ilisp-acl.el pvs4.2-sbcl/emacs/emacs-src/ilisp/ilisp-acl.el >--- pvs4.2-orig/emacs/emacs-src/ilisp/ilisp-acl.el 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/emacs/emacs-src/ilisp/ilisp-acl.el 2009-03-24 18:56:17.000000000 +0000 >@@ -22,10 +22,10 @@ > (defun allegro-check-prompt (old new) > "Compare the break level printed at the beginning of the prompt." > (let* ((old-level (if (and old (eq 1 (string-match "[0-9]+" old))) >- (string-to-int (substring old 1)) >+ (string-to-number (substring old 1)) > 0)) > (new-level (if (eq 1 (string-match "[0-9]+" new)) >- (string-to-int (substring new 1)) >+ (string-to-number (substring new 1)) > 0))) > (<= new-level old-level))) > >diff -Naur pvs4.2-orig/emacs/emacs-src/ilisp/ilisp-chs.el pvs4.2-sbcl/emacs/emacs-src/ilisp/ilisp-chs.el >--- pvs4.2-orig/emacs/emacs-src/ilisp/ilisp-chs.el 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/emacs/emacs-src/ilisp/ilisp-chs.el 2009-03-24 18:56:17.000000000 +0000 >@@ -40,7 +40,7 @@ > (string-match "Break" old) > (string-match "[0-9]+" old))) > (old-level (if was-in >- (string-to-int >+ (string-to-number > (substring old (match-beginning 0) > (match-end 0))) > 0)) >@@ -48,7 +48,7 @@ > (string-match "Break" new) > (string-match "[0-9]+" new))) > (new-level (if is-in >- (string-to-int >+ (string-to-number > (substring new (match-beginning 0) > (match-end 0))) > 0))) >diff -Naur pvs4.2-orig/emacs/emacs-src/ilisp/ilisp-def.el pvs4.2-sbcl/emacs/emacs-src/ilisp/ilisp-def.el >--- pvs4.2-orig/emacs/emacs-src/ilisp/ilisp-def.el 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/emacs/emacs-src/ilisp/ilisp-def.el 2009-03-24 18:56:17.000000000 +0000 >@@ -43,8 +43,8 @@ > ;;; > (defmacro deflocal (variable default &optional documentation) > "Define an ilisp local variable." >- (` (progn (lisp-deflocal '(, variable)) >- (defvar (, variable) (, default) (, documentation))))) >+ `(progn (lisp-deflocal ',variable) >+ (defvar ,variable ,default ,documentation))) > > ;;;%%Simple customization > >diff -Naur pvs4.2-orig/emacs/emacs-src/ilisp/ilisp-dia.el pvs4.2-sbcl/emacs/emacs-src/ilisp/ilisp-dia.el >--- pvs4.2-orig/emacs/emacs-src/ilisp/ilisp-dia.el 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/emacs/emacs-src/ilisp/ilisp-dia.el 2009-03-24 18:56:17.000000000 +0000 >@@ -120,27 +120,26 @@ > (hook (read (format "%s-hook" dialect))) > (program (read (format "%s-program" dialect))) > (dialects (format "%s" dialect))) >- (` >- (progn >- (defvar (, hook) nil (, (format "*Inferior %s hook." full-name))) >- (defvar (, program) nil >- (, (format "*Inferior %s default program." full-name))) >- (defun (, setup) (buffer) >- (, (format "Set up for interacting with %s." full-name)) >- (, (read (format "(setup-%s buffer)" parent))) >- (,@ body) >- (setq ilisp-program (or (, program) ilisp-program) >- ilisp-dialect (cons '(, dialect) ilisp-dialect)) >- (run-hooks '(, (read (format "%s-hook" dialect))))) >- (defun (, dialect) (&optional buffer program) >- (, (format "Create an inferior %s. With prefix, prompt for buffer and program." >- full-name)) >+ `(progn >+ (defvar ,hook nil ,(format "*Inferior %s hook." full-name)) >+ (defvar ,program nil >+ ,(format "*Inferior %s default program." full-name)) >+ (defun ,setup (buffer) >+ ,(format "Set up for interacting with %s." full-name) >+ ,(read (format "(setup-%s buffer)" parent)) >+ ,@body >+ (setq ilisp-program (or ,program ilisp-program) >+ ilisp-dialect (cons ',dialect ilisp-dialect)) >+ (run-hooks ',(read (format "%s-hook" dialect)))) >+ (defun ,dialect (&optional buffer program) >+ ,(format "Create an inferior %s. With prefix, prompt for buffer and program." >+ full-name) > (interactive (list nil nil)) >- (ilisp-start-dialect (or buffer (, dialects)) >- program >- '(, setup)) >- (setq (, program) ilisp-program)) >- (lisp-add-dialect (, dialects)))))) >+ (ilisp-start-dialect (or buffer ,dialects) >+ program >+ ',setup) >+ (setq ,program ilisp-program)) >+ (lisp-add-dialect ,dialects)))) > > ;;;%%ilisp > (defun setup-ilisp (buffer) >diff -Naur pvs4.2-orig/emacs/emacs-src/ilisp/ilisp-snd.el pvs4.2-sbcl/emacs/emacs-src/ilisp/ilisp-snd.el >--- pvs4.2-orig/emacs/emacs-src/ilisp/ilisp-snd.el 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/emacs/emacs-src/ilisp/ilisp-snd.el 2009-03-24 18:56:17.000000000 +0000 >@@ -409,16 +409,16 @@ > (comint-send > (ilisp-process) binary > t nil 'binary nil >- (` (lambda (error wait message output last) >+ `(lambda (error wait message output last) > (if (or error > (not (string-match "\"[^\"]*\"" output))) > (progn > (lisp-display-output output) > (abort-commands-lisp "No binary")) >- (setq (, var) >+ (setq ,var > (substring output > (1+ (match-beginning 0)) >- (1- (match-end 0)))))))))))) >+ (1- (match-end 0))))))))))) > > ;;; > (defun ilisp-done-init () >diff -Naur pvs4.2-orig/emacs/emacs-src/pvs-cmds.el pvs4.2-sbcl/emacs/emacs-src/pvs-cmds.el >--- pvs4.2-orig/emacs/emacs-src/pvs-cmds.el 2008-02-20 10:35:41.000000000 +0000 >+++ pvs4.2-sbcl/emacs/emacs-src/pvs-cmds.el 2009-03-24 18:56:17.000000000 +0000 >@@ -478,7 +478,7 @@ > (goto-char (point-min)) > (pop-to-buffer pbuf) > (pvs-mode)) >- (error "%s is not in the prelude.")))))) >+ (error "%s is not in the prelude." fname)))))) > > (defun get-prelude-file-and-region (theoryname) > (let ((freg nil) >@@ -768,7 +768,7 @@ > "Name of root file (CR for this one): ") > (list (y-or-n-p "Include libraries? ")) > (list (read-from-minibuffer >- (format "Mail to: " pvs-last-email-address) >+ (format "Mail to: ") > pvs-last-email-address)) > (list (read-string "CC: ")) > (list (read-string "Subject: ")))) >@@ -787,9 +787,9 @@ > (let* ((lkeymap (copy-keymap (current-local-map))) > (file-string (pvs-dump-files-string pvs-file libraries-p))) > (define-key lkeymap "\C-c\C-c" >- (` (lambda () >- (interactive) >- (pvs-mail-send-and-exit (, to) (, subject) (, file-string))))) >+ `(lambda () >+ (interactive) >+ (pvs-mail-send-and-exit ,to ,subject ,file-string))) > (use-local-map lkeymap))) > > (defun pvs-mail-send-and-exit (to subject file-string) >@@ -1435,8 +1435,8 @@ > > (defun pvs-major-version-number () > (if *pvs-version-information* >- (string-to-int (car *pvs-version-information*)) >- (string-to-int (pvs-send-and-wait "*pvs-version*" nil nil)))) >+ (string-to-number (car *pvs-version-information*)) >+ (string-to-number (pvs-send-and-wait "*pvs-version*" nil nil)))) > > ;;; Replay > >diff -Naur pvs4.2-orig/emacs/emacs-src/pvs-ilisp.el pvs4.2-sbcl/emacs/emacs-src/pvs-ilisp.el >--- pvs4.2-orig/emacs/emacs-src/pvs-ilisp.el 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/emacs/emacs-src/pvs-ilisp.el 2009-03-24 18:56:17.000000000 +0000 >@@ -111,6 +111,7 @@ > (case (intern (getenv "PVSLISP")) > (allegro (pvsallegro "pvs" nil)) > (cmulisp (pvscmulisp "pvs" nil)) >+ (sbclisp (pvssbclisp "pvs" nil)) > (t (error "Unknown lisp - %s" (getenv "PVSLISP")))) > (save-excursion > (set-buffer (ilisp-buffer)) >@@ -164,7 +165,7 @@ > (setq ilisp-binary-extension (pvs-cmulisp-binary-extension)) > (setq ilisp-init-binary-extension ilisp-binary-extension) > (setq ilisp-load-inits nil) >- (setq ilisp-program (format "%s -qq" (pvs-program))) >+ (setq ilisp-program (format "%s -quiet -noinit" (pvs-program))) > (setq comint-prompt-regexp > "^\\([0-9]+\\]+\\|\\*\\|[-a-zA-Z0-9]*\\[[0-9]+\\]:\\) \\|Rule\\? \\|<GndEval> \\|<PVSio> \\|(Y or N)\\|(Yes or No)\\|Please enter") > (setq comint-interrupt-regexp "^Interrupted at") >@@ -173,6 +174,24 @@ > "^\\([0-9]+\\]+\\|\\*\\|[-a-zA-Z0-9]*\\[[0-9]+\\]:\\) ") > (setq pvs-gc-end-regexp ";;; Finished GC")) > >+(defdialect pvssbclisp "pvs-sbclisp" >+ cmulisp >+ (pvs-comint-init) >+ ;;(setq comint-send-newline nil) >+ (setq ilisp-binary-extension (pvs-sbclisp-binary-extension)) >+ (setq ilisp-init-binary-extension ilisp-binary-extension) >+ (setq ilisp-load-inits nil) >+ (setq ilisp-program (format "%s --noinform --no-userinit" (pvs-program))) >+ (setq ilisp-reset ":abort") >+ (setq comint-prompt-regexp >+ "^\\([0-9]+\\]+\\|\\*\\|[-a-zA-Z0-9]*\\[[0-9]+\\]:\\) \\|Rule\\? \\|<GndEval> \\|<PVSio> \\|(Y or N)\\|(Yes or No)\\|Please enter") >+ (setq comint-interrupt-regexp "^ Interactive interrupt at") >+ (setq comint-continue ":continue") >+ (setq ilisp-error-regexp "^restarts (invokable by number or by possibly-abbreviated name):$") >+ (setq pvs-top-regexp >+ "^\\([0-9]+\\]+\\|\\*\\|[-a-zA-Z0-9]*\\[[0-9]+\\]:\\) ") >+ (setq pvs-gc-end-regexp ";;; Finished GC")) >+ > (defun pvs-allegro-binary-extension () > (let ((machine (getenv "PVSARCH"))) > (cond ((string-equal machine "sun4") ; Sun/Solaris >@@ -193,6 +212,18 @@ > "ppcf") > (t (error "Machine architecture %s not recognized" machine))))) > >+(defun pvs-sbclisp-binary-extension () >+ (let ((machine (getenv "PVSARCH"))) >+ (cond ((string-equal machine "sun4") ; Sun/Solaris >+ "sparcs") >+ ((string-equal machine "ix86") ; Intel/Linux >+ "x86s") >+ ((string-equal machine "ix86_64") ; Intel/Linux >+ "x8664s") >+ ((string-equal machine "powerpc") ; Mac >+ "ppcs") >+ (t (error "Machine architecture %s not recognized" machine))))) >+ > (defun pvs-comint-init () > (setq ilisp-motd nil) > (setq pvs-fix-error comint-fix-error) >@@ -736,7 +767,7 @@ > > (defun resize-info-buffer () > (unless (one-window-p t) >- (let* ((maxsize (/ (screen-height) 2)) >+ (let* ((maxsize (/ (frame-height) 2)) > (cursize (1- (window-height))) > (lines (real-number-of-lines)) > (size (min maxsize lines))) >@@ -1108,11 +1139,6 @@ > (show-entry)) > (t (error "Unknown display type %s" type)))))) > >-(defun pvs-locate (out) >- (apply 'display-file-at-location >- (parse-pvs-message out))) >- >- > (defun pvs-locate (output) > (let* ((message (parse-pvs-message output)) > (dir (car message)) >diff -Naur pvs4.2-orig/emacs/emacs-src/pvs-load.el pvs4.2-sbcl/emacs/emacs-src/pvs-load.el >--- pvs4.2-orig/emacs/emacs-src/pvs-load.el 2008-07-07 08:03:45.000000000 +0000 >+++ pvs4.2-sbcl/emacs/emacs-src/pvs-load.el 2009-03-24 18:56:17.000000000 +0000 >@@ -238,7 +238,7 @@ > (insert "\n\nPlease check our website periodically for news of later versions") > (insert "\nat http://pvs.csl.sri.com/") > (insert "\n\n" (cadr (cdddr vers)) "\n" (cadr (cddddr vers))) >- (insert-string " >+ (insert " > ---------- > Bug reports and suggestions for improvement should be sent to > pvs-bugs@csl.sri.com >diff -Naur pvs4.2-orig/emacs/emacs-src/pvs-prover.el pvs4.2-sbcl/emacs/emacs-src/pvs-prover.el >--- pvs4.2-orig/emacs/emacs-src/pvs-prover.el 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/emacs/emacs-src/pvs-prover.el 2009-03-24 18:56:17.000000000 +0000 >@@ -1043,7 +1043,7 @@ > (if (> indent 0) > (while (and (>= (point) start) > (progn (beginning-of-line) >- (insert-string indstr) >+ (insert indstr) > (= (forward-line -1) 0)))))) > (when crs (insert "\n\n")))) > >@@ -1084,7 +1084,7 @@ > (pvs-bury-output) > (let ((file (current-pvs-file))) > (when (buffer-modified-p (get-file-buffer file)) >- (error "~a is not parsed" file)) >+ (error "%s is not parsed" file)) > (when (pvs-send-and-wait (format "(lisp (modify-declaration-at \"%s\" %d))" > file (current-line-number)) > nil nil 'bool) >@@ -1192,7 +1192,7 @@ > nil) > ((and (stringp depth) > (string-match "^[ \t]*[0-9]+[ \t]*$" depth)) >- (string-to-int depth)) >+ (string-to-number depth)) > (t (error "set-rewrite-depth: %s is not a number or nil" > depth))))) > (pvs-send (format "(setq *rewrite-print-depth* %s)" dep)))) >@@ -1221,7 +1221,7 @@ > nil) > ((and (stringp length) > (string-match "^[ \t]*[0-9]+[ \t]*$" length)) >- (string-to-int length)) >+ (string-to-number length)) > (t (error "set-rewrite-length: %s is not an integer or nil" > length))))) > (pvs-send (format "(setq *rewrite-print-length* %s)" len)))) >@@ -1242,7 +1242,7 @@ > nil) > ((and (stringp depth) > (string-match "^[ \t]*[0-9]+[ \t]*$" depth)) >- (string-to-int depth)) >+ (string-to-number depth)) > (t (error "set-print-depth: %s is not an integer" depth))))) > (pvs-send (format "(setq *prover-print-depth* %s)" > (when (plusp dep) dep))))) >@@ -1264,7 +1264,7 @@ > nil) > ((and (stringp length) > (string-match "^[ \t]*[0-9]+[ \t]*$" length)) >- (string-to-int length)) >+ (string-to-number length)) > (t (error "set-print-length: %s is not an integer" > length))))) > (pvs-send (format "(setq *prover-print-length* %s)" >@@ -1285,7 +1285,7 @@ > nil) > ((and (stringp lines) > (string-match "^[ \t]*[0-9]+[ \t]*$" lines)) >- (string-to-int lines)) >+ (string-to-number lines)) > (t (error "set-print-lines: %s is not an integer" lines))))) > (pvs-send (format "(setq *prover-print-lines* %s)" > (when (plusp dep) dep))))) >@@ -2153,7 +2153,7 @@ > 1) > ((and (stringp num) > (string-match "^[ \t]*[0-9]+[ \t]*$" num)) >- (string-to-int num)) >+ (string-to-number num)) > (t (error "set-proof-backup-number: %s is not an integer" > num))))) > (pvs-send (format "(setq *number-of-proof-backups* %s)" n)))) >diff -Naur pvs4.2-orig/emacs/emacs-src/pvs-prover-helps.el pvs4.2-sbcl/emacs/emacs-src/pvs-prover-helps.el >--- pvs4.2-orig/emacs/emacs-src/pvs-prover-helps.el 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/emacs/emacs-src/pvs-prover-helps.el 2009-03-24 18:56:17.000000000 +0000 >@@ -244,7 +244,7 @@ > (setq ept (point)) > (setq def2arw (buffer-substring bpt ept))) > (setq def2arw (read-from-minibuffer "Auto-rewrite: "))) >- (end-of-buffer) >+ (goto-char (point-max)) > (insert "(auto-rewrite " ?\" def2arw ?\" ")") > (return-ilisp))) > >@@ -372,7 +372,7 @@ > (setq fnum (buffer-substring bpt ept))) > (setq fnum (read-from-minibuffer > "in formula [CR for default]# " "")))) >- (end-of-buffer) >+ (goto-char (point-max)) > (insert "(expand " ?\" def2expand ?\" " " fnum ")") > (return-ilisp))))) > >@@ -701,7 +701,7 @@ > (setq expr (buffer-substring start end)) > (if (not (y-or-n-p (concat "Typepred for " expr))) > (error "typepred aborted."))) >- (end-of-buffer) >+ (goto-char (point-max)) > (insert "(typepred " ?\" expr ?\" ")") > (return-ilisp))) > >@@ -767,7 +767,7 @@ > (if editprfwin > (set-window-point editprfwin (point)))) > (setq cmd (buffer-substring beg end)))) >- (end-of-buffer) >+ (goto-char (point-max)) > (insert cmd) > (return-ilisp) > (hilit-next-prover-command) >@@ -820,10 +820,10 @@ > (pvs-prover-goto-prev-step t)) > (hilit-next-prover-command) > (switch-to-buffer pvsbuf) >- (end-of-buffer) >+ (goto-char (point-max)) > (switch-to-buffer editprfbuf) > (pop-to-buffer pvsbuf) >- (end-of-buffer)))) >+ (goto-char (point-max))))) > > > ;;; pvs-prover-goto-next-step puts the cursor at the beginning of the next >diff -Naur pvs4.2-orig/emacs/emacs-src/pvs-tcl.el pvs4.2-sbcl/emacs/emacs-src/pvs-tcl.el >--- pvs4.2-orig/emacs/emacs-src/pvs-tcl.el 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/emacs/emacs-src/pvs-tcl.el 2009-03-24 18:56:17.000000000 +0000 >@@ -94,7 +94,7 @@ > "PVS Error")) > (t (comint-display-output > (format "PVS was developed and tested for %s versions %s,\nbut you are using version %s.\nThis is unlikely to cause problems, as it is a later release." >- program-name expected version program-name) >+ program-name expected version) > "PVS Warning")))))) > > (defun pvs-parse-version-numbers (vnum) >diff -Naur pvs4.2-orig/emacs/emacs-src/pvs-utils.el pvs4.2-sbcl/emacs/emacs-src/pvs-utils.el >--- pvs4.2-orig/emacs/emacs-src/pvs-utils.el 2008-07-18 04:39:20.000000000 +0000 >+++ pvs4.2-sbcl/emacs/emacs-src/pvs-utils.el 2009-03-24 18:56:17.000000000 +0000 >@@ -238,7 +238,7 @@ > nil nil 'list))) > (when fandp > (cond ((not (file-exists-p (car fandp))) >- (error "Theory ~a was in ~a which no longer exists" >+ (error "Theory %s was in %s which no longer exists" > theoryname (car fandp))) > ((or (null (cdr fandp)) > (buffer-modified-p (find-file-noselect (car fandp)))) >@@ -990,13 +990,6 @@ > (error "Must specify a theory name") > (list theory)))))) > >-(defun remove-duplicates (list) >- (let ((nlist nil)) >- (dolist (e list) >- (unless (member-equal e nlist) >- (push e nlist))) >- (nreverse nlist))) >- > (defun current-theory () > (let ((file (current-pvs-file t))) > (if file >@@ -1235,13 +1228,6 @@ > (or (car (get cmd 'abbreviations)) > cmd)) > >-(defun remove-if (pred list) >- (let ((nlist nil)) >- (dolist (e list) >- (unless (funcall pred e) >- (push e nlist))) >- (nreverse nlist))) >- > (defun add-final-newline () > (save-excursion > (unless (equal (char-after (1- (point-max))) ?\n) >@@ -1355,9 +1341,14 @@ > (setq pvs-reserved-words-regexp > "\\bassuming\\b\\|\\baxiom\\b\\|\\baccept\\b\\|\\bchanges\\b\\|\\ball\\b\\|\\band\\b\\|\\barray\\b\\|\\bbegin\\b\\|\\bby\\b\\|\\bcase\\b\\|\\bdeclare\\b\\|\\bdefinition\\b\\|\\belse\\b\\|\\belsif\\b\\|\\bendif\\b\\|\\bendassuming\\b\\|\\bendcase\\b\\|\\bend\\b\\|\\bexists\\b\\|\\bexporting\\b\\|\\bexit\\b\\|\\bforall\\b\\|\\bfunction\\b\\|\\bformula\\b\\|\\bfrom\\b\\|\\bif\\b\\|\\biff\\b\\|\\bimplies\\b\\|\\bimporting\\b\\|\\bin\\b\\|\\bis\\b\\|\\blambda\\b\\|\\blemma\\b\\|\\bloop\\b\\|\\bmapping\\b\\|\\bmeasure\\b\\|\\bmodule\\b\\|\\bnot\\b\\|\\bnothing\\b\\|\\bof\\b\\|\\bonto\\b\\|\\bobligation\\b\\|\\bopspec\\b\\|\\bor\\b\\|\\bproof\\b\\|\\bprove\\b\\|\\brecursive\\b\\|\\bresult\\b\\|\\btheorem\\b\\|\\btheory\\b\\|\\busing\\b\\|\\bvar\\b\\|\\bvariable\\b\\|\\brecord\\b\\|\\bverify\\b\\|\\bwhere\\b\\|\\bthen\\b\\|\\btype\\b\\|\\bwhen\\b\\|\\bwhile\\b\\|\\bwith\\b\\|\\blet\\b\\|\\bsetvariable\\b\\|\\[#\\|#\\]\\|[(]#\\|#[)]") > >+(defmacro pvs-find-face (name) >+ (if (featurep 'xemacs) >+ `(find-face ,name) >+ `(facep ,name))) >+ > (defun highlight-pvs () > (interactive) >- (unless (internal-find-face 'pvs-keyword) >+ (unless (pvs-find-face 'pvs-keyword) > (make-face 'pvs-keyword) > (set-face-foreground 'pvs-keyword "Blue") > (set-face-font 'pvs-keyword "*courier-bold-r-normal--12*")) >@@ -1575,7 +1566,7 @@ > (defvar pvs-unexpected-output nil) > > (defmacro pvs-validate (file directory &rest body) >- (` (let* ((logfile (concat default-directory (, file)))) >+ `(let* ((logfile (concat default-directory ,file))) > (pvs-backup-logfile logfile) > (let ((logbuf (find-file-noselect logfile t))) > (unwind-protect >@@ -1592,9 +1583,9 @@ > (default-directory default-directory)) > (pvs-message (pvs-version-string)) > (let ((pvs-disable-messages nil)) >- (change-context (, directory))) >+ (change-context ,directory)) > (condition-case err >- (progn (,@ body)) >+ (progn ,@body) > (error (pvs-message "ERROR: Emacs: %s %s" > (car err) (cdr err))))) > (pvs-wait-for-it) >@@ -1659,7 +1650,7 @@ > (pvs-message "NO BASELINE - using this run to create baseline.log") > (copy-file (buffer-file-name) "baseline.log")))) > (fset 'pvs-handler 'pvs-handler-orig) >- (fset 'ask-user-about-lock 'ask-user-about-lock-orig)))))) >+ (fset 'ask-user-about-lock 'ask-user-about-lock-orig))))) > > > ;;; This function provides the most basic form of test, removing bin >diff -Naur pvs4.2-orig/emacs/go-pvs.el pvs4.2-sbcl/emacs/go-pvs.el >--- pvs4.2-orig/emacs/go-pvs.el 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/emacs/go-pvs.el 2009-03-24 18:56:17.000000000 +0000 >@@ -24,6 +24,7 @@ > ;; -------------------------------------------------------------------- > > (setq debug-on-error t) >+(setq inhibit-startup-screen t) > > (defconst pvs-emacs-system > (cond ((or (string-match "XEmacs 21" (emacs-version)) >diff -Naur pvs4.2-orig/ess/box-defs.lisp pvs4.2-sbcl/ess/box-defs.lisp >--- pvs4.2-orig/ess/box-defs.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/box-defs.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -15,8 +15,8 @@ > ;;; Frank Pfenning (fp@cs.cmu.edu) ;;; > ;;; ******************************************************************* ;;; > >-(in-package :tools #+sbcl (:use :common-lisp :ergolisp)) >-#-sbcl (use-package :ergolisp) >+(in-package :tools) >+(use-package :ergolisp) > > (export '(*plain-readtable*)) > >diff -Naur pvs4.2-orig/ess/lang/ab-term/rel/af-dependency.lisp pvs4.2-sbcl/ess/lang/ab-term/rel/af-dependency.lisp >--- pvs4.2-orig/ess/lang/ab-term/rel/af-dependency.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/ab-term/rel/af-dependency.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -24,7 +24,7 @@ > ;;; 07-17-86 rln Initial development and release > ;;; 07-22-87 rln Reimplementation > >-(in-package 'analysis-facility) >+(in-package :analysis-facility) > (use-package '("AF-RUNTIME-LIB")) > > ;;; The variable *CODE* accumulates the code descriptors generated by SCHEDULE. >diff -Naur pvs4.2-orig/ess/lang/ab-term/rel/af-runtime.lisp pvs4.2-sbcl/ess/lang/ab-term/rel/af-runtime.lisp >--- pvs4.2-orig/ess/lang/ab-term/rel/af-runtime.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/ab-term/rel/af-runtime.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -25,7 +25,12 @@ > ;;; 07-22-87 rln Initial development release. > ;;; > >-(in-package "AF-RUNTIME-LIB" :nicknames '(abrt afrt)) >+(eval-when (compile load eval) >+ (unless (find-package "AF-RUNTIME-LIB") >+ (make-package "AF-RUNTIME-LIB" >+ :nicknames '("ABRT" "AFRT") >+ :use '("COMMON-LISP")))) >+(in-package "AF-RUNTIME-LIB") > > (export '(opcase argcase rt-delta-error rt-term-argn rt-term-args > rt-symbol rt-ite rt-opt rt-function rt-ast >diff -Naur pvs4.2-orig/ess/lang/ab-term/rel/af-structs.lisp pvs4.2-sbcl/ess/lang/ab-term/rel/af-structs.lisp >--- pvs4.2-orig/ess/lang/ab-term/rel/af-structs.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/ab-term/rel/af-structs.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -23,7 +23,7 @@ > ;;; > ;;; 07-22-87 rln Initial development and release. > >-(in-package 'analysis-facility) >+(in-package :analysis-facility) > > ;;; A DP-EVAL structure describes an attribute which is defined by an expression. > ;;; An expression always defines exactly one attribute. >diff -Naur pvs4.2-orig/ess/lang/ab-term/rel/af-top.lisp pvs4.2-sbcl/ess/lang/ab-term/rel/af-top.lisp >--- pvs4.2-orig/ess/lang/ab-term/rel/af-top.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/ab-term/rel/af-top.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -29,7 +29,7 @@ > ;;; 07-22-87 rln Initial development release. > > >-(in-package 'analysis-facility :nicknames '(ab af)) >+(in-package :analysis-facility) > > (export '(ab ab-make help)) > >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/access-par.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/access-par.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/access-par.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/access-par.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -21,7 +21,7 @@ > ;;; Revised Scott Dietzen, Mon Oct 13 15:32:09 1986 > > >-(in-package 'syntax-box) (use-package :ergolisp) >+(in-package :syntax-box) (use-package :ergolisp) > > > >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/aux-funs.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/aux-funs.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/aux-funs.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/aux-funs.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -17,7 +17,7 @@ > ;;; Scott Dietzen, Mon Oct 13 16:05:43 1986 > > >-(in-package 'syntax-box) (use-package :ergolisp) >+(in-package :syntax-box) (use-package :ergolisp) > > > (defparameter *sb-package* (find-package :sb)) >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/collapse.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/collapse.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/collapse.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/collapse.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -16,7 +16,7 @@ > > ;;;; Basic Function: Collapse fragments into lisp functions > >-(in-package 'syntax-box) (use-package :ergolisp) >+(in-package :syntax-box) (use-package :ergolisp) > > > ; The purpose of collapse is to take the fragments produced by process-grammar >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/flatten.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/flatten.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/flatten.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/flatten.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -17,7 +17,7 @@ > > ;;;; Basic Function: Flatten Patterns > >-(in-package 'syntax-box) (use-package :ergolisp) >+(in-package :syntax-box) (use-package :ergolisp) > > > >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/inter-phase.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/inter-phase.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/inter-phase.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/inter-phase.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -16,8 +16,8 @@ > > ;;; Intermediate Phase. > >-(in-package 'syntax-box) (use-package :ergolisp) >-(use-package '(sb-runtime)) >+(in-package :syntax-box) (use-package :ergolisp) >+(use-package :sb-runtime) > > ;;; Understanding of the internal grammar term structure is essential to > ;;; understanding this code (see documentation in access.lisp). @@@ >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/lexer-gen.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/lexer-gen.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/lexer-gen.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/lexer-gen.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -31,7 +31,7 @@ > ;;; (Routines check-comment-char(s)-with-op(S)) > > >-(in-package 'syntax-box) (use-package :ergolisp) >+(in-package :syntax-box) (use-package :ergolisp) > > > >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/look-ahead.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/look-ahead.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/look-ahead.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/look-ahead.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -9,9 +9,9 @@ > ;;; ******************************************************************* ;;; > > >-(in-package 'syntax-box) (use-package :ergolisp) >+(in-package :syntax-box) (use-package :ergolisp) > >-(use-package '(sb-runtime)) >+(use-package :sb-runtime) > > > >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/new-rt-format.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/new-rt-format.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/new-rt-format.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/new-rt-format.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -13,7 +13,7 @@ > > ;;; Scott Dietzen, Wed Aug 26 17:16:29 1987 > >-(in-package 'sb-runtime) (use-package :ergolisp) >+(in-package :sb-runtime) (use-package :ergolisp) > > (export '( > format-uterm >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/old-rt-format.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/old-rt-format.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/old-rt-format.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/old-rt-format.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -13,7 +13,7 @@ > > ;;; Scott Dietzen, Wed Aug 26 17:16:29 1987 > >-(in-package 'sb-runtime) (use-package :ergolisp) >+(in-package :sb-runtime) (use-package :ergolisp) > > (export '( > format-uterm >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/old-rt-unp-structs.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/old-rt-unp-structs.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/old-rt-unp-structs.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/old-rt-unp-structs.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -13,7 +13,7 @@ > > ;;; Scott Dietzen, Wed Aug 26 17:16:29 1987 > >-(in-package 'sb-runtime) (use-package :ergolisp) >+(in-package :sb-runtime) (use-package :ergolisp) > > (export '(token-p make-token token-kind token-subkind > token-value token-str-value >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/rt-lex.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/rt-lex.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/rt-lex.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/rt-lex.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -40,7 +40,7 @@ > )) > > >-(defconstant possible-single-char-operators >+(defconstant-if-unbound possible-single-char-operators > '(#\( #\) #\[ #\] #\{ #\} #\< #\> #\, #\; #\| #\^ #\# #\~ #\/ > #\! #\@ #\$ #\& #\_ #\- #\? #\% #\' #\: #\* #\+ #\` #\= #\\)) > >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/rt-term.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/rt-term.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/rt-term.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/rt-term.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -19,7 +19,7 @@ > > > >-(in-package "SB-RUNTIME" :nicknames '("RT-SB" "RTSB" "SB-RT" "SBRT")) >+(in-package "SB-RUNTIME") > (use-package :ergolisp) > > (use-package '("TERM" "OCC" "OPER")) >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/rt-unparse.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/rt-unparse.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/rt-unparse.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/rt-unparse.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -117,17 +117,17 @@ > > ;;; Just so we don't repeatedly cons identical tokens. > >-(defconstant ellipsis-token >+(defconstant-if-unbound ellipsis-token > (make-token :kind :lt :subkind :string :value "#")) >-(defconstant cr-token >+(defconstant-if-unbound cr-token > (make-token :kind :whitespace :subkind :cr)) >-(defconstant unindent-token >+(defconstant-if-unbound unindent-token > (make-token :kind :whitespace :subkind :unindent)) >-(defconstant tab-left-token >+(defconstant-if-unbound tab-left-token > (make-token :kind :whitespace :subkind :tab-left)) >-(defconstant tab-right-token >+(defconstant-if-unbound tab-right-token > (make-token :kind :whitespace :subkind :tab-right)) >-(defconstant untab-token >+(defconstant-if-unbound untab-token > (make-token :kind :whitespace :subkind :untab)) > > >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/rt-unp-attr.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/rt-unp-attr.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/rt-unp-attr.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/rt-unp-attr.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -13,7 +13,7 @@ > > ;;; Scott Dietzen, Tue Oct 6 15:32:22 1987 > >-(in-package 'sb-runtime) (use-package :ergolisp) >+(in-package "SB-RUNTIME") (use-package :ergolisp) > > > ;;; The following is a hack to avoid the problems inherent in the circularity >@@ -42,38 +42,6 @@ > > > >-(defun memo-uterm (term unp-function &key (top-level? nil)) >- (if (or *disable-caching* >- (and *disable-nested-caching* >- (null top-level?))) >- (funcall unp-function term) >- (newattr::get-gsyn theuterm >- term >- (list unp-function >- *unparse-style* >- *no-escapes* >- *sb-print-depth* >- *sb-print-length* >- *formatting-off*)))) >- >- >-(defun memo-aw (uterm width indent-unit-width fontwidth fontheight) >- (if *disable-caching* >- (let* ((aw (make-aw :uterm uterm >- :indent-unit-width indent-unit-width))) >- (format-aw uterm aw width)) >- (newattr::get-gsyn theaw >- (uterm-term uterm) >- (list uterm >- width >- indent-unit-width >- fontwidth >- fontheight)))) >- >- >- >- >- > (newattr::defgcon uterm-args) > (newattr::defgsyn theuterm uterm-args) > >@@ -105,3 +73,33 @@ > :indent-unit-width indent-unit-width))) > (format-aw uterm aw width)))) > >+ >+ >+ >+(defun memo-uterm (term unp-function &key (top-level? nil)) >+ (if (or *disable-caching* >+ (and *disable-nested-caching* >+ (null top-level?))) >+ (funcall unp-function term) >+ (newattr::get-gsyn theuterm >+ term >+ (list unp-function >+ *unparse-style* >+ *no-escapes* >+ *sb-print-depth* >+ *sb-print-length* >+ *formatting-off*)))) >+ >+ >+(defun memo-aw (uterm width indent-unit-width fontwidth fontheight) >+ (if *disable-caching* >+ (let* ((aw (make-aw :uterm uterm >+ :indent-unit-width indent-unit-width))) >+ (format-aw uterm aw width)) >+ (newattr::get-gsyn theaw >+ (uterm-term uterm) >+ (list uterm >+ width >+ indent-unit-width >+ fontwidth >+ fontheight)))) >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/rt-unp-structs.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/rt-unp-structs.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/rt-unp-structs.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/rt-unp-structs.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -13,7 +13,7 @@ > > ;;; Scott Dietzen, Wed Aug 26 17:16:29 1987 > >-(in-package 'sb-runtime) (use-package :ergolisp) >+(in-package "SB-RUNTIME") (use-package :ergolisp) > > (export '(token-p make-token token-kind token-subkind > token-value token-str-value >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/sbrt-lang-def.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/sbrt-lang-def.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/sbrt-lang-def.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/sbrt-lang-def.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -2,7 +2,9 @@ > ;;; package SB-RUNTIME is seen. fp, Mon Jan 2 11:07:17 1989. > #-gcl > (defpackage :sb-runtime >- #+sbcl (:use :common-lisp :ergolisp :oper :occ :term :sort :lang)) >+ #+sbcl (:nicknames "RT-SB" "RTSB" "SB-RT" "SBRT") >+ #+sbcl (:use :common-lisp :ergolisp :oper :occ :term :sort :lang) >+ #+sbcl (:shadowing-import-from :sb-int memq)) > (in-package :sb-runtime) > #-sbcl (use-package :ergolisp) > #-sbcl (use-package '(:oper :occ :term :sort :lang)) >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/top.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/top.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/top.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/top.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -25,7 +25,7 @@ > ;;; Added calls to preprocessing phase. > > >-(in-package 'syntax-box) (use-package :ergolisp) >+(in-package :syntax-box) (use-package :ergolisp) > > (export '(sb sb-make)) > >diff -Naur pvs4.2-orig/ess/lang/sb-term/rel/unp-code-revise.lisp pvs4.2-sbcl/ess/lang/sb-term/rel/unp-code-revise.lisp >--- pvs4.2-orig/ess/lang/sb-term/rel/unp-code-revise.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/lang/sb-term/rel/unp-code-revise.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -14,7 +14,7 @@ > ;;; This code modifies unparser generator code. > ;;; Scott Dietzen, Wed Nov 11 15:38:39 1987 > >-(in-package 'SB) (use-package :ergolisp) >+(in-package :SB) (use-package :ergolisp) > > > (defun unp-code-revision (routines) >diff -Naur pvs4.2-orig/ess/sys/ergolisp/rel/dlambda.lisp pvs4.2-sbcl/ess/sys/ergolisp/rel/dlambda.lisp >--- pvs4.2-orig/ess/sys/ergolisp/rel/dlambda.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/sys/ergolisp/rel/dlambda.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -26,7 +26,7 @@ > ;; This is a macro so that setf will work for declare-constructor > `(gethash ,constr *constructors-table* :no-info)) > >-(defconstant *reserved-constrs* '(:as) >+(defconstant-if-unbound *reserved-constrs* '(:as) > "List of symbols that may not be used as constructors.") > > (defmacro defreconstr (constr argcnt &key equal) >diff -Naur pvs4.2-orig/ess/sys/tools/rel/box-system.lisp pvs4.2-sbcl/ess/sys/tools/rel/box-system.lisp >--- pvs4.2-orig/ess/sys/tools/rel/box-system.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/sys/tools/rel/box-system.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -190,15 +190,11 @@ > (when lisp-compiler > (when boot > (load source-file)) >- (if readtable >- (let ((*readtable* readtable)) >- (compile-file source-file :output-file compiled-file >- #+(or lucid allegro) :messages #+(or lucid allegro) messages >- #+(or cmu sbcl) :progress #+(or cmu sbcl) messages >- )) >+ (let ((*readtable* (if readtable readtable *readtable*)) >+ #+sbcl (*compiler-progress* messages)) > (compile-file source-file :output-file compiled-file > #+(or lucid allegro) :messages #+(or lucid allegro) messages >- #+(or cmu sbcl) :progress #+(or cmu sbcl) messages >+ #+cmu :progress #+cmu messages > )) > ) > ;; #+kcl (rename-file (merge-pathnames ".o" source-file) compiled-file) >@@ -249,6 +245,8 @@ > (multiple-value-bind (junk1 junk2 result junk4) > (run-program "cc" :arguments arguments) > result) >+ #+sbcl >+ (sb-ext:process-exit-code (sb-ext:run-program "cc" arguments)) > #+allegro > (excl:run-shell-command > (format nil "cc ~{ ~a~}" arguments)))) >@@ -390,8 +388,8 @@ > ;;; all source files are .lisp, so we need only one set. > ;;; Recommend not changing the source extension. -fp > >-(defconstant *lisp-source-extension* "lisp") >-(defconstant *lisp-compiled-extension* >+(defconstant-if-unbound *lisp-source-extension* "lisp") >+(defconstant-if-unbound *lisp-compiled-extension* > #+(and allegro sparc) "fasl" ; Sun4 > #+(and allegro rios) "rfasl" ; PowerPC/RS6000 > #+(and allegro hpux) "hfasl" ; HP 9000 >@@ -421,14 +419,14 @@ > for this implementation of Lisp in the file sys/tools/rel/box-system.lisp. > Right now it is assumed to be \"bin\".") > >-(defconstant *lisp-source-suffix-string* >+(defconstant-if-unbound *lisp-source-suffix-string* > (concatenate 'string "." *lisp-source-extension*)) > >-(defconstant *lisp-compiled-suffix-string* >+(defconstant-if-unbound *lisp-compiled-suffix-string* > (concatenate 'string "." *lisp-compiled-extension*)) > >-(defconstant *lisp-source-extension-pathname* >+(defconstant-if-unbound *lisp-source-extension-pathname* > (make-pathname :type *lisp-source-extension*)) > >-(defconstant *lisp-compiled-extension-pathname* >+(defconstant-if-unbound *lisp-compiled-extension-pathname* > (make-pathname :type *lisp-compiled-extension*)) >diff -Naur pvs4.2-orig/ess/sys/tools/rel/print-utils.lisp pvs4.2-sbcl/ess/sys/tools/rel/print-utils.lisp >--- pvs4.2-orig/ess/sys/tools/rel/print-utils.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/sys/tools/rel/print-utils.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -8,6 +8,7 @@ > (defpackage :print-utils #+sbcl (:use :common-lisp :ergolisp)) > (in-package :print-utils) #-sbcl (use-package :ergolisp) > >+#-sbcl > (export '(lisp::print-struct lisp::writing-readably) > :lisp) > (export '(print-struct writing-readably)) >diff -Naur pvs4.2-orig/ess/sys/tools/rel/regression-test.lisp pvs4.2-sbcl/ess/sys/tools/rel/regression-test.lisp >--- pvs4.2-orig/ess/sys/tools/rel/regression-test.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/sys/tools/rel/regression-test.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -19,8 +19,8 @@ > (defvar *regression-testing-p* nil) > > (defun regression-test (&key (name "Anonymous test") >- form (form-predicate #'identity) script endp) >- (declare (special name script endp)) >+ form (form-predicate #'identity) script donep) >+ (declare (special name script donep)) > (let ((*regression-testing-p* t)) > (catch 'script-ended > (let ((formval (if (functionp form) (funcall form) (eval form)))) >@@ -43,13 +43,13 @@ > (cadr (car script))) > > (defun move-script () >- (declare (special name script endp)) >+ (declare (special name script donep)) > (when (null script) >- (if endp >+ (if donep > (throw 'script-ended nil) > (error "Regression test ~s fell off of end of script." name))) > (pop script) >- (when (and (null script) endp) (throw 'script-ended nil)) >+ (when (and (null script) donep) (throw 'script-ended nil)) > (values)) > > (defmacro regression-test-only (key &body body) >@@ -164,7 +164,7 @@ > :name "Regressible-error should succeed." > :form '(regressible-error :test "Error message ~s." 'foo) > :script '((:test "Error message FOO.")) >- :endp t) >+ :donep t) > > #+regression > (regression-test >diff -Naur pvs4.2-orig/ess/term/language/rel/languages.lisp pvs4.2-sbcl/ess/term/language/rel/languages.lisp >--- pvs4.2-orig/ess/term/language/rel/languages.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/term/language/rel/languages.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -85,18 +85,18 @@ > > > >-(defconstant standard-use-packages >+(defconstant-if-unbound standard-use-packages > '("ERGOLISP" "OPER" "OCC" "TERM" "SORT" "SB-RUNTIME" "LANG" "NEWATTR") > "The standard packages used by SB output files.") > >-(defconstant standard-use-languages >+(defconstant-if-unbound standard-use-languages > '("LEXICAL-TERMINALS") > "The standard languages used by SB output files.") > > >-(defconstant gen-src-file-ext "lisp") >+(defconstant-if-unbound gen-src-file-ext "lisp") > >-(defconstant per-gen-src-file-ext >+(defconstant-if-unbound per-gen-src-file-ext > (concatenate 'string "." gen-src-file-ext)) > > >diff -Naur pvs4.2-orig/ess/term/trep/rel/attr-prims.lisp pvs4.2-sbcl/ess/term/trep/rel/attr-prims.lisp >--- pvs4.2-orig/ess/term/trep/rel/attr-prims.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/term/trep/rel/attr-prims.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -19,7 +19,11 @@ > ;;; features from the terms, so it is the default method for storing > ;;; attributes. > >-(in-package "TERM" :nicknames '("GTERM")) (use-package :ergolisp) >+(eval-when (compile load eval) >+ (unless (find-package "TERM") >+ (make-package "TERM" :nicknames '("GTERM") >+ :use '(:cl-user :common-lisp :ergolisp)))) >+(in-package "TERM") > > (export '(attr-clear-one attr-clear-all)) > >diff -Naur pvs4.2-orig/ess/term/trep/rel/gterm.lisp pvs4.2-sbcl/ess/term/trep/rel/gterm.lisp >--- pvs4.2-orig/ess/term/trep/rel/gterm.lisp 2007-07-02 20:07:41.000000000 +0000 >+++ pvs4.2-sbcl/ess/term/trep/rel/gterm.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -29,7 +29,11 @@ > ;;; instead of a real operator. > ;;; > >-(in-package :term :nicknames '(:gterm)) (use-package :ergolisp) >+(eval-when (compile load eval) >+ (unless (find-package "TERM") >+ (make-package "TERM" :nicknames '("GTERM") >+ :use '(:cl-user :common-lisp :ergolisp)))) >+(in-package "TERM") > > (export '(term termp mk-term ds-term term-op term-args > term-attr set-term-attr)) >diff -Naur pvs4.2-orig/install-sh pvs4.2-sbcl/install-sh >--- pvs4.2-orig/install-sh 2007-07-02 20:07:43.000000000 +0000 >+++ pvs4.2-sbcl/install-sh 2009-03-24 18:56:17.000000000 +0000 >@@ -1,7 +1,7 @@ > #!/bin/sh > # install - install a program, script, or datafile > >-scriptversion=2005-11-07.23 >+scriptversion=2006-12-25.00 > > # This originates from X11R5 (mit/util/scripts/install.sh), which was > # later released in X11R6 (xc/config/util/install.sh) with the >@@ -39,52 +39,68 @@ > # when there is no Makefile. > # > # This script is compatible with the BSD install script, but was written >-# from scratch. It can only install one file at a time, a restriction >-# shared with many OS's install programs. >+# from scratch. >+ >+nl=' >+' >+IFS=" "" $nl" > > # set DOITPROG to echo to test this script > > # Don't use :- since 4.3BSD and earlier shells don't like it. >-doit="${DOITPROG-}" >+doit=${DOITPROG-} >+if test -z "$doit"; then >+ doit_exec=exec >+else >+ doit_exec=$doit >+fi > >-# put in absolute paths if you don't have them in your path; or use env. vars. >+# Put in absolute file names if you don't have them in your path; >+# or use environment vars. > >-mvprog="${MVPROG-mv}" >-cpprog="${CPPROG-cp}" >-chmodprog="${CHMODPROG-chmod}" >-chownprog="${CHOWNPROG-chown}" >-chgrpprog="${CHGRPPROG-chgrp}" >-stripprog="${STRIPPROG-strip}" >-rmprog="${RMPROG-rm}" >-mkdirprog="${MKDIRPROG-mkdir}" >+chgrpprog=${CHGRPPROG-chgrp} >+chmodprog=${CHMODPROG-chmod} >+chownprog=${CHOWNPROG-chown} >+cmpprog=${CMPPROG-cmp} >+cpprog=${CPPROG-cp} >+mkdirprog=${MKDIRPROG-mkdir} >+mvprog=${MVPROG-mv} >+rmprog=${RMPROG-rm} >+stripprog=${STRIPPROG-strip} >+ >+posix_glob='?' >+initialize_posix_glob=' >+ test "$posix_glob" != "?" || { >+ if (set -f) 2>/dev/null; then >+ posix_glob= >+ else >+ posix_glob=: >+ fi >+ } >+' > >-posix_glob= > posix_mkdir= > >-# Symbolic mode for testing mkdir with directories. >-# It is the same as 755, but also tests that "u+" works. >-test_mode=u=rwx,g=rx,o=rx,u+wx >- > # Desired mode of installed file. > mode=0755 > >-# Desired mode of newly created intermediate directories. >-# It is empty if not known yet. >-intermediate_mode= >- >+chgrpcmd= > chmodcmd=$chmodprog > chowncmd= >-chgrpcmd= >-stripcmd= >+mvcmd=$mvprog > rmcmd="$rmprog -f" >-mvcmd="$mvprog" >+stripcmd= >+ > src= > dst= > dir_arg= >-dstarg= >+dst_arg= >+ >+copy_on_change=false > no_target_directory= > >-usage="Usage: $0 [OPTION]... [-T] SRCFILE DSTFILE >+usage="\ >+Usage: $0 [OPTION]... [-T] SRCFILE DSTFILE > or: $0 [OPTION]... SRCFILES... DIRECTORY > or: $0 [OPTION]... -t DIRECTORY SRCFILES... > or: $0 [OPTION]... -d DIRECTORIES... >@@ -94,81 +110,86 @@ > In the 4th, create DIRECTORIES. > > Options: >--c (ignored) >--d create directories instead of installing files. >--g GROUP $chgrpprog installed files to GROUP. >--m MODE $chmodprog installed files to MODE. >--o USER $chownprog installed files to USER. >--s $stripprog installed files. >--t DIRECTORY install into DIRECTORY. >--T report an error if DSTFILE is a directory. >---help display this help and exit. >---version display version info and exit. >+ --help display this help and exit. >+ --version display version info and exit. >+ >+ -c (ignored) >+ -C install only if different (preserve the last data modification time) >+ -d create directories instead of installing files. >+ -g GROUP $chgrpprog installed files to GROUP. >+ -m MODE $chmodprog installed files to MODE. >+ -o USER $chownprog installed files to USER. >+ -s $stripprog installed files. >+ -t DIRECTORY install into DIRECTORY. >+ -T report an error if DSTFILE is a directory. > > Environment variables override the default commands: >- CHGRPPROG CHMODPROG CHOWNPROG CPPROG MKDIRPROG MVPROG RMPROG STRIPPROG >+ CHGRPPROG CHMODPROG CHOWNPROG CMPPROG CPPROG MKDIRPROG MVPROG >+ RMPROG STRIPPROG > " > >-while test -n "$1"; do >+while test $# -ne 0; do > case $1 in >- -c) shift >- continue;; >+ -c) ;; > >- -d) dir_arg=true >- shift >- continue;; >+ -C) copy_on_change=true;; >+ >+ -d) dir_arg=true;; > > -g) chgrpcmd="$chgrpprog $2" >- shift >- shift >- continue;; >+ shift;; > > --help) echo "$usage"; exit $?;; > > -m) mode=$2 >- shift >- shift >- continue;; >+ case $mode in >+ *' '* | *' '* | *' >+'* | *'*'* | *'?'* | *'['*) >+ echo "$0: invalid mode: $mode" >&2 >+ exit 1;; >+ esac >+ shift;; > > -o) chowncmd="$chownprog $2" >- shift >- shift >- continue;; >- >- -s) stripcmd=$stripprog >- shift >- continue;; >- >- -t) dstarg=$2 >- shift >- shift >- continue;; >- >- -T) no_target_directory=true >- shift >- continue;; >+ shift;; >+ >+ -s) stripcmd=$stripprog;; >+ >+ -t) dst_arg=$2 >+ shift;; >+ >+ -T) no_target_directory=true;; > > --version) echo "$0 $scriptversion"; exit $?;; > >- *) # When -d is used, all remaining arguments are directories to create. >- # When -t is used, the destination is already specified. >- test -n "$dir_arg$dstarg" && break >- # Otherwise, the last argument is the destination. Remove it from $@. >- for arg >- do >- if test -n "$dstarg"; then >- # $@ is not empty: it contains at least $arg. >- set fnord "$@" "$dstarg" >- shift # fnord >- fi >- shift # arg >- dstarg=$arg >- done >+ --) shift > break;; >+ >+ -*) echo "$0: invalid option: $1" >&2 >+ exit 1;; >+ >+ *) break;; > esac >+ shift > done > >-if test -z "$1"; then >+if test $# -ne 0 && test -z "$dir_arg$dst_arg"; then >+ # When -d is used, all remaining arguments are directories to create. >+ # When -t is used, the destination is already specified. >+ # Otherwise, the last argument is the destination. Remove it from $@. >+ for arg >+ do >+ if test -n "$dst_arg"; then >+ # $@ is not empty: it contains at least $arg. >+ set fnord "$@" "$dst_arg" >+ shift # fnord >+ fi >+ shift # arg >+ dst_arg=$arg >+ done >+fi >+ >+if test $# -eq 0; then > if test -z "$dir_arg"; then > echo "$0: no input file specified." >&2 > exit 1 >@@ -178,13 +199,38 @@ > exit 0 > fi > >-test -n "$dir_arg" || trap '(exit $?); exit' 1 2 13 15 >+if test -z "$dir_arg"; then >+ trap '(exit $?); exit' 1 2 13 15 >+ >+ # Set umask so as not to create temps with too-generous modes. >+ # However, 'strip' requires both read and write access to temps. >+ case $mode in >+ # Optimize common cases. >+ *644) cp_umask=133;; >+ *755) cp_umask=22;; >+ >+ *[0-7]) >+ if test -z "$stripcmd"; then >+ u_plus_rw= >+ else >+ u_plus_rw='% 200' >+ fi >+ cp_umask=`expr '(' 777 - $mode % 1000 ')' $u_plus_rw`;; >+ *) >+ if test -z "$stripcmd"; then >+ u_plus_rw= >+ else >+ u_plus_rw=,u+rw >+ fi >+ cp_umask=$mode$u_plus_rw;; >+ esac >+fi > > for src > do > # Protect names starting with `-'. > case $src in >- -*) src=./$src ;; >+ -*) src=./$src;; > esac > > if test -n "$dir_arg"; then >@@ -202,22 +248,22 @@ > exit 1 > fi > >- if test -z "$dstarg"; then >+ if test -z "$dst_arg"; then > echo "$0: no destination specified." >&2 > exit 1 > fi > >- dst=$dstarg >+ dst=$dst_arg > # Protect names starting with `-'. > case $dst in >- -*) dst=./$dst ;; >+ -*) dst=./$dst;; > esac > > # If destination is a directory, append the input filename; won't work > # if double slashes aren't ignored. > if test -d "$dst"; then > if test -n "$no_target_directory"; then >- echo "$0: $dstarg: Is a directory" >&2 >+ echo "$0: $dst_arg: Is a directory" >&2 > exit 1 > fi > dstdir=$dst >@@ -230,14 +276,25 @@ > expr X"$dst" : 'X\(.*[^/]\)//*[^/][^/]*/*$' \| \ > X"$dst" : 'X\(//\)[^/]' \| \ > X"$dst" : 'X\(//\)$' \| \ >- X"$dst" : 'X\(/\)' \| \ >- . : '\(.\)' 2>/dev/null || >+ X"$dst" : 'X\(/\)' \| . 2>/dev/null || > echo X"$dst" | >- sed '/^X\(.*[^/]\)\/\/*[^/][^/]*\/*$/{ s//\1/; q; } >- /^X\(\/\/\)[^/].*/{ s//\1/; q; } >- /^X\(\/\/\)$/{ s//\1/; q; } >- /^X\(\/\).*/{ s//\1/; q; } >- s/.*/./; q' >+ sed '/^X\(.*[^/]\)\/\/*[^/][^/]*\/*$/{ >+ s//\1/ >+ q >+ } >+ /^X\(\/\/\)[^/].*/{ >+ s//\1/ >+ q >+ } >+ /^X\(\/\/\)$/{ >+ s//\1/ >+ q >+ } >+ /^X\(\/\).*/{ >+ s//\1/ >+ q >+ } >+ s/.*/./; q' > ` > > test -d "$dstdir" >@@ -250,83 +307,131 @@ > if test $dstdir_status != 0; then > case $posix_mkdir in > '') >- posix_mkdir=false >- if $mkdirprog -m $test_mode -p -- / >/dev/null 2>&1; then >- posix_mkdir=true >- else >- # Remove any dirs left behind by ancient mkdir implementations. >- rmdir ./-m "$test_mode" ./-p ./-- 2>/dev/null >- fi ;; >- esac >- >- if >- $posix_mkdir && { >+ # Create intermediate dirs using mode 755 as modified by the umask. >+ # This is like FreeBSD 'install' as of 1997-10-28. >+ umask=`umask` >+ case $stripcmd.$umask in >+ # Optimize common cases. >+ *[2367][2367]) mkdir_umask=$umask;; >+ .*0[02][02] | .[02][02] | .[02]) mkdir_umask=22;; >+ >+ *[0-7]) >+ mkdir_umask=`expr $umask + 22 \ >+ - $umask % 100 % 40 + $umask % 20 \ >+ - $umask % 10 % 4 + $umask % 2 >+ `;; >+ *) mkdir_umask=$umask,go-w;; >+ esac > > # With -d, create the new directory with the user-specified mode. >- # Otherwise, create it using the same intermediate mode that >- # mkdir -p would use when creating intermediate directories. >- # POSIX says that this mode is "$(umask -S),u+wx", so use that >- # if umask -S works. >- >+ # Otherwise, rely on $mkdir_umask. > if test -n "$dir_arg"; then >- mkdir_mode=$mode >+ mkdir_mode=-m$mode > else >- case $intermediate_mode in >- '') >- if umask_S=`(umask -S) 2>/dev/null`; then >- intermediate_mode=$umask_S,u+wx >- else >- intermediate_mode=$test_mode >- fi ;; >- esac >- mkdir_mode=$intermediate_mode >+ mkdir_mode= > fi > >- $mkdirprog -m "$mkdir_mode" -p -- "$dstdir" >- } >+ posix_mkdir=false >+ case $umask in >+ *[123567][0-7][0-7]) >+ # POSIX mkdir -p sets u+wx bits regardless of umask, which >+ # is incompatible with FreeBSD 'install' when (umask & 300) != 0. >+ ;; >+ *) >+ tmpdir=${TMPDIR-/tmp}/ins$RANDOM-$$ >+ trap 'ret=$?; rmdir "$tmpdir/d" "$tmpdir" 2>/dev/null; exit $ret' 0 >+ >+ if (umask $mkdir_umask && >+ exec $mkdirprog $mkdir_mode -p -- "$tmpdir/d") >/dev/null 2>&1 >+ then >+ if test -z "$dir_arg" || { >+ # Check for POSIX incompatibilities with -m. >+ # HP-UX 11.23 and IRIX 6.5 mkdir -m -p sets group- or >+ # other-writeable bit of parent directory when it shouldn't. >+ # FreeBSD 6.1 mkdir -m -p sets mode of existing directory. >+ ls_ld_tmpdir=`ls -ld "$tmpdir"` >+ case $ls_ld_tmpdir in >+ d????-?r-*) different_mode=700;; >+ d????-?--*) different_mode=755;; >+ *) false;; >+ esac && >+ $mkdirprog -m$different_mode -p -- "$tmpdir" && { >+ ls_ld_tmpdir_1=`ls -ld "$tmpdir"` >+ test "$ls_ld_tmpdir" = "$ls_ld_tmpdir_1" >+ } >+ } >+ then posix_mkdir=: >+ fi >+ rmdir "$tmpdir/d" "$tmpdir" >+ else >+ # Remove any dirs left behind by ancient mkdir implementations. >+ rmdir ./$mkdir_mode ./-p ./-- 2>/dev/null >+ fi >+ trap '' 0;; >+ esac;; >+ esac >+ >+ if >+ $posix_mkdir && ( >+ umask $mkdir_umask && >+ $doit_exec $mkdirprog $mkdir_mode -p -- "$dstdir" >+ ) > then : > else > >- # mkdir does not conform to POSIX, or it failed possibly due to >- # a race condition. Create the directory the slow way, step by >- # step, checking for races as we go. >+ # The umask is ridiculous, or mkdir does not conform to POSIX, >+ # or it failed possibly due to a race condition. Create the >+ # directory the slow way, step by step, checking for races as we go. > > case $dstdir in >- /*) pathcomp=/ ;; >- -*) pathcomp=./ ;; >- *) pathcomp= ;; >+ /*) prefix='/';; >+ -*) prefix='./';; >+ *) prefix='';; > esac > >- case $posix_glob in >- '') >- if (set -f) 2>/dev/null; then >- posix_glob=true >- else >- posix_glob=false >- fi ;; >- esac >+ eval "$initialize_posix_glob" > > oIFS=$IFS > IFS=/ >- $posix_glob && set -f >+ $posix_glob set -f > set fnord $dstdir > shift >- $posix_glob && set +f >+ $posix_glob set +f > IFS=$oIFS > >+ prefixes= >+ > for d > do >- test "x$d" = x && continue >+ test -z "$d" && continue > >- pathcomp=$pathcomp$d >- if test ! -d "$pathcomp"; then >- $mkdirprog "$pathcomp" >- # Don't fail if two instances are running concurrently. >- test -d "$pathcomp" || exit 1 >+ prefix=$prefix$d >+ if test -d "$prefix"; then >+ prefixes= >+ else >+ if $posix_mkdir; then >+ (umask=$mkdir_umask && >+ $doit_exec $mkdirprog $mkdir_mode -p -- "$dstdir") && break >+ # Don't fail if two instances are running concurrently. >+ test -d "$prefix" || exit 1 >+ else >+ case $prefix in >+ *\'*) qprefix=`echo "$prefix" | sed "s/'/'\\\\\\\\''/g"`;; >+ *) qprefix=$prefix;; >+ esac >+ prefixes="$prefixes '$qprefix'" >+ fi > fi >- pathcomp=$pathcomp/ >+ prefix=$prefix/ > done >- obsolete_mkdir_used=true >+ >+ if test -n "$prefixes"; then >+ # Don't fail if two instances are running concurrently. >+ (umask $mkdir_umask && >+ eval "\$doit_exec \$mkdirprog $prefixes") || >+ test -d "$dstdir" || exit 1 >+ obsolete_mkdir_used=true >+ fi > fi > fi > >@@ -334,7 +439,7 @@ > { test -z "$chowncmd" || $doit $chowncmd "$dst"; } && > { test -z "$chgrpcmd" || $doit $chgrpcmd "$dst"; } && > { test "$obsolete_mkdir_used$chowncmd$chgrpcmd" = false || >- test -z "$chmodcmd" || $doit $chmodcmd "$mode" "$dst"; } || exit 1 >+ test -z "$chmodcmd" || $doit $chmodcmd $mode "$dst"; } || exit 1 > else > > # Make a couple of temp file names in the proper directory. >@@ -345,7 +450,7 @@ > trap 'ret=$?; rm -f "$dsttmp" "$rmtmp" && exit $ret' 0 > > # Copy the file name to the temp name. >- $doit $cpprog "$src" "$dsttmp" && >+ (umask $cp_umask && $doit_exec $cpprog "$src" "$dsttmp") && > > # and set any options; do chmod last to preserve setuid bits. > # >@@ -353,41 +458,54 @@ > # ignore errors from any of these, just make sure not to ignore > # errors from the above "$doit $cpprog $src $dsttmp" command. > # >- { test -z "$chowncmd" || $doit $chowncmd "$dsttmp"; } \ >- && { test -z "$chgrpcmd" || $doit $chgrpcmd "$dsttmp"; } \ >- && { test -z "$stripcmd" || $doit $stripcmd "$dsttmp"; } \ >- && { test -z "$chmodcmd" || $doit $chmodcmd "$mode" "$dsttmp"; } && >- >- # Now rename the file to the real destination. >- { $doit $mvcmd -f "$dsttmp" "$dst" 2>/dev/null \ >- || { >- # The rename failed, perhaps because mv can't rename something else >- # to itself, or perhaps because mv is so ancient that it does not >- # support -f. >- >- # Now remove or move aside any old file at destination location. >- # We try this two ways since rm can't unlink itself on some >- # systems and the destination file might be busy for other >- # reasons. In this case, the final cleanup might fail but the new >- # file should still install successfully. >- { >- if test -f "$dst"; then >- $doit $rmcmd -f "$dst" 2>/dev/null \ >- || { $doit $mvcmd -f "$dst" "$rmtmp" 2>/dev/null \ >- && { $doit $rmcmd -f "$rmtmp" 2>/dev/null; :; }; }\ >- || { >- echo "$0: cannot unlink or rename $dst" >&2 >- (exit 1); exit 1 >- } >- else >- : >- fi >- } && >- >- # Now rename the file to the real destination. >- $doit $mvcmd "$dsttmp" "$dst" >- } >- } || exit 1 >+ { test -z "$chowncmd" || $doit $chowncmd "$dsttmp"; } && >+ { test -z "$chgrpcmd" || $doit $chgrpcmd "$dsttmp"; } && >+ { test -z "$stripcmd" || $doit $stripcmd "$dsttmp"; } && >+ { test -z "$chmodcmd" || $doit $chmodcmd $mode "$dsttmp"; } && >+ >+ # If -C, don't bother to copy if it wouldn't change the file. >+ if $copy_on_change && >+ old=`LC_ALL=C ls -dlL "$dst" 2>/dev/null` && >+ new=`LC_ALL=C ls -dlL "$dsttmp" 2>/dev/null` && >+ >+ eval "$initialize_posix_glob" && >+ $posix_glob set -f && >+ set X $old && old=:$2:$4:$5:$6 && >+ set X $new && new=:$2:$4:$5:$6 && >+ $posix_glob set +f && >+ >+ test "$old" = "$new" && >+ $cmpprog "$dst" "$dsttmp" >/dev/null 2>&1 >+ then >+ rm -f "$dsttmp" >+ else >+ # Rename the file to the real destination. >+ $doit $mvcmd -f "$dsttmp" "$dst" 2>/dev/null || >+ >+ # The rename failed, perhaps because mv can't rename something else >+ # to itself, or perhaps because mv is so ancient that it does not >+ # support -f. >+ { >+ # Now remove or move aside any old file at destination location. >+ # We try this two ways since rm can't unlink itself on some >+ # systems and the destination file might be busy for other >+ # reasons. In this case, the final cleanup might fail but the new >+ # file should still install successfully. >+ { >+ test ! -f "$dst" || >+ $doit $rmcmd -f "$dst" 2>/dev/null || >+ { $doit $mvcmd -f "$dst" "$rmtmp" 2>/dev/null && >+ { $doit $rmcmd -f "$rmtmp" 2>/dev/null; :; } >+ } || >+ { echo "$0: cannot unlink or rename $dst" >&2 >+ (exit 1); exit 1 >+ } >+ } && >+ >+ # Now rename the file to the real destination. >+ $doit $mvcmd "$dsttmp" "$dst" >+ } >+ fi || exit 1 > > trap '' 0 > fi >diff -Naur pvs4.2-orig/Makefile.in pvs4.2-sbcl/Makefile.in >--- pvs4.2-orig/Makefile.in 2009-03-24 18:55:34.000000000 +0000 >+++ pvs4.2-sbcl/Makefile.in 2009-03-24 18:56:17.000000000 +0000 >@@ -90,18 +90,18 @@ > endif > endif > >-# ifneq ($(SBCL_HOME),) >-# # Check that the given SBCL_HOME works >-# SBCLISPEXE = $(SBCL_HOME)/bin/lisp >-# ifeq ($(shell if [ -x "$(SBCLISPEXE)" ]; then echo OK; fi),OK) >-# SBCLVERSION = $(shell $(SBCL_HOME)/bin/lisp -batch -eval '(progn (format t "~a" (lisp-implementation-version)) (terpri) (quit))') >-# $(warning "SBCL Version $(SBCLVERSION)") >-# sbcl-devel += $(bindir)/devel/$(SYSTEM)-sbclisp >-# sbcl-rt += $(bindir)/runtime/$(SYSTEM)-sbclisp >-# else >-# $(error "$(SBCLISPEXE) is not executable") >-# endif >-# endif >+ifneq ($(SBCLISP_HOME),) >+# Check that the given SBCLISP_HOME works >+SBCLISPEXE = $(SBCLISP_HOME)/bin/sbcl >+ifeq ($(shell if [ -x "$(SBCLISPEXE)" ]; then echo OK; fi),OK) >+SBCLVERSION = $(shell $(SBCLISPEXE) --version) >+$(warning "$(SBCLVERSION)") >+sbcl-devel += $(bindir)/devel/$(SYSTEM)-sbclisp >+sbcl-rt += $(bindir)/runtime/$(SYSTEM)-sbclisp >+else >+$(error "$(SBCLISPEXE) is not executable") >+endif >+endif > > > LOAD-FOREIGN-EXTENSION=so >@@ -342,6 +342,7 @@ > src/tex-support.lisp \ > src/raw-api.lisp > >+sbcllisp += src/utils/file-utils-sbcl.lisp > cmulisp += src/utils/file-utils-cmu.lisp > allegrolisp += src/utils/file-utils.lisp > >@@ -372,6 +373,7 @@ > > bddlisp = BDD/bdd.lisp BDD/mu.lisp > allegrolisp += BDD/bdd-allegro.lisp BDD/mu-allegro.lisp >+sbcllisp += BDD/bdd-sbcl.lisp BDD/mu-sbcl.lisp > cmulisp += BDD/bdd-cmu.lisp BDD/mu-cmu.lisp > > PVSiolisp = src/PVSio/pvs-lib.lisp src/PVSio/defattach.lisp \ >@@ -423,6 +425,7 @@ > groundevallisp := $(patsubst %,$(PVSPATH)%,$(groundevallisp)) > inst-by-unif-lisp := $(patsubst %,$(PVSPATH)%,$(inst-by-unif-lisp)) > allegrolisp := $(patsubst %,$(PVSPATH)%,$(allegrolisp)) >+sbcllisp := $(patsubst %,$(PVSPATH)%,$(sbcllisp)) > cmulisp := $(patsubst %,$(PVSPATH)%,$(cmulisp)) > endif > >@@ -437,16 +440,16 @@ > .PHONY : all devel runtime parser emacs prelude-files-and-regions etags > > ifneq ($(buildcmds),) >-ifeq ($(CMULISP_HOME)$(ALLEGRO_HOME),) >-$(error "Must set CMULISP_HOME or ALLEGRO_HOME") >+ifeq ($(SBCLISP_HOME)$(CMULISP_HOME)$(ALLEGRO_HOME),) >+$(error "Must set SBCLISP_HOME, CMULISP_HOME, or ALLEGRO_HOME") > endif > endif > > all : devel runtime prelude-files-and-regions $(emacs-elc) etags > >-devel : $(allegro-devel) $(cmulisp-devel) >+devel : $(allegro-devel) $(sbcl-devel) $(cmulisp-devel) > >-runtime : $(allegro-rt) $(cmulisp-rt) >+runtime : $(allegro-rt) $(sbcl-rt) $(cmulisp-rt) > > parser : pvs-parser-out > >@@ -454,8 +457,8 @@ > > etags : $(PVSPATH)TAGS > >-$(PVSPATH)TAGS : $(lisp-files) $(allegrolisp) $(cmulisp) $(pvs-emacs-src) >- $(ETAGS) $(lisp-files) $(allegrolisp) $(cmulisp) $(pvs-emacs-src) >+$(PVSPATH)TAGS : $(lisp-files) $(allegrolisp) $(sbcllisp) $(cmulisp) $(pvs-emacs-src) >+ $(ETAGS) $(lisp-files) $(allegrolisp) $(sbcllisp) $(cmulisp) $(pvs-emacs-src) > > fileutils = \ > $(PVSPATH)src/utils/$(PLATFORM)/file_utils.$(LOAD-FOREIGN-EXTENSION) \ >@@ -472,6 +475,56 @@ > # Here are the rules for building the PVS grammar, pvs-methods file, and > # devel and runtime images. > >+ifneq ($(SBCLISP_HOME),) >+ >+ifeq ($(ALLEGRO_HOME),) # Build these with Allegro, if available >+$(PVSPATH)src/pvs-lexer.lisp : $(pvs-parser-in) >+ @echo "******* Creating parser" >+ $(SBCLISPEXE) --load src/make-pvs-parser >+ >+$(PVSPATH)src/pvs-methods.lisp : $(PVSPATH)src/make-pvs-methods.lisp \ >+ $(PVSPATH)src/defcl.lisp \ >+ $(PVSPATH)src/classes-expr.lisp \ >+ $(PVSPATH)src/classes-decl.lisp >+ @echo "******* Creating pvs-methods.lisp" >+ $(SBCLISPEXE) --eval "(defvar *pvs-path* \"$(PVSPATH)\")" \ >+ --load src/make-pvs-methods.lisp >+endif >+ >+$(sbcl-devel) $(sbcl-rt) : $(image-deps) \ >+ $(pvs-make-files) $(ess) $(ff-files) \ >+ $(lisp-files) $(sbcllisp) \ >+ $(PVSPATH)lib/prelude.pvs $(PVSPATH)lib/prelude.prf >+ $(MKDIR) -p $(subst $(SYSTEM)-sbclisp,,$@) >+ @echo "******* Compiling PVS files in Steel Bank Common Lisp (SBCL)" >+ $(SBCLISPEXE) --eval '(require :sb-posix)' \ >+ --eval '(require :sb-md5)' \ >+ --eval '(load "pvs.system" :verbose t)' \ >+ --eval "(let ((*load-pvs-prelude* nil)) \ >+ (mk:operate-on-system :pvs :compile))" \ >+ --eval '(quit)' >+ cp $(PVSPATH)src/utils/$(PLATFORM)/b64 $(bindir) >+ @echo "******* Building PVS image $@" >+ $(SBCLISPEXE) --eval '(require :sb-posix)' \ >+ --eval '(require :sb-md5)' \ >+ --eval '(load "pvs.system" :verbose t)' \ >+ --eval "(unwind-protect \ >+ (mk:operate-on-system :pvs :compile) \ >+ (save-lisp-and-die \"$@.core\" \ >+ :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,,$@) >+ cp $(PVSPATH)BDD/bdd-sbcl.lisp $(PVSPATH)BDD/mu-sbcl.lisp $(subst $(SYSTEM)-sbclisp,,$@) >+ cp $(PVSPATH)src/WS1S/$(PLATFORM)/ws1s.$(LOAD-FOREIGN-EXTENSION) $(subst $(SYSTEM)-sbclisp,,$@) >+ cp $(PVSPATH)src/WS1S/lisp/dfa-foreign-sbcl.lisp $(subst $(SYSTEM)-sbclisp,,$@) >+ cp $(PVSPATH)src/utils/$(PLATFORM)/b64 $(bindir) >+ echo "#!/bin/sh" > $@ >+ echo "sbcl --core \`dirname \$$0\`/\`basename \$$0\`.core \$$*" >> $@ >+ chmod a+x $@ >+endif >+ > ifneq ($(CMULISP_HOME),) > > ifeq ($(ALLEGRO_HOME),) # Build these with Allegro, if available >@@ -621,7 +674,7 @@ > > faslexts = fasl,rfasl,hfasl,lfasl,mfasl,nfasl,sbin,obin,rbin,mbin,x86f,ppcf,sparcf,x8664s,x86s,ppcs,sparcs,clfasl,wfasl,err > >-platforms = ix86-Linux,ix86-MacOSX,powerpc-MacOSX,powerpc-MacOSX,sun4-SunOS5 >+platforms = ix86-Linux,ix86_64-Linux,ix86-MacOSX,powerpc-MacOSX,powerpc-MacOSX,sun4-SunOS5 > # HT: Need to put a comma in a variable, because a literal > # comma cannot appear in a makefile function argument. > comma:= , >diff -Naur pvs4.2-orig/pvs-config.lisp pvs4.2-sbcl/pvs-config.lisp >--- pvs4.2-orig/pvs-config.lisp 2008-07-20 08:40:19.000000000 +0000 >+++ pvs4.2-sbcl/pvs-config.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -99,7 +99,7 @@ > > #+sbcl > (defun bye (&optional (exit-status 0)) >- (sb-unix:unix-exit exit-status)) >+ (quit :unix-status exit-status)) > > (defun pvs-version-and-quit () > (format t "PVS Version ~a" (eval (find-symbol (string :*pvs-version*) :pvs))) >diff -Naur pvs4.2-orig/pvs.in pvs4.2-sbcl/pvs.in >--- pvs4.2-orig/pvs.in 2008-07-20 08:48:14.000000000 +0000 >+++ pvs4.2-sbcl/pvs.in 2009-03-24 18:56:17.000000000 +0000 >@@ -11,7 +11,7 @@ > # -version | --version prints the PVS version > # -emacs emacsref emacs, xemacs, alias, or pathname > # -load-after efile loads emacs file name after PVS emacs files >-# -lisp name lisp image name - allegro or cmulisp >+# -lisp name lisp image name - allegro, cmulisp, or sbclisp > # -runtime use the runtime image (devel is default, if there) > # -decision-procedures set the default decision procedures (ics or shostak) > # -force-decision-procedures forces the decision procedures to be used >@@ -42,10 +42,10 @@ > # PVSVERBOSE - corresponds to the -v argument > # > # The following environment variables are used by PVS, and are set below: >-# PVSPATH pvs system path - this should not normally be set by the user >-# PVSARCH sun4 or ix86 >+# PVSPATH pvs system path - this should not normally be set by the user >+# PVSARCH sun4, ix86, ix86_64, or powerpc > # >-# The PVS binary paths are appended to the front of the PATH variable >+# The PVS binary paths are appended to the front of the PATH variable > # -------------------------------------------------------------------- > # PVS > # Copyright (C) 2006, SRI International. All Rights Reserved. >@@ -98,7 +98,8 @@ > case $2 in > allegro) PVSLISP=allegro;; > cmulisp) PVSLISP=cmulisp;; >- *) echo "Only allegro and cmulisp are currently available" >+ sbclisp) PVSLISP=sbclisp;; >+ *) echo "Only allegro, cmulisp, and sbclisp are currently available" > exit 1;; > esac > shift;; >@@ -170,7 +171,7 @@ > -version | --version show the PVS version number > -emacs emacsref emacs, xemacs, alias, or pathname > -load-after efile loads emacs file after PVS emacs files >- -lisp name lisp image name (allegro or cmulisp) >+ -lisp name lisp image name (allegro, cmulisp, or sbclisp) > -runtime use the runtime image > -decision-procedures set default decision procedures (ics or shostak) > -force-decision-procedures forces the decision procedures (ics or shostak) >@@ -198,13 +199,17 @@ > case $opsys in > SunOS) majvers=`uname -r | cut -d"." -f1` > if [ $majvers = 4 ] >- then echo "PVS 3.3 only runs under Mac OS X, Linux, FreeBSD, or Solaris"; exit 1 >+ then echo "PVS 4.2 only runs under Mac OS X, Linux, FreeBSD, or Solaris"; exit 1 > fi > PVSARCH=sun4;; > Linux) # If Linux, we need to determine the Redhat version to use. > opsys=Linux > majvers= >- PVSARCH=ix86 >+ case `uname -m` in >+ x86) PVSARCH=ix86 ;; >+ x86_64) PVSARCH=ix86_64 ;; >+ *) echo "PVS 4.2 only runs on Intel Linux"; exit 1 >+ esac > # Allegro does not work with Linux's New Posix Thread Library (NPTL) > # used in newer Red Hat kernels and 2.6 kernels. This will force > # the old thread-implementation. >@@ -215,7 +220,11 @@ > ;; > FreeBSD) opsys=Linux > majvers= >- PVSARCH=ix86 >+ case `uname -m` in >+ x86) PVSARCH=ix86 ;; >+ x86_64) PVSARCH=ix86_64 ;; >+ *) echo "PVS 4.2 only runs on Intel Linux"; exit 1 >+ esac > # Allegro does not work with Linux's New Posix Thread Library (NPTL) > # used in newer Red Hat kernels and 2.6 kernels. This will force > # the old thread-implementation. >@@ -233,13 +242,13 @@ > #majvers=`uname -r | cut -d"." -f1` > majvers= > ;; >- *) echo "PVS 3.3 only runs under Solaris, Linux, FreeBSD (linux-enabled), or Mac (Darwin 7.4)"; exit 1 >+ *) echo "PVS 4.2 only runs under Solaris, Linux, FreeBSD (linux-enabled), or Mac (Darwin 7.4)"; exit 1 > esac > > binpath=$PVSPATH/bin/$PVSARCH-$opsys${majvers} > >-if [ -n "$PVSLISP" -a "$PVSLISP" != "allegro" -a "$PVSLISP" != "cmulisp" ] >- then echo "ERROR: PVSLISP must be unset, or set to 'allegro' or 'cmulisp'" >+if [ -n "$PVSLISP" -a "$PVSLISP" != "allegro" -a "$PVSLISP" != "cmulisp" -a "$PVSLISP" != "sbclisp" ] >+ then echo "ERROR: PVSLISP must be unset, or set to 'allegro', 'cmulisp', or 'sbclisp'" > exit 1 > fi > >@@ -252,6 +261,10 @@ > then PVSLISP=cmulisp > elif [ -x $binpath/runtime/pvs-cmulisp ] > then PVSLISP=cmulisp >+ elif [ -x $binpath/devel/pvs-sbclisp ] >+ then PVSLISP=sbclisp >+ elif [ -x $binpath/runtime/pvs-sbclisp ] >+ then PVSLISP=sbclisp > else echo "No executable available in $binpath" > exit 1 > fi >@@ -292,6 +305,16 @@ > do flags="$flags -load $lf"; done > fi > ;; >+ sbclisp) >+ noinit="--noinform --no-userinit" >+ evalflag="--eval" >+ if [ -n "$lisploadfiles" ] >+ then >+ flags="$flags --eval (pvs::pvs-init)" >+ for lf in $lisploadfiles >+ do flags="$flags --load $lf"; done >+ fi >+ ;; > esac > > PVSPATCHLEVEL=${PVSPATCHLEVEL:-2} >diff -Naur pvs4.2-orig/pvsio.in pvs4.2-sbcl/pvsio.in >--- pvs4.2-orig/pvsio.in 2007-11-09 20:39:43.000000000 +0000 >+++ pvs4.2-sbcl/pvsio.in 2009-03-24 18:56:17.000000000 +0000 >@@ -22,7 +22,7 @@ > -T|--timing print timing information for each evaluation > -v|--version print PVSio version > -V|--verbose print typechecking information >- -l|--lisp PVS lisp version [allegro,cmulisp] >+ -l|--lisp PVS lisp version [allegro,cmulisp,sbclisp] > <file>@<theory>:<main> load <theory> from <file>.pvs, evaluate <main>, > and exit > >@@ -42,7 +42,8 @@ > case $2 in > allegro) PVSLISP='-lisp allegro';; > cmulisp) PVSLISP='-lisp cmulisp';; >- *) echo "Only allegro and cmulisp are currently available" >+ sbclisp) PVSLISP='-lisp sbclisp';; >+ *) echo "Only allegro, cmulisp, and sbclisp are currently available" > exit 1;; > esac > shift;; >diff -Naur pvs4.2-orig/pvs-sbcl.spec pvs4.2-sbcl/pvs-sbcl.spec >--- pvs4.2-orig/pvs-sbcl.spec 1970-01-01 00:00:00.000000000 +0000 >+++ pvs4.2-sbcl/pvs-sbcl.spec 2009-03-24 18:56:17.000000000 +0000 >@@ -0,0 +1,131 @@ >+Name: pvs-sbcl >+Version: 4.2 >+Release: 1%{?dist} >+Summary: The PVS Verification System, SBCL build >+ >+Group: Applications/Engineering >+License: GPLv2+ >+URL: http://pvs.csl.sri.com/ >+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 >+Patch0: pvs-4.2-sbcl.patch >+Patch1: pvs-4.2-unused.patch >+Patch2: pvs-4.2-64bit.patch >+Patch3: pvs-4.2-mona.patch >+Patch4: pvs-4.2-config.patch >+Patch5: pvs-4.2-typo.patch >+Patch6: pvs-4.2-emacs.patch >+Patch7: pvs-4.2-latex.patch >+BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n) >+ >+BuildRequires: sbcl, texinfo-tex, texlive-latex, emacs-el, xemacs-devel >+Requires: sbcl, texlive-latex >+Provides: pvs = %{version}-%{release}, pvsio = %{version}-%{release} >+ >+%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. PVS is a research >+prototype: it evolves and improves as we develop or apply new capabilities, >+and as the stress of real use exposes new requirements. >+ >+%prep >+%setup -q -c >+cp -p %{SOURCE1} %{SOURCE2} %{SOURCE3} %{SOURCE4} . >+ >+# Enable support for building PVS with sbcl >+%patch0 -p1 >+ >+# Get rid of an unused variable warning >+%patch1 -p1 >+ >+# Enable building on 64-bit platforms >+%patch2 -p1 >+ >+# Enable use of a system-installed Mona >+%patch3 -p1 >+ >+# Update config.sub and config.guess so they'll recognize amd64- systems >+%patch4 -p1 >+ >+# Fix a few typographical errors that result in miscompilations >+%patch5 -p1 >+ >+# Modernize the Emacs interface >+%patch6 -p1 >+ >+# Use the fancyhdr package instead of the obsolete fancyheadings package. >+# Also don't try to make Emacs kill an already dead process. >+%patch7 -p1 >+ >+%build >+./configure CFLAGS="$RPM_OPT_FLAGS -fPIC" >+make SBCLISP_HOME=/usr PVSPATH=`pwd`/ >+ >+# 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/language >+mv doc/language/language.pdf pvs-language-reference.pdf >+ >+make -C doc/prover >+mv doc/prover/prover.pdf pvs-prover-guide.pdf >+ >+rm -f doc/release-notes/pvs-release-notes.pdf >+make -C doc/release-notes pvs-release-notes.pdf >+ >+make -C doc/user-guide >+mv doc/user-guide/user-guide.pdf pvs-system-guide.pdf >+ >+# Mimic the effects of the relocate script for the installed location >+sed -i -e "s,^PVSPATH=.*$,PVSPATH=%{_datadir}/pvs," pvs >+sed -i -e "s,^PVSPATH=.*$,PVSPATH=%{_datadir}/pvs," pvsio >+ >+%install >+rm -rf $RPM_BUILD_ROOT >+mkdir -p $RPM_BUILD_ROOT%{_bindir} >+mkdir -p $RPM_BUILD_ROOT%{_datadir}/pvs/doc/release-notes >+mkdir -p $RPM_BUILD_ROOT%{_datadir}/texmf/tex/latex/pvs >+cp -a bin emacs lib pvs-tex.sub wish $RPM_BUILD_ROOT%{_datadir}/pvs >+cp -a doc/release-notes/pvs-release-notes.info $RPM_BUILD_ROOT%{_datadir}/pvs/doc/release-notes >+cp -a pvs.sty $RPM_BUILD_ROOT%{_datadir}/texmf/tex/latex/pvs >+cp -a pvs pvsio $RPM_BUILD_ROOT%{_bindir} >+ >+# We don't need the relocate script >+rm -f $RPM_BUILD_ROOT%{_datadir}/pvs/bin/relocate >+ >+%clean >+rm -rf $RPM_BUILD_ROOT >+ >+%post -p /usr/bin/mktexlsr >+ >+%postun -p /usr/bin/mktexlsr >+ >+%files >+%defattr(-,root,root,-) >+%doc *.pdf *.ps.gz LICENSE NOTICES README doc/PVSio-2.d.pdf Examples >+%{_bindir}/pvs* >+%{_datadir}/pvs >+%{_datadir}/texmf/tex/latex/pvs >+ >+%changelog >+* Fri Jan 23 2009 Jerry James <loganjerry@gmail.com> - 4.2-1 >+- Initial package, based on cmulisp package >diff -Naur pvs4.2-orig/pvs.system pvs4.2-sbcl/pvs.system >--- pvs4.2-orig/pvs.system 2007-09-20 05:19:31.000000000 +0000 >+++ pvs4.2-sbcl/pvs.system 2009-03-24 18:56:17.000000000 +0000 >@@ -25,6 +25,16 @@ > ;; Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. > ;; -------------------------------------------------------------------- > >+(in-package :common-lisp) >+ >+(#-(or cmu sbcl) progn >+ #+cmu ext:without-package-locks >+ #+sbcl sb-ext:without-package-locks >+ (defmacro defconstant-if-unbound (name value &optional doc) >+ `(defconstant ,name (if (boundp ',name) (symbol-value ',name) ,value) >+ ,@(when doc (list doc)))) >+ (export 'defconstant-if-unbound)) >+ > (in-package :cl-user) > > #+allegro >@@ -46,9 +56,11 @@ > #+sbcl > (defun startup-pvs () > (in-package :pvs) >- ;; Can't directly call (pvs::pvs-init) >- (apply (find-symbol (string :pvs-init) :pvs) nil) >- ) >+ ;; Turn off compiler warnings >+ (handler-bind ((sb-ext:compiler-note #'muffle-warning)) >+ ;; Can't directly call (pvs::pvs-init) >+ (apply (find-symbol (string :pvs-init) :pvs) nil) >+ (sb-impl::toplevel-init))) > > #+allegro > (eval-when (eval load) >@@ -59,12 +71,17 @@ > excl:*enclose-printer-errors* nil > *print-pretty* t)) > >+#+sbcl >+(eval-when (eval load) >+ (setq *compile-verbose* nil) >+ (setq *compile-print* nil)) >+ > (eval-when (eval load) > ;; This sets *pvs-path* and sets *pvs-binary-type* > (load "pvs-config.lisp") > #+allegro (chdir *pvs-path*)) > >-(defpackage :ilisp) >+(defpackage :ilisp (:nicknames :ILISP) (:use :common-lisp #+:CMU :conditions)) > (defpackage :bvec) > > (unless (find-package :make) >@@ -181,7 +198,11 @@ > (load (format nil "~a/src/xp" *pvs-path*)) > #+gcl > (load (format nil "~a/src/xp-code" *pvs-path*)) >- (apply (find-symbol :install :xp) :package :pvs nil)) >+ #-sbcl >+ (apply (find-symbol :install :xp) :package :pvs nil) >+ #+sbcl >+ (apply (find-symbol "INSTALL" (find-package :xp)) >+ :package :pvs nil)) > #-(or cmu sbcl) > (load (format nil "~a/ess/dist-ess.lisp" *pvs-path*)) > #-gcl >@@ -215,6 +236,7 @@ > (let* ((platform #+(and sun4 sunos4) "sun4-SunOS4" > #+(and sun4 (not sunos4)) "sun4-SunOS5" > #+(and x86 (not macosx)) "ix86-Linux" >+ #+(and x86-64 (not macosx)) "ix86_64-Linux" > #+(and macosx powerpc) "powerpc-MacOSX" > #+(and macosx x86) "ix86-MacOSX") > (utilpath (concatenate 'string >@@ -281,7 +303,9 @@ > :components ((:file "hashfn") > #+allegro > (:file "file-utils") >- #+(or cmu sbcl) >+ #+sbcl >+ (:file "file-utils-sbcl") >+ #+cmu > (:file "file-utils-cmu"))) > (:module language > :source-pathname "src/" >diff -Naur pvs4.2-orig/src/abstraction/abstract.lisp pvs4.2-sbcl/src/abstraction/abstract.lisp >--- pvs4.2-orig/src/abstraction/abstract.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/abstraction/abstract.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -27,7 +27,7 @@ > ;; Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. > ;; -------------------------------------------------------------------- > >-(in-package 'pvs) >+(in-package :pvs) > > > (defvar *abs-cache+* nil) >diff -Naur pvs4.2-orig/src/classes-decl.lisp pvs4.2-sbcl/src/classes-decl.lisp >--- pvs4.2-orig/src/classes-decl.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/classes-decl.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -141,7 +141,7 @@ > type-name type-name? type-value types update-expr using-hash > var-decl visible?)) > #+(or cmu sbcl) >-(ext:without-package-locks >+(#-sbcl ext:without-package-locks #+sbcl sb-ext:without-package-locks > (defgeneric class (x)) > (defgeneric (setf class) (x y)) > (defgeneric keyword (x)) >@@ -338,6 +338,9 @@ > ;;; unparser. The type is set by the typechecker to the canonical value > ;;; of the declared-type. > >+( >+ #-sbcl progn >+ #+sbcl sb-ext:without-package-locks > (defcl declaration (syntax) > (newline-comment :restore-as nil) > (id :type (or symbol number) :parse t :restore-as nil) >@@ -353,6 +356,7 @@ > (semi :parse t :restore-as nil) > (tcc-form :fetch-as nil :ignore t) > (typecheck-time :restore-as nil)) >+) > > ;;; declared-type-string keeps the string of the declared type for > ;;; creating the pvs context - see create-declaration-entry >diff -Naur pvs4.2-orig/src/classes-expr.lisp pvs4.2-sbcl/src/classes-expr.lisp >--- pvs4.2-orig/src/classes-expr.lisp 2007-10-11 00:11:41.000000000 +0000 >+++ pvs4.2-sbcl/src/classes-expr.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -35,7 +35,7 @@ > propositional-application)) > > #+(or cmu sbcl) >-(ext:without-package-locks >+(#-sbcl ext:without-package-locks #+sbcl sb-ext:without-package-locks > (defgeneric type (x)) > (defgeneric (setf type) (x y)) > (defgeneric number (x)) >@@ -45,7 +45,7 @@ > > #+(or cmu sbcl) > ;; This is actually defined in utils, but convenient to add here >-(ext:without-package-locks >+(#-sbcl ext:without-package-locks #+sbcl sb-ext:without-package-locks > (defgeneric condition (x))) > > ;;; Provide a class on which to hang syntactic information >@@ -172,8 +172,13 @@ > ;; When an extraction-expr is used as a conversion > (defcl extraction-conversion (extraction-application)) > >+#-sbcl > (defcl number-expr (expr) > (number :type integer :parse t :restore-as nil)) >+#+sbcl >+(sb-ext:without-package-locks >+ (defcl number-expr (expr) >+ (number :type integer :parse t :restore-as nil))) > > ;; This is for integers of the form xxx.000, where the fractional part is > ;; all zeros. We keep it as a number expr, but store the number of zeros so >@@ -529,10 +534,17 @@ > ;;; resolution. The inclusions are the predicates which will become > ;;; TCCs if that particular resolution is chosen. > >+#-sbcl > (defcl resolution () > (declaration :restore-as nil) > module-instance > type) >+#+sbcl >+(sb-ext:without-package-locks >+ (defcl resolution () >+ (declaration :restore-as nil) >+ module-instance >+ type)) > > ;(defcl judgement-resolution (resolution) > ; judgement-type >diff -Naur pvs4.2-orig/src/context.lisp pvs4.2-sbcl/src/context.lisp >--- pvs4.2-orig/src/context.lisp 2008-05-11 20:34:50.000000000 +0000 >+++ pvs4.2-sbcl/src/context.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -402,8 +402,9 @@ > subdir)) > (multiple-value-bind (result err) > (ignore-lisp-errors #+allegro (excl:make-directory subdir) >- #+(or cmu sbcl) >- (unix:unix-mkdir (namestring subdir) #o777)) >+ #+cmu (unix:unix-mkdir (namestring subdir) #o777) >+ #+sbcl >+ (sb-unix:unix-mkdir (namestring subdir) #o777)) > (cond (result (pvs-message "Created directory ~a" subdir) > t) > (t (pvs-message "Error creating ~a: ~a" subdir err) >@@ -534,7 +535,7 @@ > > #+(or cmu sbcl) > (defun md5-file (file) >- (let ((digest (md5:md5sum-file file)) >+ (let ((digest (#+cmu md5:md5sum-file #+sbcl sb-md5:md5sum-file file)) > (sum 0)) > (loop for x across digest > do (setq sum (+ (* sum 256) x))) >diff -Naur pvs4.2-orig/src/datatype.lisp pvs4.2-sbcl/src/datatype.lisp >--- pvs4.2-orig/src/datatype.lisp 2008-05-11 20:36:59.000000000 +0000 >+++ pvs4.2-sbcl/src/datatype.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -203,7 +203,8 @@ > (checksum-ok? (and adt-ce > file-exists? > (equal #+allegro (excl:md5-file adt-path) >- #-allegro (md5:md5sum-file adt-path) >+ #+sbcl (sb-md5:md5sum-file adt-path) >+ #-(or allegro sbcl) (md5:md5sum-file adt-path) > (ce-md5sum adt-ce))))) > (unless (and file-exists? > ce >diff -Naur pvs4.2-orig/src/defcl.lisp pvs4.2-sbcl/src/defcl.lisp >--- pvs4.2-orig/src/defcl.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/defcl.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -51,11 +51,13 @@ > (defmacro defcl (name classes &rest args) > (setf args (mapcar #'(lambda (a) (if (consp a) a (list a))) args)) > `(progn ,@(mapcar #'(lambda (a) >- #+allegro `(declaim (ftype (function >+ #+(or allegro sbcl) >+ `(declaim (ftype (function > (t) > ,(cadr (member :type a))) > ,(car a))) >- #-allegro `(proclaim '(function ,(car a) (t) >+ #-(or allegro sbcl) >+ `(proclaim '(function ,(car a) (t) > ,(cadr (member :type a))))) > (remove-if-not #'(lambda (a) (member :type a)) > args)) >diff -Naur pvs4.2-orig/src/defsystem.lisp pvs4.2-sbcl/src/defsystem.lisp >--- pvs4.2-orig/src/defsystem.lisp 2007-07-06 19:08:53.000000000 +0000 >+++ pvs4.2-sbcl/src/defsystem.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -4796,7 +4796,7 @@ > :loader #+:lucid #'load-foreign-files > #+:allegro #'load > #+(or :cmu :scl) #'alien:load-foreign >- #+:sbcl #'sb-alien:load-foreign >+ #+:sbcl #'sb-alien:load-shared-object > #+(and :lispworks :unix (not :linux) (not :macosx)) #'link-load:read-foreign-modules > #+(and :lispworks :unix (or :linux :macosx)) #'fli:register-module > #+(and :lispworks :win32) #'fli:register-module >diff -Naur pvs4.2-orig/src/globals.lisp pvs4.2-sbcl/src/globals.lisp >--- pvs4.2-orig/src/globals.lisp 2008-07-17 18:12:19.000000000 +0000 >+++ pvs4.2-sbcl/src/globals.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -346,7 +346,9 @@ > (pprint-indent :block 0) > (loop (pprint-exit-if-list-exhausted) > (write (pprint-pop) :stream stream :escape nil :pretty nil >- :pprint-dispatch nil) >+ :pprint-dispatch #-sbcl nil >+ #+sbcl (sb-pretty::make-pprint-dispatch-table) >+ ) > (pprint-exit-if-list-exhausted) > (pprint-newline :mandatory stream))))) > >@@ -385,6 +387,7 @@ > > (defvar *use-default-dp?* nil) > (defvar *prover-print-lines* nil) >+#-sbcl > (defvar *print-lines* nil) > > (defvar *substit-dont-simplify* nil) >diff -Naur pvs4.2-orig/src/groundeval/eval-utils.lisp pvs4.2-sbcl/src/groundeval/eval-utils.lisp >--- pvs4.2-orig/src/groundeval/eval-utils.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/groundeval/eval-utils.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -68,14 +68,14 @@ > (defmethod print-object ((obj eval-info) stream) > (if *debugging-print-object* > (call-next-method) >- (format stream "~@<#<eval-info ~2I~_~:0Iinternal: ~W~:@_external: ~W>~:>" >+ (format stream "~@<#<eval-info ~2I~_~0:Iinternal: ~W~:@_external: ~W>~:>" > (internal obj) (external obj)))) > > (defmethod print-object ((obj eval-defn-info) stream) > (if *debugging-print-object* > (call-next-method) > (format stream >- "~@<#<eval-defn-info ~2I~_~:0Iunary: ~W~:@_multiary: ~W~:@_destructive: ~W>~:>" >+ "~@<#<eval-defn-info ~2I~_~0:Iunary: ~W~:@_multiary: ~W~:@_destructive: ~W>~:>" > (unary obj) (multiary obj) (destructive obj)))) > > (defmethod print-object ((obj eval-defn) stream) >diff -Naur pvs4.2-orig/src/groundeval/ground-expr.lisp pvs4.2-sbcl/src/groundeval/ground-expr.lisp >--- pvs4.2-orig/src/groundeval/ground-expr.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/groundeval/ground-expr.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -29,7 +29,7 @@ > ; -- no free variables > ; > >-(in-package 'pvs) >+(in-package :pvs) > > (defun ground-expr? (expr) > (assert (type expr)) >diff -Naur pvs4.2-orig/src/groundeval/pvs2clean.lisp pvs4.2-sbcl/src/groundeval/pvs2clean.lisp >--- pvs4.2-orig/src/groundeval/pvs2clean.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/groundeval/pvs2clean.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -138,7 +138,7 @@ > > (defmethod pvs2clean* ((expr projection-application) bindings livevars) > (let* ((ll (length (exprs expr))) >- (dummy (gentemp 'ddd)) >+ (dummy (gentemp "DDD")) > (match-list (pvs2clean_tuple (matchlist (index expr) ll dummy))) > (expr-list (pvs2clean* expr bindings livevars))) > `(let ,match-list = ,expr-list in ,dummy))) >@@ -177,7 +177,7 @@ > (updateable-free-formal-vars operator) > livevars)))) > (if (clean-updateable? (type operator)) >- (format nil "(pvsSelect ~a ~a)" >+ (format nil "(pvsSelect ~a ~a ~a)" > clean-op clean-arg > (mk-clean-funcall clean-op > (list clean-arg)))))))) >@@ -375,6 +375,7 @@ > livevars)))))) > (if else-part > (format nil "~a ~% _ -> ~a" >+ selections-clean > (pvs2clean* (expression else-part) bindings livevars)) > selections-clean))) > >diff -Naur pvs4.2-orig/src/groundeval/pvseval-update.lisp pvs4.2-sbcl/src/groundeval/pvseval-update.lisp >--- pvs4.2-orig/src/groundeval/pvseval-update.lisp 2007-12-01 23:04:01.000000000 +0000 >+++ pvs4.2-sbcl/src/groundeval/pvseval-update.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -47,7 +47,7 @@ > (if (special-variable-p id) > (let ((lid (gethash id *lisp-id-hash*))) > (or lid >- (let ((new-lid (intern (gensym (string id))))) >+ (let ((new-lid (intern (symbol-name (gensym (string id)))))) > (setf (gethash id *lisp-id-hash*) new-lid) > new-lid))) > id)) >@@ -1779,7 +1779,7 @@ > :if-exists > (if supersede? :supersede :append) > :if-does-not-exist :create) >- (when supersede? (format output "(in-package 'PVS)~%")) >+ (when supersede? (format output "(in-package :pvs)~%")) > (print-lisp-defns-to-output (get-theory theory) output)) > (print-lisp-defns-to-output (get-theory theory) nil))) > >diff -Naur pvs4.2-orig/src/groundeval/static-update.lisp pvs4.2-sbcl/src/groundeval/static-update.lisp >--- pvs4.2-orig/src/groundeval/static-update.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/groundeval/static-update.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -42,7 +42,7 @@ > ;; Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. > ;; -------------------------------------------------------------------- > >-(in-package 'pvs) >+(in-package :pvs) > > (defmethod updateable? ((texpr tupletype)) > (updateable? (types texpr))) >diff -Naur pvs4.2-orig/src/ground-prover/prglobals.lisp pvs4.2-sbcl/src/ground-prover/prglobals.lisp >--- pvs4.2-orig/src/ground-prover/prglobals.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/ground-prover/prglobals.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -46,7 +46,7 @@ > (defconstant true 'true ) > (defconstant false 'false ) > >-(defconstant primtypealist >+(defconstant-if-unbound primtypealist > '((true . bool) > (false . bool) > (and . bool) >@@ -139,16 +139,16 @@ > > ;;; the following special declarations are rather offensive: > >-(proclaim '(special const sum u s eq lit var coef product ineqpot )) >+(proclaim '(special const sum u s #-sbcl eq lit var coef product ineqpot )) > > > ;;; the following (til end-of-file) are taken from prpp: > >-(defconstant *infixlist* ;temporary list of infixes >+(defconstant-if-unbound *infixlist* ;temporary list of infixes > '(equal nequal lessp greaterp lesseq lesseqp greatereq greatereqp > PLUS MINUS TIMES DIVIDE DIFFERENCE) ) > >-(defconstant precedence-alist >+(defconstant-if-unbound precedence-alist > '((iff 1) > (implies 2) > (or 3) >diff -Naur pvs4.2-orig/src/ground-prover/prmacros.lisp pvs4.2-sbcl/src/ground-prover/prmacros.lisp >--- pvs4.2-orig/src/ground-prover/prmacros.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/ground-prover/prmacros.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -55,21 +55,21 @@ > (defun prerr (&rest args) > (apply #'error args)) > >-(defconstant *truecons* '(true)) >+(defconstant-if-unbound *truecons* '(true)) > >-(defconstant *eqarithrels* '(greatereqp lesseqp)) >+(defconstant-if-unbound *eqarithrels* '(greatereqp lesseqp)) > > (defconstant *ifops* nil ;;'(if if*) > ) > >-(defconstant *boolconstants* '(false true)) >+(defconstant-if-unbound *boolconstants* '(false true)) > >-(defconstant *arithrels* '(lessp lesseqp greaterp greatereqp)) >+(defconstant-if-unbound *arithrels* '(lessp lesseqp greaterp greatereqp)) > >-(defconstant *arithops* '(PLUS TIMES DIFFERENCE MINUS)) >+(defconstant-if-unbound *arithops* '(PLUS TIMES DIFFERENCE MINUS)) > >-(defconstant *boolops* '(and or implies not ;;if >- iff)) >+(defconstant-if-unbound *boolops* '(and or implies not ;;if >+ iff)) > > (defmacro singleton? (obj) > `(and (consp ,obj) (null (cdr ,obj)))) >diff -Naur pvs4.2-orig/src/ground-prover/process.lisp pvs4.2-sbcl/src/ground-prover/process.lisp >--- pvs4.2-orig/src/ground-prover/process.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/ground-prover/process.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -729,7 +729,7 @@ > ; (set (setsolve atf)) > (tuple (tupsolve atf)) > (array (arraysolve atf)) >- (t (error "No solver for type " (prtype (arg1 atf)))) >+ (t (error "No solver for type ~a" (prtype (arg1 atf)))) > ))))) > > ; ------------------------------------------------------------------ >@@ -808,7 +808,7 @@ > ; (set (setnsolve atf)) > (tuple (tupnsolve atf)) > (array (arraynsolve atf)) >- (t (error "No nsolve for type " >+ (t (error "No nsolve for type ~a" > (or (prtype (arg1 atf)) (prtype (arg2 atf))) )) > ))))) > >diff -Naur pvs4.2-orig/src/interface/pvs-emacs.lisp pvs4.2-sbcl/src/interface/pvs-emacs.lisp >--- pvs4.2-orig/src/interface/pvs-emacs.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/interface/pvs-emacs.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -66,11 +66,15 @@ > *noninteractive-timeout* > ,(not (and (listp form) > (memq (car form) *prover-invoking-commands*)))) >- #-(or multiprocessing mp) nil >+ #-(or multiprocessing mp sbcl) nil > #+(or multiprocessing mp) > (mp:with-timeout (*noninteractive-timeout* > (format t "Timed out!")) > ,form) >+ #+sbcl >+ (sb-ext:with-timeout *noninteractive-timeout* >+ (handler-case ,form >+ (sb-ext:timeout () (format t "Timed out!")))) > ,form)) > (string (error) > (with-output-to-string (string) >@@ -94,7 +98,7 @@ > ;;; This replaces ilisp-restore in pvs-init > (defun pvs-ilisp-restore () > "Restore the old result history." >- (declare (special / // + ++ * **)) >+ #-sbcl (declare (special / // + ++ * **)) > (setq // (pop *old-result*) > ** (first //) > / (pop *old-result*) >@@ -105,7 +109,7 @@ > nil) > > (defun pvs-ilisp-save () >- (declare (special / // /// + ++ +++)) >+ #-sbcl (declare (special / // /// + ++ +++)) > (unless *old-result* > (setq *old-result* (list /// // +++ ++)))) > >@@ -546,7 +550,8 @@ > (t (cons (char string pos) result)))) > (coerce (nreverse result) 'string))) > >-(#+(or cmu sbcl) ext:without-package-locks >+(#+cmu ext:without-package-locks >+ #+sbcl sb-ext:without-package-locks > #-(or cmu sbcl) progn > (defun parse-error (obj message &rest args) > ;;(assert (or *in-checker* *current-file*)) >@@ -606,7 +611,8 @@ > (defvar *type-error-argument* nil) > (defvar *skip-all-conversion-checks* nil) > >-(#+(or cmu sbcl) ext:without-package-locks >+(#+cmu ext:without-package-locks >+ #+sbcl sb-ext:without-package-locks > #-(or cmu sbcl) progn > (defun type-error (obj message &rest args) > (let ((errmsg (type-error-for-conversion obj message args))) >diff -Naur pvs4.2-orig/src/linked-hash-table.lisp pvs4.2-sbcl/src/linked-hash-table.lisp >--- pvs4.2-orig/src/linked-hash-table.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/linked-hash-table.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -51,7 +51,7 @@ > (if (memq test '(eq eql equal equalp)) > (make-hash-table :test test :size size :rehash-size rehash-size > :rehash-threshold rehash-threshold >- :weak-p weak-keys) >+ #-sbcl :weak-p #+sbcl :weakness weak-keys) > (make-pvs-hash-table > :strong-eq? (eq test 'strong-tc-eq) > :weak-p weak-keys >@@ -77,6 +77,8 @@ > :weak-keys (excl:hash-table-weak-keys ht)) > #-allegro > (let* ((test (hash-table-test ht)) >+ (weakp #+sbcl (sb-ext:hash-table-weakness ht) >+ #-sbcl (lisp::hash-table-weak-p ht)) > (newht > (if (memq test '(eq eql equal equalp)) > (make-hash-table >@@ -84,13 +86,14 @@ > :size size > :rehash-size rehash-size > :rehash-threshold rehash-threshold >- :weak-p (lisp::hash-table-weak-p ht)) >+ #-sbcl :weak-p #+sbcl :weakness weakp) > (make-pvs-hash-table :strong-eq? (eq test 'strong-tc-eq) >- :weak-keys? (lisp::hash-table-weak-p ht) >+ :weak-keys? weakp > :size size > :rehash-size rehash-size > :rehash-threshold rehash-threshold >- :table (lisp::hash-table-table ht))))) >+ :table #-sbcl (lisp::hash-table-table ht) >+ #+sbcl (sb-impl::hash-table-table ht))))) > (declare (inline maphash)) > (maphash #'(lambda (x y) (setf (gethash x newht) y)) > ht) >diff -Naur pvs4.2-orig/src/make-pvs-methods.lisp pvs4.2-sbcl/src/make-pvs-methods.lisp >--- pvs4.2-orig/src/make-pvs-methods.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/make-pvs-methods.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -33,8 +33,11 @@ > ;; This sets *pvs-path* and sets *pvs-binary-type* > (load "pvs-config.lisp")) > >-(defpackage pvs (:use #+lucid :lucid-common-lisp :lisp >- #-(or gcl cmu sbcl) :clos #+(or gcl cmu sbcl) :pcl)) >+(defpackage pvs (:use #+lucid :lucid-common-lisp #-sbcl :lisp #+sbcl :cl >+ #-(or gcl cmu sbcl) :clos #+(or gcl cmu) :pcl >+ #+sbcl :sb-pcl) >+ #+sbcl (:shadowing-import-from :sb-int memq) >+ #+sbcl (:export memq)) > > (in-package :pvs) > (import '(cl-user:*pvs-path*)) >diff -Naur pvs4.2-orig/src/metering.lisp pvs4.2-sbcl/src/metering.lisp >--- pvs4.2-orig/src/metering.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/metering.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -288,7 +288,7 @@ > ;;; to seconds. > > (progn >- #-(or cmu allegro) >+ #-(or sbcl cmu allegro) > (eval-when (compile eval) > (warn > "You may want to supply implementation-specific get-time functions.")) >@@ -302,6 +302,12 @@ > ;;; The get-cons macro is called to find the total number of bytes > ;;; consed since the beginning of time. > >+#+sbcl >+(defmacro get-cons () >+ "The get-cons macro is called to find the total number of bytes >+ consed since the beginning of time." >+ '(sb-ext:get-bytes-consed)) >+ > #+:cmu > (defmacro get-cons () > "The get-cons macro is called to find the total number of bytes >@@ -312,7 +318,7 @@ > #+:lcl3.0 > (defmacro get-cons () `(gc-size)) > >-#-(or :cmu :lcl3.0) >+#-(or sbcl :cmu :lcl3.0) > (progn > (eval-when (compile eval) > (warn "No consing will be reported unless a get-cons function is ~ >@@ -326,6 +332,12 @@ > ;;; arguments. The function Required-Arguments returns two values: the first > ;;; is the number of required arguments, and the second is T iff there are any > ;;; non-required arguments (e.g. &optional, &rest, &key). >+#+sbcl >+(defun required-arguments (name) >+ (multiple-value-bind (min max) >+ (sb-kernel:fun-type-nargs (sb-kernel:ctype-of (symbol-function name))) >+ (values (or min 0) (or (null max) (> max min))))) >+ > #+cmu > (progn > #-new-compiler >@@ -387,7 +399,7 @@ > > > >-#-(or :cmu :lcl3.0 (and :allegro (not :coral))) >+#-(or sbcl :cmu :lcl3.0 (and :allegro (not :coral))) > (progn > (eval-when (compile eval) > (warn >diff -Naur pvs4.2-orig/src/pp-html.lisp pvs4.2-sbcl/src/pp-html.lisp >--- pvs4.2-orig/src/pp-html.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/pp-html.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -611,7 +611,8 @@ > (when (eq ans :auto) > (setq *force-dirs* t))))) > #+allegro (excl:make-directory dir) >- #+(or cmu sbcl) (unix:unix-mkdir dir #o777) >+ #+cmu (unix:unix-mkdir dir #o777) >+ #+sbcl (sb-unix:unix-mkdir dir #o777) > (pvs-message "Directory ~a created" dir)) > (t (html-pvs-error "Directory ~a not created" dir)))))) > >diff -Naur pvs4.2-orig/src/prover/checker-macros.lisp pvs4.2-sbcl/src/prover/checker-macros.lisp >--- pvs4.2-orig/src/prover/checker-macros.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/prover/checker-macros.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -55,7 +55,7 @@ > (defvar *printproofstate* nil) > (defvar *in-checker* nil) > (defvar *in-apply* nil) >-(defvar *please-interrupt* nil) >+(defvar *please-interrupt* #-sbcl nil #+sbcl t) > (defvar *assert-bindings* nil) > (defvar *modsubst* nil) > (defvar *proving-tcc* nil) >@@ -143,9 +143,11 @@ > (defvar *module-context*) > ;;(defvar *current-theory*) > (defvar *ps* nil) >-(defvar * '*) >-(defvar + '+) >-(defvar - '-) >+(#+sbcl sb-ext:without-package-locks >+ #-sbcl progn >+ (defvar * '*) >+ (defvar + '+) >+ (defvar - '-)) > (defvar *macro-names* nil) > (defvar *subst-type-hash* ;;used in assert-sformnums > ;;(make-pvs-hash-table) >@@ -177,14 +179,22 @@ > (defmacro with-interrupts-deferred (&body form) > `(let ((excl::*without-interrupts* t)) ,@form)) > >-#+(or cmu sbcl) >+#+cmu > (defmacro with-interrupts-allowed (&body form) > `(system:with-interrupts ,@form)) > >-#+(or cmu sbcl) >+#+cmu > (defmacro with-interrupts-deferred (&body form) > `(system:without-interrupts ,@form)) > >+#+sbcl >+(defmacro with-interrupts-allowed (&body form) >+ `(sb-sys:with-interrupts ,@form)) >+ >+#+sbcl >+(defmacro with-interrupts-deferred (&body form) >+ `(sb-sys:without-interrupts ,@form)) >+ > > > ;;; KCL does not really have the equivalent to the following - punt for now. >diff -Naur pvs4.2-orig/src/prover/eproofcheck.lisp pvs4.2-sbcl/src/prover/eproofcheck.lisp >--- pvs4.2-orig/src/prover/eproofcheck.lisp 2008-01-14 11:12:56.000000000 +0000 >+++ pvs4.2-sbcl/src/prover/eproofcheck.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -210,9 +210,15 @@ > (and *noninteractive* > *noninteractive-timeout*)) > (let ((timeout (or *proof-timeout* *noninteractive-timeout*))) >+ #-sbcl > (mp:with-timeout (timeout (pvs-message "Interrupted: ~a sec timeout" > timeout)) >- (call-next-method))) >+ (call-next-method)) >+ #+sbcl >+ (sb-ext:with-timeout timeout >+ (handler-case (call-next-method) >+ (sb-ext:timeout () >+ (pvs-message "Interrupted: ~a sec timeout" timeout))))) > (call-next-method))) > > (defmethod prove-decl ((decl formula-decl) &key strategy context) >@@ -3446,7 +3452,7 @@ > (values 'X nil nil)) > ((and (or (digit-char-p (char strlbl 0)) > (char= (char strlbl 0) #\-)) >- (every #'digit-char-p (subseq strlbl) 1)) >+ (every #'digit-char-p (subseq strlbl 1))) > (error-format-if > "~%Label cannot be an integer")) > (t >diff -Naur pvs4.2-orig/src/prover/rules.lisp pvs4.2-sbcl/src/prover/rules.lisp >--- pvs4.2-orig/src/prover/rules.lisp 2008-01-16 04:53:29.000000000 +0000 >+++ pvs4.2-sbcl/src/prover/rules.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -334,9 +334,15 @@ > (init-time (get-internal-run-time)) > (result (let ((*in-apply* ps)) > (if timeout >+ #-sbcl > (mp:with-timeout (timeout nil) > (prove* newps) > newps) >+ #+sbcl >+ (sb-ext:with-timeout timeout >+ (handler-case >+ (progn (prove* newps) newps) >+ (sb-ext:timeout () nil))) > (prove* newps)))) > (end-time (/ (- (get-internal-run-time) init-time) > internal-time-units-per-second))) >diff -Naur pvs4.2-orig/src/prover/translate-to-yices.lisp pvs4.2-sbcl/src/prover/translate-to-yices.lisp >--- pvs4.2-orig/src/prover/translate-to-yices.lisp 2007-09-07 20:02:37.000000000 +0000 >+++ pvs4.2-sbcl/src/prover/translate-to-yices.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -910,6 +910,13 @@ > :input "//dev//null" > :output out > :error-output :output) >+ #+sbcl >+ (sb-ext:run-program >+ (format nil "~a ~a" *yices-call* (namestring file)) >+ nil >+ :input "//dev//null" >+ :output out >+ :error out) > #+cmu > (extensions:run-program > (format nil "~a ~a" *yices-call* (namestring file)) >diff -Naur pvs4.2-orig/src/pvs.lisp pvs4.2-sbcl/src/pvs.lisp >--- pvs4.2-orig/src/pvs.lisp 2008-07-19 20:29:49.000000000 +0000 >+++ pvs4.2-sbcl/src/pvs.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -102,19 +102,21 @@ > (let ((exepath (car (make::split-string > (environment-variable "LD_LIBRARY_PATH") :item #\:)))) > (pushnew exepath *pvs-directories*) >- (ext:load-foreign (format nil "~a/mu.~a" exepath >+ (#+cmu ext:load-foreign #+sbcl sb-alien:load-shared-object >+ (format nil "~a/mu.~a" exepath > #+darwin "dylib" > #-darwin "so")) >- (ext:load-foreign (format nil "~a/ws1s.~a" exepath >+ (#+cmu ext:load-foreign #+sbcl sb-alien:load-shared-object >+ (format nil "~a/ws1s.~a" exepath > #+darwin "dylib" > #-darwin "so")) > ;; Have no idea what is going on here, but if you leave this out, > ;; bdd-cmu gives a compile error. >- (fmakunbound 'bdd_cofactor_neg_) >- (lf "bdd-cmu") >- (lf "mu-cmu") >+ #+cmu (fmakunbound 'bdd_cofactor_neg_) >+ #+cmu (lf "bdd-cmu") #+sbcl (lf "bdd-sbcl") >+ #+cmu (lf "mu-cmu") #+sbcl (lf "mu-sbcl") > (bdd_init) >- (lf "dfa-foreign-cmu")) >+ #+cmu (lf "dfa-foreign-cmu") #+sbcl (lf "dfa-foreign-sbcl")) > (setq *started-with-minus-q* > (or dont-load-user-lisp > (let ((mq (environment-variable "PVSMINUSQ"))) >diff -Naur pvs4.2-orig/src/restore-theories.lisp pvs4.2-sbcl/src/restore-theories.lisp >--- pvs4.2-orig/src/restore-theories.lisp 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/restore-theories.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -27,7 +27,7 @@ > ;; Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. > ;; -------------------------------------------------------------------- > >-(in-package 'pvs) >+(in-package :pvs) > > ;;; Restores the state of the system from information provided in the > ;;; context. The context has the form >diff -Naur pvs4.2-orig/src/store-object.lisp pvs4.2-sbcl/src/store-object.lisp >--- pvs4.2-orig/src/store-object.lisp 2007-10-13 21:30:22.000000000 +0000 >+++ pvs4.2-sbcl/src/store-object.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -301,8 +301,8 @@ > (ensure-vector-size *store-object-store* *store-object-store-size* size) > (with-open-file (f file :direction :input > :element-type '(unsigned-byte 32)) >- (lisp:read-sequence *store-object-store* f >- :start 0 :end size)) >+ (cl:read-sequence *store-object-store* f >+ :start 0 :end size)) > (when reverse-endian > (dotimes (i size) > (setf (object-store i) >diff -Naur pvs4.2-orig/src/tex-support.lisp pvs4.2-sbcl/src/tex-support.lisp >--- pvs4.2-orig/src/tex-support.lisp 2008-03-11 22:53:37.000000000 +0000 >+++ pvs4.2-sbcl/src/tex-support.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -532,7 +532,7 @@ > (when (and *report-mode* > (loop for sf in neg-s-forms > thereis (memq sf par-sforms))) >- (format stream "~% & $\\vdots$ \\\\" *prover-indent*))) >+ (format stream "~%~VT & $\\vdots$ \\\\" *prover-indent*))) > (t (format stream "\\strut\\\\"))) > (format stream "\\hline~%") > (cond (pos-s-forms >diff -Naur pvs4.2-orig/src/utils/file-utils-sbcl.lisp pvs4.2-sbcl/src/utils/file-utils-sbcl.lisp >--- pvs4.2-orig/src/utils/file-utils-sbcl.lisp 1970-01-01 00:00:00.000000000 +0000 >+++ pvs4.2-sbcl/src/utils/file-utils-sbcl.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -0,0 +1,66 @@ >+;; -------------------------------------------------------------------- >+;; PVS >+;; Copyright (C) 2008, 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., 51 Franklin Street - Fifth Floor, Boston, MA >+;; 02110-1301, USA. >+;; -------------------------------------------------------------------- >+ >+(in-package :pvs) >+(require :sb-posix) >+(export '(file-exists-p directory-p read-permission? write-permission? >+ file-write-time get-file-info)) >+ >+(defun remove-backslashes (string) >+ (declare (type string string)) >+ (sb-impl::remove-backslashes string 0 (length string))) >+ >+(defun file-exists-p (file) >+ (handler-case >+ (zerop >+ (sb-posix:access >+ (remove-backslashes (namestring (merge-pathnames file))) >+ sb-posix:f-ok)) >+ (sb-posix:syscall-error () nil))) >+ >+(defun directory-p (dir) >+ (handler-case >+ (let ((filestring (namestring (merge-pathnames dir)))) >+ (when (sb-posix:s-isdir (sb-posix:stat-mode (sb-posix:stat filestring))) >+ ;; Needs to end with a slash!!! >+ (pathname (if (char= (char filestring (1- (length filestring))) #\/) >+ filestring >+ (concatenate 'string filestring "/"))))) >+ (sb-posix:syscall-error () nil))) >+ >+(defun read-permission? (file) >+ (handler-case (zerop (sb-posix:access file sb-posix:r-ok)) >+ (sb-posix:syscall-error () nil))) >+ >+(defun write-permission? (file) >+ (handler-case (zerop (sb-posix:access file sb-posix:w-ok)) >+ (sb-posix:syscall-error () nil))) >+ >+(defconstant u1970 (encode-universal-time 0 0 0 1 1 1970 0)) >+ >+(defun file-write-time (file) >+ (handler-case (+ u1970 (sb-posix:stat-mtime (sb-posix:stat file))) >+ (sb-posix:syscall-error () nil))) >+ >+(defun get-file-info (file) >+ (handler-case >+ (let ((stat (sb-posix:stat file))) >+ (list (sb-posix:stat-dev stat) (sb-posix:stat-ino stat))) >+ (sb-posix:syscall-error () nil))) >diff -Naur pvs4.2-orig/src/utils/hashfn.lisp pvs4.2-sbcl/src/utils/hashfn.lisp >--- pvs4.2-orig/src/utils/hashfn.lisp 2007-10-11 00:14:03.000000000 +0000 >+++ pvs4.2-sbcl/src/utils/hashfn.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -56,7 +56,7 @@ > ;; Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. > ;; -------------------------------------------------------------------- > >-(in-package 'pvs) >+(in-package :pvs) > > ;(declaim (function pvs-sxhash* (T list) (integer 0 65535))) > >@@ -64,7 +64,7 @@ > ;(defun tc-eq (x y &optional bindings) > ; (tc-eq* x y bindings)) > >-(defconstant pvs-sxhash-byte (byte #+allegro 24 #-allegro 29 0)) >+(defconstant-if-unbound pvs-sxhash-byte (byte #+allegro 24 #-allegro 29 0)) > > (defconstant pvs-max-hashnum (1- (expt 2 #+allegro 24 #-allegro 29))) > >@@ -104,7 +104,7 @@ > (declare (ignore bindings)) > (the positive-fixnum (sxhash x))) > >-(defconstant nil-sxhash (sxhash nil)) >+(defconstant-if-unbound nil-sxhash (sxhash nil)) > > (defmethod pvs-sxhash* ((x null) bindings) > (declare (ignore bindings)) >diff -Naur pvs4.2-orig/src/utils/ix86_64-Linux/Makefile pvs4.2-sbcl/src/utils/ix86_64-Linux/Makefile >--- pvs4.2-orig/src/utils/ix86_64-Linux/Makefile 1970-01-01 00:00:00.000000000 +0000 >+++ pvs4.2-sbcl/src/utils/ix86_64-Linux/Makefile 2009-03-24 18:56:17.000000000 +0000 >@@ -0,0 +1,23 @@ >+LD = gcc >+LDFLAGS = -shared -L./ >+CC=gcc >+CFLAGS=-fPIC >+WFLAGS=-Wall >+VPATH=.. >+ >+obj=file_utils.o >+ >+.SUFFIXES: >+.SUFFIXES: .c .o >+.c.o : ; $(CC) $(XCFLAGS) ${WFLAGS} ${CFLAGS} -c $< -o $@ >+ >+all : file_utils.so b64 >+ >+file_utils.so: ${obj} >+ $(LD) ../utils-ld-table $(LDFLAGS) -o file_utils.so ${obj} -lc >+ >+b64: ../b64.c >+ $(CC) -o ./b64 ../b64.c >+ >+clean : >+ rm -f *.o *.a *.so b64 >diff -Naur pvs4.2-orig/src/utils.lisp pvs4.2-sbcl/src/utils.lisp >--- pvs4.2-orig/src/utils.lisp 2008-07-17 10:35:11.000000000 +0000 >+++ pvs4.2-sbcl/src/utils.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -137,11 +137,12 @@ > (let* ((test (hash-table-test ht)) > (size (hash-table-count ht)) > (weak? #+allegro (excl:hash-table-weak-keys ht) >- #+(or cmu sbcl) (lisp::hash-table-weak-p ht)) >+ #+cmu (lisp::hash-table-weak-p ht) >+ #+sbcl (sb-ext:hash-table-weakness ht)) > (new-ht (if (memq test '(eq eql equal equalp)) > (make-hash-table > :test test :size size >- #+allegro :weak-keys #+(or cmu sbcl) :weak-p weak?) >+ #+allegro :weak-keys #+cmu :weak-p #+sbcl :weakness weak?) > (make-pvs-hash-table :strong-eq? (eq test 'strong-tc-eq) > :size size > :weak-keys? weak?)))) >@@ -279,7 +280,8 @@ > #+(and allegro (version>= 6) (not (version>= 7))) > (excl::variable-special-p obj nil) > #+(and allegro (not (version>= 6))) (clos::variable-special-p obj nil) >- #+(or cmu sbcl) (eq (extensions:info variable kind obj) :special) >+ #+cmu (eq (extensions:info variable kind obj) :special) >+ #+sbcl (sb-walker:var-globally-special-p obj) > #+harlequin-common-lisp (system:declared-special-p obj) > #-(or lucid kcl allegro harlequin-common-lisp cmu sbcl) > (error "Need to handle special variables for this version of lisp") >@@ -310,14 +312,22 @@ > (namestring (working-directory)))) > nil) > >-#+(or gcl cmu sbcl) >+#+(or gcl cmu) > (defun working-directory () > (pathname (nth-value 1 (unix:unix-current-directory)))) > >-#+(or gcl cmu sbcl) >+#+(or gcl cmu) > (defun set-working-directory (dir) > (unix:unix-chdir (namestring dir))) > >+#+sbcl >+(defun working-directory () >+ (make-pathname :directory (sb-posix:getcwd))) >+ >+#+sbcl >+(defun set-working-directory (dir) >+ (sb-posix:chdir dir)) >+ > #+allegro > (defun working-directory () > (excl:current-directory)) >@@ -334,10 +344,14 @@ > (defun environment-variable (string) > (sys:getenv string)) > >-#+(or cmu sbcl) >+#+cmu > (defun environment-variable (string) > (tools:getenv string)) > >+#+sbcl >+(defun environment-variable (string) >+ (sb-posix:getenv string)) >+ > #+harlequin-common-lisp > (defun environment-variable (string) > ;; This didn't work before >@@ -370,13 +384,20 @@ > :show-cmd nil > :output-stream (open "/dev/null" :direction :output > :if-exists :append))) >-#+(or cmu sbcl) >+#+cmu > (defun chmod (prot file) > (extensions:run-program > "chmod" > (list prot (namestring file)) > :output nil :error nil :wait nil)) > >+#+sbcl >+(defun chmod (prot file) >+ (sb-ext:run-program >+ "chmod" >+ (list prot (namestring file)) >+ :output nil :error nil :wait nil)) >+ > #+gcl > (defun chmod (prot file) > (system (format nil "chmod ~a ~a" prot (namestring file)))) >@@ -605,11 +626,12 @@ > > (defun shortpath (directory) > (or (gethash directory *shortpath-directories*) >- (let* ((dirlist (pathname-directory >+ (let* ((realdir (namestring (truename directory))) >+ (dirlist (pathname-directory > (directory-p >- (#+allegro excl:pathname-resolve-symbolic-links >- #+(or cmu sbcl) unix:unix-resolve-links >- (namestring (truename directory)))))) >+ #+allegro (excl:pathname-resolve-symbolic-links realdir) >+ #+cmu (unix:unix-resolve-links realdir) >+ #-(or allegro cmu) realdir))) > (file-info (get-file-info directory)) > (result (if (eq (car dirlist) :absolute) > (shortpath* (reverse (cdr dirlist)) file-info) >@@ -2915,10 +2937,14 @@ > (defun direct-superclasses (class) > (slot-value class 'pcl:class-direct-superclasses)) > >-#+(or cmu sbcl) >+#+cmu > (defun direct-superclasses (class) > (class-direct-superclasses class)) > >+#+sbcl >+(defun direct-superclasses (class) >+ (sb-mop:class-direct-superclasses class)) >+ > (defun types-of (obj) > (let ((types nil)) > (labels ((tof (type) >@@ -3225,7 +3251,7 @@ > (when (compiled-function-p #'pvs-gc-after-hook) > (setf excl:*gc-after-hook* #'pvs-gc-after-hook))) > >-#+(or cmu sbcl) >+#+cmu > (eval-when (load) > (setf extensions:*gc-verbose* nil)) > >@@ -4022,7 +4048,8 @@ > (every #'(lambda (slot) > (let ((name (slot-value slot > '#+allegro excl::name >- #+(or cmu sbcl) pcl::name))) >+ #+cmu pcl::name >+ #+sbcl sb-pcl::name))) > (equals (slot-value x name) (slot-value y name)))) > slots))) > >@@ -4059,8 +4086,12 @@ > #-(or allegro cmu sbcl) > (error "Need a hash-table for tc-eq for this lisp")) > >-#+(or cmu sbcl) >+#+cmu > (extensions:define-hash-table-test 'tc-eq-test #'tc-eq #'pvs-sxhash) >-#+(or cmu sbcl) >+#+cmu > (extensions:define-hash-table-test 'strong-tc-eq-test > #'strong-tc-eq #'pvs-sxhash) >+#+sbcl >+(sb-int:define-hash-table-test 'tc-eq-test #'tc-eq #'pvs-sxhash) >+#+sbcl >+(sb-int:define-hash-table-test 'strong-tc-eq-test #'strong-tc-eq #'pvs-sxhash) >diff -Naur pvs4.2-orig/src/WS1S/ix86_64-Linux/Makefile pvs4.2-sbcl/src/WS1S/ix86_64-Linux/Makefile >--- pvs4.2-orig/src/WS1S/ix86_64-Linux/Makefile 1970-01-01 00:00:00.000000000 +0000 >+++ pvs4.2-sbcl/src/WS1S/ix86_64-Linux/Makefile 2009-03-24 18:56:40.000000000 +0000 >@@ -0,0 +1,64 @@ >+ifneq (,) >+This makefile requires GNU Make. >+endif >+ >+BDD = ../mona/BDD >+DFA = ../mona/DFA >+UTILS = ../mona/Mem >+INCLUDES = -I$(BDD) -I$(DFA) -I$(UTILS) >+LD = gcc >+LDFLAGS = -shared -L./ >+CC = gcc >+CFLAGS += -fPIC -D_POSIX_SOURCE -DSYSV $(INCLUDES) >+XCFLAGS = -O >+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 >+ >+.SUFFIXES: >+.SUFFIXES: .c .o >+.c.o : ; $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@ >+ >+all : ws1s.so >+ >+ws1s_extended_interface.o : ../ws1s_extended_interface.c >+ $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@ >+ >+ws1s.so : ${obj} >+ $(LD) ../ws1s-ld-table $(LDFLAGS) -o ws1s.so ${obj} >+ >+bdd.o: bdd.c bdd.h bdd_internal.h >+bdd_double.o: bdd_double.c bdd.h bdd_internal.h >+bdd_external.o: bdd_external.c bdd_external.h mem.h >+bdd_manager.o: bdd_manager.c bdd.h bdd_internal.h >+hash.o: hash.c mem.h hash.h >+bdd_dump.o: bdd_dump.c bdd_dump.h >+bdd_trace.o: bdd_trace.c bdd.h bdd_internal.h >+bdd_cache.o: bdd_cache.c bdd.h bdd_internal.h >+ >+analyze.o: analyze.c dfa.h mem.h >+prefix.o: prefix.c dfa.h mem.h >+product.o: product.c dfa.h bdd.h hash.h mem.h >+quotient.o: quotient.c dfa.h hash.h mem.h >+basic.o: basic.c dfa.h mem.h >+external.o: external.c dfa.h bdd_external.h mem.h >+makebasic.o: makebasic.c dfa.h bdd_internal.h >+minimize.o: minimize.c dfa.h hash.h mem.h >+printdfa.o: printdfa.c dfa.h mem.h >+project.o: project.c dfa.h hash.h mem.h >+dfa.o: dfa.c dfa.h bdd.h hash.h mem.h >+ >+dlmalloc.o: dlmalloc.c dlmalloc.h >+mem.o: mem.c dlmalloc.h >+ >+clean : >+ rm -f *.o *.a *.so >diff -Naur pvs4.2-orig/src/WS1S/ix86-Linux/Makefile pvs4.2-sbcl/src/WS1S/ix86-Linux/Makefile >--- pvs4.2-orig/src/WS1S/ix86-Linux/Makefile 2007-07-02 20:07:40.000000000 +0000 >+++ pvs4.2-sbcl/src/WS1S/ix86-Linux/Makefile 2009-03-24 18:56:17.000000000 +0000 >@@ -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 > > .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 -Naur pvs4.2-orig/src/WS1S/lisp/dfa-foreign-sbcl.lisp pvs4.2-sbcl/src/WS1S/lisp/dfa-foreign-sbcl.lisp >--- pvs4.2-orig/src/WS1S/lisp/dfa-foreign-sbcl.lisp 1970-01-01 00:00:00.000000000 +0000 >+++ pvs4.2-sbcl/src/WS1S/lisp/dfa-foreign-sbcl.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -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))) >diff -Naur pvs4.2-orig/src/WS1S/lisp/symtab.lisp pvs4.2-sbcl/src/WS1S/lisp/symtab.lisp >--- pvs4.2-orig/src/WS1S/lisp/symtab.lisp 2007-07-02 20:07:39.000000000 +0000 >+++ pvs4.2-sbcl/src/WS1S/lisp/symtab.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -81,7 +81,7 @@ > (let* ((free (symtab-freevars symtab)) > (size (length free)) > (offsets (make-array size :element-type 'fixnum)) >- (fvars (make-array size :element-type 'string)) >+ (fvars (make-array size :element-type 'string :initial-element "")) > (types (make-string size)) > (i 0)) > (mapc #'(lambda (bndng) >diff -Naur pvs4.2-orig/src/WS1S/lisp/ws1s-strategy.lisp pvs4.2-sbcl/src/WS1S/lisp/ws1s-strategy.lisp >--- pvs4.2-orig/src/WS1S/lisp/ws1s-strategy.lisp 2007-07-02 20:07:39.000000000 +0000 >+++ pvs4.2-sbcl/src/WS1S/lisp/ws1s-strategy.lisp 2009-03-24 18:56:17.000000000 +0000 >@@ -193,7 +193,7 @@ > (loop* 0 (emptyset-operator)))) > > (defun ws1s-automaton-output (p num fvars offsets) >- (format t "~2%Free vars:~2%" fvars) >+ (format t "~2%Free vars:~{ ~s~}~2%" fvars) > (dfa-print p num fvars offsets) > (format t "~%")) >
You cannot view the attachment while viewing its details because your browser does not support IFRAMEs.
View the attachment on a separate page
.
View Attachment As Diff
View Attachment As Raw
Actions:
View
|
Diff
Attachments on
bug 257679
:
180966
|
180968
|
180987
|
182421
|
186061
|
186211
|
186212
|
186214
| 186215 |
186217