See https://koji.fedoraproject.org/koji/buildinfo?buildID=476165 cliff's notes: ******* Building PVS image bin/linux/runtime/pvs-sbclisp /usr/bin/sbcl --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 \"bin/linux/runtime/pvs-sbclisp\" \ :toplevel (function startup-pvs)))" This is SBCL 1.1.13-1.fc21, an implementation of ANSI Common Lisp. More information about SBCL is available at <http://www.sbcl.org/>. SBCL is free software, provided as is, with absolutely no warranty. It is mostly in the public domain; some portions are provided under BSD-style licenses. See the CREDITS and COPYING files in the distribution for more information. ; loading #P"/builddir/build/BUILD/pvs-6.0/pvs.system" STYLE-WARNING: redefining COMMON-LISP:DEFCONSTANT-IF-UNBOUND in DEFMACRO ; file: /builddir/build/BUILD/pvs-6.0/pvs-config.lisp ; in: DEFUN BYE ; (QUIT :UNIX-STATUS EXIT-STATUS) ; ; caught STYLE-WARNING: ; SB-EXT:QUIT has been deprecated as of SBCL 1.0.56.55. Use SB-EXT:EXIT or ; SB-THREAD:ABORT-THREAD instead. ; ; In future SBCL versions SB-EXT:QUIT will signal a full warning at compile-time. ; ; compilation unit finished ; caught 1 STYLE-WARNING condition debugger invoked on a SB-INT:EXTENSION-FAILURE in thread #<THREAD "main thread" RUNNING {1002AC4003}>: Don't know how to REQUIRE ASDF. See also: The SBCL Manual, Variable *MODULE-PROVIDER-FUNCTIONS* The SBCL Manual, Function REQUIRE Type HELP for debugger help, or (SB-EXT:EXIT) to exit from SBCL. restarts (invokable by number or by possibly-abbreviated name): 0: [RETRY ] Retry EVAL of current toplevel form. 1: [CONTINUE] Ignore error and continue loading file "/builddir/build/BUILD/pvs-6.0/pvs.system". 2: [ABORT ] Abort loading file "/builddir/build/BUILD/pvs-6.0/pvs.system". 3: Ignore runtime option --eval "(load \"pvs.system\" :verbose t)". 4: Skip rest of --eval and --load options. 5: Skip to toplevel READ/EVAL/PRINT loop. 6: [EXIT ] Exit SBCL (calling #'EXIT, killing the process). (SB-IMPL::REQUIRE-ERROR "Don't know how to ~S ~A." REQUIRE :ASDF) 0] I can say that in sbcl-1.1.13 asdf and other contrib stuff physically moved from /usr/lib/sbcl to /usr/lib/sbcl/contrib/
PVS uses a little trick to get SBCL to load native-compiled modules in preference to FASL files. With sbcl 1.1.13, that trick appears to be making SBCL look for native-compiled modules *only*. And since ASDF is distributed as a FASL, guess what? Now you can't load ASDF. I've "fixed" this by forcing ASDF to load before the trick is put into play. I'll look into finding a better fix for the problem. In the meantime, though, the pvs-sbcl package once again builds in Rawhide.