We've had similar issues with ACL2 (which, like PVS, is a theorem
proving system whose end users probably don't want to see comments
from the Lisp compiler). Here is some relevant ACL2 code, which might
give you ideas.
#+(or cmu sbcl)
(setq *compile-verbose* nil)
#+(or cmu sbcl)
(setq *compile-print* nil)
(defmacro with-warnings-suppressed (&rest forms)
; Keep this in sync with the handler-bind call in init.lisp. Thanks to Juho
; Snellman for the SBCL form.
; We are happy to turn off redefinition warnings because we trust that
; functions such as add-trip know what they are doing. Without this code, for
; example, :oops can cause many screens of such warnings.
(style-warning (lambda (c)
(declare (ignore c))
`(progn (setq ext:*gc-verbose* nil) ,@forms)
`(let ((compiler::*redefinition-action* :QUIET)) ,@forms)
`(let ((excl:*redefinition-warnings* nil)) ,@forms)
`(let ((custom::*suppress-check-redefinition* t)) ,@forms)
#-(or cmucl sbcl lispworks allegro clisp)
(if (cdr forms) `(progn ,@forms) (car forms)))
(defmacro with-suppression (&rest forms)
; Since "COMMON-LISP" is a package known to ACL2, a user should have permission
; to type 'common-lisp::foo (say) and not get a reader error due to a package
; lock. This macro suppresses the package lock on "COMMON-LISP" for Lisps
; where we know this is necessary, and also inhibits some warnings.
#-(or sbcl clisp) `(with-warnings-suppressed ,@forms)
(proclaim `(optimize ;; a bunch of stuff I'll spare you here...
#+sbcl (sb-ext:inhibit-warnings 3)
;; a bunch of stuff I'll spare you here...
#+sbcl ; turn off compiler notes (noisy)
(declaim (sb-ext:muffle-conditions sb-ext:compiler-note))
Received-SPF: pass (1b2kzd1.ch3.sourceforge.com: domain of gmail.com
designates 188.8.131.52 as permitted sender)
Date: Sat, 4 Oct 2008 11:24:52 -0600
From: "Jerry James" <loganjerry@...>
X-Spam-Score: -1.9 (-)
X-Spam-Report: Spam Filtering performed by mx.sourceforge.net.
See http://spamassassin.org/tag/ for more details.
-1.5 SPF_CHECK_PASS SPF reports sender host as permitted sender for
-0.0 SPF_PASS SPF: sender matches SPF record
-0.0 DKIM_VERIFIED Domain Keys Identified Mail: signature passes
0.0 DKIM_SIGNED Domain Keys Identified Mail: message has a signature
0.2 URIBL_GREY Contains an URL listed in the URIBL greylist
-0.6 AWL AWL: From: address is in the auto white-list
X-SpamAssassin-Status: No, hits=-1.0 required=5.0
X-UTCS-Spam-Status: No, hits=-124 required=165
I have put together a port of PVS  to SBCL. One problem I haven't
figured out how to solve is how to make SBCL stop chattering while
developing an interactive proof. I get lots of messages about
unreachable code being deleted, along with complaints about being
unable to open code various operations due to lack of type
information. The end user doesn't want to see these. I am invoking
SBCL with the option --noinform. I don't want to use --noprint or
--disable-debugger, because PVS users are accustomed to having those
facilities available. How do I stop just the unreachable code and
missing type information messages? Thanks.
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
Sbcl-help mailing list