Spec URL: http://jjames.fedorapeople.org/pvs/pvs-sbcl.spec SRPM URL: http://jjames.fedorapeople.org/pvs/pvs-sbcl-4.2-1.svn20091008.fc12.src.rpm 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. This is a build with SBCL. The name was chosen so that builds with other Common Lisp engines in the future are not precluded.
Thanks for doing this! I did a quick scan of the spec file to start with, and have a few questions based on just that scan: * I think the release number should be changed. It's currently "1.svn20091008%{?dist}", but I don't think that will sort correctly with later items. As I interpret "https://fedoraproject.org/wiki/Packaging:NamingGuidelines#PreReleasePackages", it should be something like "1.20091008svn%{?dist}". I understand why you had to pull from svn, and agree with that decision, but I'm not sure that will sort well later. * In the Summary, I'd add "(PVS)" at the end, to simply the job of keyword searchers. The expanded name of PVS is more historical than reality... I think it's always referred to by its initials, not its full name. * Patch0: I think it's okay for now, but in the long term, it might be nice for there to be a build option that skips mona and uses the existing packaging system. That way it'll be easier to package for other distros, *and* it may reduce your longer-term pain as PVS changes. I'd at least send the patch to the developers, explaining why it's needed. I'm surprised at the number of "cannot be built" documents due to missing components; did you ask SRI for them? At the least, I suspect Rushby wouldn't mind releasing his "/homes/rushby/tex/prelude" as OSS, or at least enough to build one of the docs. I don't see a license issue with the spec the way it is, so I don't think that should hold up anything, but it'd be nice for the future. I fear the amount of time it took to create *this* spec. This is definitely not a program that was designed to be packaged. Eek.
A few additional random thoughts on this package: * On Fedora there's already an /sbin/pvs (provided by lvm2), and /sbin is now in many users' paths. Is this likely to cause trouble? * I see a "Provides:", that's good. Should it provide "prototype-verification-system" instead of "pvs", since "pvs" has other meanings? * It seems to me that PVS should have a desktop entry, as defined by http://standards.freedesktop.org/desktop-entry-spec/latest/ That way, people can invoke it from the GUI, and double-click on ".pvs" files to invoke things correctly. Something like this in pvs.desktop: [Desktop Entry] Version=1.0 Type=Application Name=Prototype Verification System (PVS) Comment=A verification system (a specification language integrated with support tools and a theorem prover). TryExec=pvs Exec=pvs %F # Icon=fooview MimeType=image/x-pvs; (Obviously, such a desktop entry should be submitted upstream, so that in the long term everyone will package it up & they'll maintain the desktop entry.)
Is a *really* *really* long build time expected? I've had it build overnight using "rpmbuild -ba pvs.spec". It's STILL not done, after 14+ hours, and it's still burning cycles. I'm building on dual-processor Intel(R) Pentium(R) D CPU 3.60GHz (32-bit x86), 4GiB RAM, Fedora 11, 4GiB RAM. Also, I noticed some problems related to BDDs (see below). "top" reports: PID USER PR NI VIRT RES SHR S %CPU %MEM TIME+ COMMAND 14490 dwheeler 20 0 558m 44m 14m R 98.6 1.5 327758:45 sbcl 22306 dwheeler 20 0 25984 9768 4576 R 97.6 0.3 879:42.54 emacs ... Here's the tail of the build output at this time: ========================================================= Typechecking QuotientDistributive QuotientDistributive typechecked: 9 TCCs, 0 proved, 0 subsumed, 9 unproved Typechecking QuotientIteration QuotientIteration typechecked: 7 TCCs, 0 proved, 0 subsumed, 7 unproved Typechecking PartialFunctionDefinitions PartialFunctionDefinitions typechecked: 1 TCC, 0 proved, 0 subsumed, 1 unproved Typechecking PartialFunctionComposition PartialFunctionComposition typechecked: 2 TCCs, 0 proved, 0 subsumed, 2 unproved Done typechecking the prelude ; (LIST SB-RUNTIME::UNP-FUNCTION SB-RUNTIME:*UNPARSE-STYLE* ; SB-RUNTIME:*NO-ESCAPES* SB-RUNTIME:*SB-PRINT-DEPTH* ; SB-RUNTIME:*SB-PRINT-LENGTH* SB-RUNTIME::*FORMATTING-OFF*) ; ; caught WARNING: ; undefined variable: SB-RUNTIME:*FORMATTING-OFF* ; (EVERY #'FBOUNDP PVS::*UNTYPECHECK-HOOK*) ; --> LET BLOCK ; ==> ; (MAP NIL ; (LAMBDA (#:G2) ; (LET ((SB-IMPL::PRED-VALUE #)) ; (UNLESS SB-IMPL::PRED-VALUE (RETURN-FROM #:BLOCK3 NIL)))) ; PVS::*UNTYPECHECK-HOOK*) ; ; caught WARNING: ; undefined variable: PVS::*UNTYPECHECK-HOOK* ; (SB-RUNTIME:AW-TERM SB-RUNTIME::AW) ; ; caught STYLE-WARNING: ; undefined function: SB-RUNTIME:AW-TERM ; (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::SELF STREAM SB-RUNTIME::BP :VALUE ; :UNITED-FLAG :CRS :SPACES :FORMAT) ; ; caught WARNING: ; undefined variable: SB-RUNTIME::BP ; (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::PLACE STREAM SB-RUNTIME::PLACE ; SB-RUNTIME::LINETEXT SB-RUNTIME::LINENUMBER SB-RUNTIME::CHARNUMBER) ; ; caught WARNING: ; undefined variable: SB-RUNTIME::CHARNUMBER ; (ERGO-DISKSAVE TOOLS::ESS-FILENAME :RESTART-FUNCTION ; #'(LAMBDA () ; (FORMAT T "~%~72:@<Welcome to the Ergo Support System~>~%") ; (FORMAT T "~% Version ~A ~A" *ESS-VERSION* *ESS-VERSION-DATE*) ; (FORMAT T "~% with ~A" TOOLS::ESS-STRING) ; (FORMAT T "~% in ~A" TOOLS::BUILD-PARMS) ; (FORMAT T "~% generated ~A by ~A~%~%" TOOLS::BUILD-TIME TOOLS::BUILDER) ; (SETQ TOOLS::IN-REBORN-IMAGE-P T) ; (CASE (WINDOWSYSTEM) (:X11 (UNLESS # # #)) (:X10 (WHEN # # #))))) ; ; caught STYLE-WARNING: ; undefined function: ERGO-DISKSAVE ; (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::PLACE STREAM SB-RUNTIME::PLACE ; SB-RUNTIME::LINETEXT SB-RUNTIME::LINENUMBER SB-RUNTIME::CHARNUMBER) ; ; caught WARNING: ; undefined variable: SB-RUNTIME::LINENUMBER ; ; caught WARNING: ; undefined variable: SB-RUNTIME::LINETEXT ; ; caught STYLE-WARNING: ; undefined function: SB-RUNTIME::PRINT-STRUCT ; (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::SELF STREAM SB-RUNTIME::TOKEN :KIND ; :SUBKIND :VALUE :STR-VALUE) ; ; caught WARNING: ; undefined variable: SB-RUNTIME:TOKEN ; ; compilation unit finished ; Undefined functions: ; SB-RUNTIME:AW-TERM ERGO-DISKSAVE SB-RUNTIME::PRINT-STRUCT ; Undefined variables: ; SB-RUNTIME:*FORMATTING-OFF* PVS::*UNTYPECHECK-HOOK* SB-RUNTIME::BP SB-RUNTIME::CHARNUMBER SB-RUNTIME::LINENUMBER SB-RUNTIME::LINETEXT SB-RUNTIME:TOKEN ; caught 8 WARNING conditions ; caught 8 STYLE-WARNING conditions [undoing binding stack and other enclosing state... done] [saving current Lisp image into bin/ix86-Linux/runtime/pvs-sbclisp: writing 3432 bytes from the read-only space at 0x01000000 writing 2256 bytes from the static space at 0x01100000 writing 92459008 bytes from the dynamic space at 0x09000000 done] rm /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.* rm: cannot remove `/home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.*': No such file or directory make: [bin/ix86-Linux/runtime/pvs-sbclisp] Error 1 (ignored) cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/sbcl bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/mu.so bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/bdd-sbcl.lisp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/mu-sbcl.lisp bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/ix86-Linux/ws1s.so bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/utils/ix86-Linux/b64 bin/ix86-Linux ./pvs -batch -l emacs/emacs-src/pvs-set-prelude-info.el \ -f set-prelude-files-and-regions Loading /usr/share/emacs/site-lisp/site-start.d/focus-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/php-mode-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/po-mode-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/rpm-spec-mode-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/rpmdev-init.el (source)...
Thanks for all the comments, David. Sorry to be slow responding. Darn viruses .... Comment 1: you're right about the version number. I'll fix that. There was a discussion on fedora-devel recently about not including the name of the package in its Summary field, and rpmlint complains if you do that. However, you have a good point about the expansion of PVS being purely historical. I've changed the Summary to "Interactive theorem prover from SRI". Patch0 is required for Fedora. No bundled libraries are allowed without an exception. As far as I know, other distributions have similar rules, so I don't see the point in making Patch0 optional. Furthermore, the PVS copy of mona has not kept up with upstream. There are multiple bug fixes in the current mona release that have never been copied over to the PVS version. (This is exactly the reason for the "no bundled libraries" rule, in fact.) I have, in fact, made Sam Owre aware that I'm doing this and why. I asked Sam for the missing documentation files at the beginning of November. He has never replied. I am not in contact with anyone else at SRI, but I suppose I could try locating John Rushby's contact information. Comment 2: I am also worried about that other "pvs". I'll make this one "pvs-sbcl". I think the current Provides is okay. /sbin/pvs is owned by the lvm2 package, which only provides these: config(lvm2) = 2.02.53-2.fc12 lvm2 = 2.02.53-2.fc12 lvm2(x86-64) = 2.02.53-2.fc12 so there is no conflict. I did the "pvs" Provides so that libraries of PVS theories can "Requires: pvs" and have that be satisfied by a PVS built by any supported Common Lisp. Thanks for the desktop entry. I have added that, with some modifications inspired by the coq desktop file. Comment 3: Do you have PVSEMACS=xemacs in your environment? If so, see http://calypso.tux.org/pipermail/xemacs-beta/2009-December/018035.html Those BDD-related messages are harmless. They are due to the way the Makefiles are set up, which assumes that you will be doing multiple builds in the same directory. You get those messages about failing to clean up the previous build on the first build ... which, of course, is the ONLY build when constructing an RPM. The total build time for me is usually 7-8 minutes, by the way. New files: http://jjames.fedorapeople.org/pvs/pvs-sbcl.spec http://jjames.fedorapeople.org/pvs/pvs-sbcl-4.2-1.20091008svn.fc12.src.rpm
Jerry James said: > Patch0 is required for Fedora. No bundled libraries are allowed without an exception. As far as I know, other distributions have similar rules, so I don't see the point in making Patch0 optional.... Ooops, I wasn't clear enough. Sorry. I would like to see the capability of patch0 eventually merged into upstream, so that builders could easily remove the PVS-unique version of mona. By "optional", I meant "see if you could get SRI to add this option to PVS, enabling the removal of its local 'mona' library, so that future builds will not require as much patching". > I asked Sam for the missing documentation files at the beginning of November. He has never replied. Okay. Not a big deal. > I think the current Provides is okay. /sbin/pvs is owned by the lvm2 package, which only provides these... Yes, there's no naming conflict of the *packages*. But if you install pvs-sbcl and lvm2, there are two files in two different executable directories with the same name: /usr/bin/pvs and /sbin/pvs. Is there a possibility that at any time someone will call the "wrong" one? > Comment 3: Do you have PVSEMACS=xemacs in your environment? If so, see http://calypso.tux.org/pipermail/xemacs-beta/2009-December/018035.html I'll have to look. I ran PVS on that system at one time, and it's possible that I didn't clean it up properly. I'll try again on a different system; if that works, then clearly it was just a bad test on my part. > The total build time for me is usually 7-8 minutes, by the way. Thanks, that info helps. 24 hours wasn't enough in my case, so clearly there is something very wrong.
I found a bug in the build. If you have a freshly-install sbcl, there hasn't been time for 'prelink' to mangle the sbcl executable. The current script assumes that prelink *has* modified sbcl, and crashes when that's not so. Here's the tail of the "rpmbuild -ba" output: checking for emacs version >= 19... found 23.1.1 checking for etags... etags checking for mkdir... mkdir checking for tar... tar checking for GNU tar version >= 1.11... found 1.22 checking for rm... rm configure: creating ./config.status config.status: creating Makefile config.status: creating pvs config.status: creating pvsio config.status: creating doc/api/Makefile config.status: creating doc/user-guide/Makefile config.status: creating doc/language/Makefile config.status: creating doc/language/pvs-doc.el config.status: creating doc/prover/Makefile + cp -p /usr/bin/sbcl . + prelink -u ./sbcl prelink: ./sbcl does not have .gnu.prelink_undo section error: Bad exit status from /var/tmp/rpm-tmp.5D7Okc (%build)
I changed the "prelink" line to: prelink -u ./sbcl || true and re-ran "rpmbuild -ba pvs-sbcl.spec". Again, after more than 12 hours it's stuck. I did a "set | grep PVS" ; this system doesn't have *any* environment variables with "PVS" in the name. So that can't be the problem. Again, it's a 32-bit system. I suspect that this build doesn't work on 32-bit systems. Don't know why. ================================= ; (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::SELF STREAM SB-RUNTIME::TOKEN :KIND ; :SUBKIND :VALUE :STR-VALUE) ; ; caught WARNING: ; undefined variable: SB-RUNTIME:TOKEN ; ; compilation unit finished ; Undefined functions: ; SB-RUNTIME:AW-TERM ERGO-DISKSAVE SB-RUNTIME::PRINT-STRUCT ; Undefined variables: ; SB-RUNTIME:*FORMATTING-OFF* PVS::*UNTYPECHECK-HOOK* SB-RUNTIME::BP SB-RUNTIME::CHARNUMBER SB-RUNTIME::LINENUMBER SB-RUNTIME::LINETEXT SB-RUNTIME:TOKEN ; caught 8 WARNING conditions ; caught 8 STYLE-WARNING conditions [undoing binding stack and other enclosing state... done] [saving current Lisp image into bin/ix86-Linux/runtime/pvs-sbclisp: writing 3432 bytes from the read-only space at 0x01000000 writing 2256 bytes from the static space at 0x01100000 writing 92459008 bytes from the dynamic space at 0x09000000 done] rm /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.* rm: cannot remove `/home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.*': No such file or directory make: [bin/ix86-Linux/runtime/pvs-sbclisp] Error 1 (ignored) cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/sbcl bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/mu.so bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/bdd-sbcl.lisp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/mu-sbcl.lisp bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/ix86-Linux/ws1s.so bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/utils/ix86-Linux/b64 bin/ix86-Linux ./pvs -batch -l emacs/emacs-src/pvs-set-prelude-info.el \ -f set-prelude-files-and-regions Loading /usr/share/emacs/site-lisp/site-start.d/focus-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/php-mode-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/po-mode-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/rpm-spec-mode-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/rpmdev-init.el (source)...
mind you, the prelink hackery shouldn't be required in any mock/koji builds (only on live prelinked systems).
Comment 5: I did tell Sam Owre that I was doing this. The comment in the spec file about not sending it upstream is therefore not completely accurate; I just don't expect upstream to apply it. They are concentrated on providing a single download for researchers to grab, unpack, and get to work. Finding dependencies would just complicate matters for them. I renamed the binary from pvs to pvs-sbcl to avoid a name collision (see my response to comment 2 in comment 4). So when I talked about the Provide, I was really only talking about the Provide, not the binary name. The build hang has nothing to do with 32-bit vs. 64-bit systems, although I have never seen that hang with 64-bit Emacs (but have with 64-bit XEmacs). The problem is that (X)Emacs is forking off a subprocess to run PVS, but isn't noticing when that process exits, and therefore waits forever. Stephen Turnbull believes that this is a bug in X (see the URL in comment 4). In any case, I believe I have found a workaround to the problem. Briefly, I'm replacing (sit-for 1), which doesn't always notice changes in process status, with (accept-process-output nil 1), which does. Comments 6 through 8: I have applied the "|| true" change to the spec file to avoid killing the build with an unprelinked sbcl binary. New URLs: http://jjames.fedorapeople.org/pvs/pvs-sbcl.spec http://jjames.fedorapeople.org/pvs/pvs-sbcl-4.2-2.20091008svn.fc12.src.rpm
Sadly, the workaround doesn't seem to work around. It still hangs, same place, when trying to build PVS. I fired up another build for "pvs-sbcl-4.2-2.20091008svn.fc12.src.rpm" (per comment 9 ), but it hangs the same spot. I don't know why this happens, but I've put some details below in the hope that they help. The rpmbuild hangs after printing this: ; caught STYLE-WARNING: ; undefined function: SB-RUNTIME::PRINT-STRUCT ; (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::SELF STREAM SB-RUNTIME::TOKEN :KIND ; :SUBKIND :VALUE :STR-VALUE) ; ; caught WARNING: ; undefined variable: SB-RUNTIME:TOKEN ; ; compilation unit finished ; Undefined functions: ; SB-RUNTIME:AW-TERM ERGO-DISKSAVE SB-RUNTIME::PRINT-STRUCT ; Undefined variables: ; SB-RUNTIME:*FORMATTING-OFF* PVS::*UNTYPECHECK-HOOK* SB-RUNTIME::BP SB-RUNTIME::CHARNUMBER SB-RUNTIME::LINENUMBER SB-RUNTIME::LINETEXT SB-RUNTIME:TOKEN ; caught 8 WARNING conditions ; caught 8 STYLE-WARNING conditions [undoing binding stack and other enclosing state... done] [saving current Lisp image into bin/ix86-Linux/runtime/pvs-sbclisp: writing 3432 bytes from the read-only space at 0x01000000 writing 2256 bytes from the static space at 0x01100000 writing 92459008 bytes from the dynamic space at 0x09000000 done] rm /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.* rm: cannot remove `/home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.*': No such file or directory make: [bin/ix86-Linux/runtime/pvs-sbclisp] Error 1 (ignored) cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/sbcl bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/mu.so bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/bdd-sbcl.lisp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/mu-sbcl.lisp bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/ix86-Linux/ws1s.so bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/utils/ix86-Linux/b64 bin/ix86-Linux ./pvs -batch -l emacs/emacs-src/pvs-set-prelude-info.el \ -f set-prelude-files-and-regions Loading /usr/share/emacs/site-lisp/site-start.d/focus-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/php-mode-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/po-mode-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/rpm-spec-mode-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/rpmdev-init.el (source)... {and there it sits.} "top" shows that emacs is outrageously busy. When I did the rpmbuild this time it's process 30005 that is busy busy busy; here are extracts from "ps -ef -H --width 99999": dwheeler 29178 29115 0 15:33 pts/0 00:00:00 rpmbuild -ba pvs-sbcl.spec dwheeler 29279 29178 0 15:33 pts/0 00:00:00 /bin/sh -e /var/tmp/rpm-tmp.ftYHYX dwheeler 29829 29279 0 15:33 pts/0 00:00:00 make SBCLISP_HOME=/home/dwheeler/rpmbuild/BUILD/pvs-4.2 PVSPATH=/home/dwheeler/rpmbuild/BUILD/pvs-4.2/ dwheeler 29999 29829 0 16:25 pts/0 00:00:00 /bin/sh ./pvs -batch -l emacs/emacs-src/pvs-set-prelude-info.el -f set-prelude-files-and-regions dwheeler 30005 29999 98 16:25 pts/0 00:29:32 emacs -batch -load /home/dwheeler/rpmbuild/BUILD/pvs-4.2/emacs/go-pvs.el -l emacs/emacs-src/pvs-set-prelude-info.el -f set-prelude-files-and-regions dwheeler 30006 30005 0 16:25 ? 00:00:00 /home/dwheeler/rpmbuild/BUILD/pvs-4.2/bin/ix86-Linux/devel/pvs-sbclisp --noinform --no-userinit The incessantly-busy 'emacs' process 30005 has fired off a "pvs-sbclisp" process. I used gdb to try to get some backtrace information with 'gdb /usr/bin/emacs 30005'; gdb then told me to load the debug libraries by doing: yum --enablerepo='*-debuginfo' install /usr/lib/debug/.build-id/80/ba91d6689ccf229be06e5e2d828cd9e95dc65b.debug debuginfo-install alsa-lib-1.0.20-1.fc11.i586 atk-1.25.2-2.fc11.i586 bzip2-libs-1.0.5-5.fc11.i586 cairo-1.8.8-1.fc11.i586 dbus-libs-1.2.12-2.fc11.i586 e2fsprogs-libs-1.41.4-12.fc11.i586 expat-2.0.1-6.i586 fontconfig-2.7.1-1.fc11.i586 freetype-2.3.9-5.fc11.i586 giflib-4.1.6-2.fc11.i586 glib2-2.20.4-1.fc11.i586 glibc-2.10.1-4.i686 gtk2-2.16.5-1.fc11.i586 libICE-1.0.4-7.fc11.i586 libSM-1.1.0-4.fc11.i586 libX11-1.2.2-1.fc11.i586 libXau-1.0.4-5.fc11.i586 libXcomposite-0.4.0-7.fc11.i586 libXcursor-1.1.9-4.fc11.i586 libXdamage-1.1.1-6.fc11.i586 libXext-1.0.99.1-2.fc11.i586 libXfixes-4.0.3-5.fc11.i586 libXft-2.1.13-2.fc11.i586 libXi-1.2.1-1.fc11.i586 libXinerama-1.0.3-4.fc11.i586 libXpm-3.5.7-5.fc11.i586 libXrandr-1.2.99.4-3.fc11.i586 libXrender-0.9.4-5.fc11.i586 libattr-2.4.43-3.fc11.i586 libcap-2.16-4.fc11.1.i586 libcroco-0.6.2-2.fc11.i586 libgsf-1.14.11-3.fc11.i586 libjpeg-6b-45.fc11.i586 libotf-0.9.9-3.fc11.i586 libpng-1.2.37-1.fc11.i586 librsvg2-2.26.0-1.fc11.i586 libselinux-2.0.80-1.fc11.i586 libtiff-3.8.2-14.fc11.i586 libxcb-1.2-4.fc11.i586 libxml2-2.7.3-3.fc11.i586 m17n-lib-1.5.5-1.fc11.i586 ncurses-libs-5.7-2.20090207.fc11.i586 pango-1.24.5-1.fc11.i586 pixman-0.14.0-2.fc11.i586 zlib-1.2.3-22.fc11.i58 So I did that. Here's the result of "list" command: (gdb) list 5153 clear_input_pending (); 5154 QUIT; 5155 } 5156 5157 return got_some_input; 5158 } 5159 ^L 5160 /* Given a list (FUNCTION ARGS...), apply FUNCTION to the ARGS. */ 5161 5162 static Lisp_Object and here's a backtrace, with local variable info: (gdb) bt full #0 0x081c1e64 in wait_reading_process_output (time_limit=-1, microsecs=0, read_kbd=0, do_display=0, wait_for_cell=138051073, wait_proc=0x0, just_wait_proc=0) at process.c:5158 channel = 0 nfds = 0 Available = {fds_bits = {0 <repeats 32 times>}} Connecting = {fds_bits = {0 <repeats 32 times>}} check_connect = 0 check_delay = 0 no_avail = 0 xerrno = 2 proc = -1 timeout = {tv_sec = 0, tv_usec = 0} end_time = {tv_sec = 1261522014, tv_usec = 51076} wait_channel = -1 got_some_input = 0 #1 0x081c395b in Faccept_process_output (process=138051073, seconds=138051073, millisec=0, just_this_one=138051073) at process.c:4211 secs = 0 usecs = 0 #2 0x08186ad6 in Feval (form=160954061) at eval.c:2386 numargs = <value optimized out> argvals = {138051073, 138051073, 138051073, 138051073, 141037869, 137730968, 1, 1} args_left = 138051073 i = 4 fun = <value optimized out> val = <value optimized out> original_fun = 138248977 original_args = 138051073 funcar = <value optimized out> backtrace = {next = 0xbfda33e0, function = 0xbfda3328, args = 0xbfda32f0, nargs = 0, evalargs = 1 '\1', debug_on_exit = 0 '\0'} #3 0x08186d8d in Fprogn (args=160954069) at eval.c:450 val = <value optimized out> #4 0x08187720 in Fwhile (args=160954053) at eval.c:1112 test = 160954021 body = 160954069 #5 0x08186b77 in Feval (form=160954013) at eval.c:2323 numargs = 0 argvals = {-1076218560, -1076218920, -1076218924, -1, 0, 141024045, 1, 136506808} args_left = 160954053 ---Type <return> to continue, or q <return> to quit--- i = <value optimized out> fun = <value optimized out> val = <value optimized out> original_fun = 138192857 original_args = 160954053 funcar = <value optimized out> backtrace = {next = 0xbfda3490, function = 0xbfda33f8, args = 0xbfda33f4, nargs = -1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #6 0x08186d8d in Fprogn (args=161921117) at eval.c:450 val = <value optimized out> #7 0x08186b77 in Feval (form=161921141) at eval.c:2323 numargs = 0 argvals = {4, 3, 136506808, 1, 161543620, 161686483, 138051121, -726506426} args_left = 161921133 i = <value optimized out> fun = <value optimized out> val = <value optimized out> original_fun = 138190409 original_args = 161921133 funcar = <value optimized out> backtrace = {next = 0xbfda3520, function = 0xbfda34a8, args = 0xbfda34a4, nargs = -1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #8 0x08186997 in Feval (form=160953997) at eval.c:2434 fun = <value optimized out> val = <value optimized out> original_fun = 138389929 original_args = 160954005 funcar = <value optimized out> backtrace = {next = 0xbfda3610, function = 0xbfda3538, args = 0xbfda3534, nargs = -1, evalargs = 1 '\1', debug_on_exit = 0 '\0'} #9 0x08186d8d in Fprogn (args=160953989) at eval.c:450 val = <value optimized out> #10 0x08187acb in FletX (args=160953813) at eval.c:1034 varlist = 138051073 val = 161922733 elt = 160953629 #11 0x08186b77 in Feval (form=160953557) at eval.c:2323 numargs = 0 argvals = {138051073, 160955317, -1076218232, 135818103, 160955101, 0, 2, 138051097} ---Type <return> to continue, or q <return> to quit--- args_left = 160953813 i = <value optimized out> fun = <value optimized out> val = <value optimized out> original_fun = 138192833 original_args = 160953813 funcar = <value optimized out> backtrace = {next = 0xbfda36c0, function = 0xbfda3628, args = 0xbfda3624, nargs = -1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #12 0x08186d8d in Fprogn (args=160954133) at eval.c:450 val = <value optimized out> #13 0x08186b77 in Feval (form=160955293) at eval.c:2323 numargs = 0 argvals = {138051073, 1, -1076218168, 138051073, 160956933, 137730944, 2, 2} args_left = 160953541 i = <value optimized out> fun = <value optimized out> val = <value optimized out> original_fun = 138190433 original_args = 160953541 funcar = <value optimized out> backtrace = {next = 0xbfda37e0, function = 0xbfda36d8, args = 0xbfda36d4, nargs = -1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #14 0x08186d8d in Fprogn (args=160955253) at eval.c:450 val = <value optimized out> #15 0x08187918 in Flet (args=160955141) at eval.c:1090 tem = 138051073 elt = 138051073 varlist = 138051073 #16 0x08186b77 in Feval (form=160955037) at eval.c:2323 numargs = 0 argvals = {-1076217776, -1076217896, -1076217900, -1, 0, 161922517, 138190409, -726506426} args_left = 160955141 i = <value optimized out> fun = <value optimized out> val = <value optimized out> original_fun = 138192809 original_args = 160955141 funcar = <value optimized out> backtrace = {next = 0xbfda3950, function = 0xbfda37f8, ---Type <return> to continue, or q <return> to quit--- args = 0xbfda37f4, nargs = -1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #17 0x08186d8d in Fprogn (args=160955005) at eval.c:450 val = <value optimized out> #18 0x08187009 in funcall_lambda (fun=<value optimized out>, nargs=<value optimized out>, arg_vector=0x0) at eval.c:3225 val = <value optimized out> syms_left = 138051073 next = 138364953 i = 4 optional = 1 rest = 0 #19 0x0818711b in apply_lambda (fun=160954165, args=161127685, eval_flag=1) at eval.c:3156 args_left = 138051073 i = <value optimized out> tem = 138051073 #20 0x08186804 in Feval (form=161127653) at eval.c:2436 fun = 0 val = <value optimized out> original_fun = 160679793 original_args = 161127685 funcar = <value optimized out> backtrace = {next = 0xbfda3a00, function = 0xbfda3968, args = 0xbfda38a0, nargs = 4, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #21 0x08186d8d in Fprogn (args=161127757) at eval.c:450 val = <value optimized out> #22 0x08186b77 in Feval (form=161127597) at eval.c:2323 numargs = 0 argvals = {-1076217232, -1076217352, -1076217356, -1, 1073741824, 140924397, 138215665, 138051097} args_left = 161127605 i = <value optimized out> fun = <value optimized out> val = <value optimized out> original_fun = 138190409 original_args = 161127605 funcar = <value optimized out> backtrace = {next = 0xbfda3b20, function = 0xbfda3a18, args = 0xbfda3a14, nargs = -1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #23 0x08186d8d in Fprogn (args=161127765) at eval.c:450 val = <value optimized out> ---Type <return> to continue, or q <return> to quit--- #24 0x08187918 in Flet (args=161127589) at eval.c:1090 tem = 138051121 elt = 138051073 varlist = 138051073 #25 0x08186b77 in Feval (form=161127557) at eval.c:2323 numargs = 0 argvals = {138051073, 138051073, -1076217048, 1, 138051073, 161686563, -1076216952, 135819547} args_left = 161127589 i = <value optimized out> fun = <value optimized out> val = <value optimized out> original_fun = 138192809 original_args = 161127589 funcar = <value optimized out> backtrace = {next = 0xbfda3be0, function = 0xbfda3b38, args = 0xbfda3b34, nargs = -1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #26 0x08186d20 in Fprog1 (args=161127773) at eval.c:481 val = 138051073 args_left = 161127773 #27 0x08186b77 in Feval (form=161127549) at eval.c:2323 numargs = 0 argvals = {138287577, 138051073, -1076216824, 161943842, 1, 1152, -1076216840, 135784745} args_left = 161127773 i = <value optimized out> fun = <value optimized out> val = <value optimized out> original_fun = 138192617 original_args = 161127773 funcar = <value optimized out> backtrace = {next = 0xbfda3d00, function = 0xbfda3bf8, args = 0xbfda3bf4, nargs = -1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #28 0x08186d8d in Fprogn (args=161127541) at eval.c:450 val = <value optimized out> #29 0x08187918 in Flet (args=161127477) at eval.c:1090 tem = 138051073 elt = 138051073 varlist = 138051073 #30 0x08186b77 in Feval (form=161127461) at eval.c:2323 numargs = 0 argvals = {138237929, -1, -1076216524, 136506700, 4, 138486601, ---Type <return> to continue, or q <return> to quit--- -1076216552, 135749314} args_left = 161127477 i = <value optimized out> fun = <value optimized out> val = <value optimized out> original_fun = 138192809 original_args = 161127477 funcar = <value optimized out> backtrace = {next = 0xbfda3e70, function = 0xbfda3d18, args = 0xbfda3d14, nargs = -1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #31 0x08186d8d in Fprogn (args=161127453) at eval.c:450 val = <value optimized out> #32 0x08187009 in funcall_lambda (fun=<value optimized out>, nargs=<value optimized out>, arg_vector=0x0) at eval.c:3225 val = <value optimized out> syms_left = 138051073 next = 141206777 i = 3 optional = 1 rest = 0 #33 0x0818711b in apply_lambda (fun=161127941, args=161090469, eval_flag=1) at eval.c:3156 args_left = 138051073 i = <value optimized out> tem = 138051073 #34 0x08186804 in Feval (form=161090461) at eval.c:2436 fun = 0 val = <value optimized out> original_fun = 160768913 original_args = 161090469 funcar = <value optimized out> backtrace = {next = 0xbfda3f40, function = 0xbfda3e88, args = 0xbfda3dc0, nargs = 3, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #35 0x08187a1c in FletX (args=161090509) at eval.c:1028 varlist = 161090501 val = 138051073 elt = 161090453 #36 0x08186b77 in Feval (form=161090349) at eval.c:2323 numargs = 0 argvals = {38, 161956788, 17591862, 137734976, -1076215960, 138051073, -1076215976, 135813586} args_left = 161090509 ---Type <return> to continue, or q <return> to quit--- i = <value optimized out> fun = <value optimized out> val = <value optimized out> original_fun = 138192833 original_args = 161090509 funcar = <value optimized out> backtrace = {next = 0xbfda40b0, function = 0xbfda3f58, args = 0xbfda3f54, nargs = -1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #37 0x08186d8d in Fprogn (args=161088661) at eval.c:450 val = <value optimized out> #38 0x08187009 in funcall_lambda (fun=<value optimized out>, nargs=<value optimized out>, arg_vector=0x0) at eval.c:3225 val = <value optimized out> syms_left = 138051073 next = 160768793 i = 4 optional = 1 rest = 0 #39 0x0818711b in apply_lambda (fun=161088669, args=161371885, eval_flag=1) at eval.c:3156 args_left = 138051073 i = <value optimized out> tem = 160768961 #40 0x08186804 in Feval (form=161371853) at eval.c:2436 fun = 0 val = <value optimized out> original_fun = 160768841 original_args = 161371885 funcar = <value optimized out> backtrace = {next = 0xbfda41b0, function = 0xbfda40c8, args = 0xbfda4000, nargs = 4, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #41 0x08187894 in Flet (args=161371949) at eval.c:1074 tem = <value optimized out> elt = 161371845 varlist = <value optimized out> #42 0x08186b77 in Feval (form=161371837) at eval.c:2323 numargs = 0 argvals = {161686707, 138051073, -1076215352, 135658398, 137988592, 141330729, -1076215352, 135749314} args_left = 161371949 i = <value optimized out> fun = <value optimized out> ---Type <return> to continue, or q <return> to quit--- val = <value optimized out> original_fun = 138192809 original_args = 161371949 funcar = <value optimized out> backtrace = {next = 0xbfda4320, function = 0xbfda41c8, args = 0xbfda41c4, nargs = -1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #43 0x08186d8d in Fprogn (args=161371725) at eval.c:450 val = <value optimized out> #44 0x08187009 in funcall_lambda (fun=<value optimized out>, nargs=<value optimized out>, arg_vector=0x0) at eval.c:3225 val = <value optimized out> syms_left = 138051073 next = 138344865 i = 1 optional = 0 rest = 0 #45 0x0818711b in apply_lambda (fun=161372101, args=161655861, eval_flag=1) at eval.c:3156 args_left = 138051073 i = <value optimized out> tem = 138935811 #46 0x08186804 in Feval (form=161655853) at eval.c:2436 fun = 0 val = <value optimized out> original_fun = 161259201 original_args = 161655861 funcar = <value optimized out> backtrace = {next = 0xbfda44e0, function = 0xbfda4338, args = 0xbfda4270, nargs = 1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #47 0x08187632 in internal_lisp_condition_case (var=138051073, bodyform=161655853, handlers=161655893) at eval.c:1457 val = <value optimized out> c = {tag = 138051073, val = 138051073, next = 0xbfda5614, gcpro = 0x0, jmp = {{__jmpbuf = {161655888, 161655853, 161655845, -1076214696, -1797473159, 280053014}, __mask_was_saved = 0, __saved_mask = { __val = {3218752592, 3218752440, 3218752256, 58657919, 0, 138051073, 3218752472, 135749314, 138051073, 1, 3218752536, 137734976, 3218752520, 138051073, 3218752616, 135817419, 138051073, 3218752512, 138076932, 138076928, 138051073, 161259632, 3218752584, 135750692, 161259633, 138051073, 138051073, 138076928, 3218752736, 3218752552, 3218752496, 161927669}}}}, backlist = 0xbfda44e0, ---Type <return> to continue, or q <return> to quit--- handlerlist = 0xbfda56dc, lisp_eval_depth = 12, pdlcount = 61, poll_suppress_count = 1, interrupt_input_blocked = 0, byte_stack = 0xbfda48f0} h = {handler = 161655893, var = 138051073, chosen_clause = 161655813, tag = 0xbfda4374, next = 0xbfda56dc} #48 0x081876db in Fcondition_case (args=161655845) at eval.c:1398 bodyform = 161655853 handlers = 0 var = 138051073 #49 0x08186b77 in Feval (form=161655837) at eval.c:2323 numargs = 0 argvals = {161058099, 138051121, 138051121, 138051073, 138051073, 3, -1076214520, 774} args_left = 161655845 i = <value optimized out> fun = <value optimized out> val = <value optimized out> original_fun = 138192977 original_args = 161655845 funcar = <value optimized out> backtrace = {next = 0xbfda4590, function = 0xbfda44f8, args = 0xbfda44f4, nargs = -1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #50 0x08186d8d in Fprogn (args=161658733) at eval.c:450 val = <value optimized out> #51 0x08186b77 in Feval (form=161658613) at eval.c:2323 numargs = 0 argvals = {0, 0, 0, -1076214276, 161661517, 1, 5, 3} args_left = 161658677 i = <value optimized out> fun = <value optimized out> val = <value optimized out> original_fun = 138190409 original_args = 161658677 funcar = <value optimized out> backtrace = {next = 0xbfda46f0, function = 0xbfda45a8, args = 0xbfda45a4, nargs = -1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #52 0x08186d8d in Fprogn (args=161656701) at eval.c:450 val = <value optimized out> #53 0x08187009 in funcall_lambda (fun=<value optimized out>, nargs=<value optimized out>, arg_vector=0x0) at eval.c:3225 val = <value optimized out> syms_left = 138051073 ---Type <return> to continue, or q <return> to quit--- next = 1 i = 0 optional = -1076214120 rest = 135948681 #54 0x0818711b in apply_lambda (fun=161656773, args=138051073, eval_flag=1) at eval.c:3156 args_left = 138051073 i = <value optimized out> tem = 139764032 #55 0x08186804 in Feval (form=161656797) at eval.c:2436 fun = 0 val = <value optimized out> original_fun = 161251457 original_args = 138051073 funcar = <value optimized out> backtrace = {next = 0xbfda4838, function = 0xbfda4708, args = 0xbfda4650, nargs = 0, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #56 0x081a8581 in readevalloop (readcharfun=139764036, stream=<value optimized out>, sourcename=<value optimized out>, evalfun=0x8186600 <Feval>, printflag=0, unibyte=138051073, readfun=138051073, start=<value optimized out>, end=138051073) at lread.c:1785 c = <value optimized out> val = 0 b = 0x854a140 continue_reading_p = 1 whole_buffer = 1 first_sexp = <value optimized out> #57 0x081a8830 in Feval_buffer (buffer=139764036, printflag=138051073, filename=138971419, unibyte=138051073, do_allow_print=138051121) at lread.c:1846 tem = <value optimized out> buf = 139764036 #58 0x0818507d in Ffuncall (nargs=6, args=0xbfda4880) at eval.c:3059 fun = <value optimized out> original_fun = <value optimized out> funcar = <value optimized out> numargs = 5 val = <value optimized out> backtrace = {next = 0xbfda49c8, function = 0xbfda4880, args = 0xbfda4884, nargs = 5, evalargs = 0 '\0', debug_on_exit = 0 '\0'} internal_args = 0xbfda4884 ---Type <return> to continue, or q <return> to quit--- i = 0 #59 0x081bae89 in Fbyte_code (bytestr=136555643, vector=136555660, maxdepth=48) at bytecode.c:678 op = <value optimized out> stack = {pc = 0x83487a4 "\210,\16$\204\231", top = 0xbfda4894, bottom = 0xbfda4880, byte_string = 136555643, byte_string_start = 0x8348716 "\306\b!\204\22", constants = 136555660, next = 0xbfda4da0} top = 0xbfda4880 result = <value optimized out> #60 0x08186f14 in funcall_lambda (fun=<value optimized out>, nargs=<value optimized out>, arg_vector=0x0) at eval.c:3232 val = <value optimized out> syms_left = 138051073 next = <value optimized out> i = 4 optional = 1 rest = 0 #61 0x08184edb in Ffuncall (nargs=5, args=0xbfda4a20) at eval.c:3102 fun = 0 original_fun = 138428073 funcar = <value optimized out> numargs = 4 val = <value optimized out> backtrace = {next = 0xbfda4ba0, function = 0xbfda4a20, args = 0xbfda4a24, nargs = 4, evalargs = 0 '\0', debug_on_exit = 0 '\0'} internal_args = <value optimized out> i = <value optimized out> #62 0x08185279 in call4 (fn=138428073, arg1=138971419, arg2=138971419, arg3=138051073, arg4=138051121) at eval.c:2899 ret_ungc_val = 0 #63 0x081a972e in Fload (file=138967923, noerror=0, nomessage=138051121, nosuffix=138051073, must_suffix=138051073) at lread.c:1208 val = <value optimized out> stream = <value optimized out> fd = 3 found = 138971419 efound = <value optimized out> hist_file_name = 138971419 newer = -1076213160 compiled = 141274136 handler = <value optimized out> safe_p = 141014557 ---Type <return> to continue, or q <return> to quit--- tmp = {141014221, 139155901} version = 0 #64 0x08186ab3 in Feval (form=141014261) at eval.c:2390 numargs = <value optimized out> argvals = {138967923, 138051073, 138051121, 138051073, 138051073, 1, -1076232192, 139787044} args_left = 138051073 i = 5 fun = <value optimized out> val = <value optimized out> original_fun = 138180161 original_args = 141014253 funcar = <value optimized out> backtrace = {next = 0xbfda4ce8, function = 0xbfda4bb8, args = 0xbfda4b80, nargs = 4, evalargs = 1 '\1', debug_on_exit = 0 '\0'} #65 0x081a8581 in readevalloop (readcharfun=139787044, stream=<value optimized out>, sourcename=<value optimized out>, evalfun=0x8186600 <Feval>, printflag=0, unibyte=138051073, readfun=138051073, start=<value optimized out>, end=138051073) at lread.c:1785 c = <value optimized out> val = 0 b = 0x854fb20 continue_reading_p = 1 whole_buffer = 1 first_sexp = <value optimized out> #66 0x081a8830 in Feval_buffer (buffer=139787044, printflag=138051073, filename=138633667, unibyte=138051073, do_allow_print=138051121) at lread.c:1846 tem = <value optimized out> buf = 139787044 #67 0x0818507d in Ffuncall (nargs=6, args=0xbfda4d30) at eval.c:3059 fun = <value optimized out> original_fun = <value optimized out> funcar = <value optimized out> numargs = 5 val = <value optimized out> backtrace = {next = 0xbfda4e78, function = 0xbfda4d30, args = 0xbfda4d34, nargs = 5, evalargs = 0 '\0', debug_on_exit = 0 '\0'} internal_args = 0xbfda4d34 i = 0 #68 0x081bae89 in Fbyte_code (bytestr=136555643, vector=136555660, maxdepth=48) ---Type <return> to continue, or q <return> to quit--- at bytecode.c:678 op = <value optimized out> stack = {pc = 0x83487a4 "\210,\16$\204\231", top = 0xbfda4d44, bottom = 0xbfda4d30, byte_string = 136555643, byte_string_start = 0x8348716 "\306\b!\204\22", constants = 136555660, next = 0xbfda5140} top = 0xbfda4d30 result = <value optimized out> #69 0x08186f14 in funcall_lambda (fun=<value optimized out>, nargs=<value optimized out>, arg_vector=0x0) at eval.c:3232 val = <value optimized out> syms_left = 138051073 next = <value optimized out> i = 4 optional = 1 rest = 0 #70 0x08184edb in Ffuncall (nargs=5, args=0xbfda4ed0) at eval.c:3102 fun = 0 original_fun = 138428073 funcar = <value optimized out> numargs = 4 val = <value optimized out> backtrace = {next = 0xbfda5078, function = 0xbfda4ed0, args = 0xbfda4ed4, nargs = 4, evalargs = 0 '\0', debug_on_exit = 0 '\0'} internal_args = <value optimized out> i = <value optimized out> #71 0x08185279 in call4 (fn=138428073, arg1=138633667, arg2=138633667, arg3=138051073, arg4=138051121) at eval.c:2899 ret_ungc_val = 0 #72 0x081a972e in Fload (file=138614003, noerror=0, nomessage=138051121, nosuffix=138051073, must_suffix=138051073) at lread.c:1208 val = <value optimized out> stream = <value optimized out> fd = 3 found = 138633667 efound = <value optimized out> hist_file_name = 138633667 newer = 0 compiled = 141274136 handler = <value optimized out> safe_p = 2003054437 tmp = {141021573, 139155901} version = 0 ---Type <return> to continue, or q <return> to quit--- #73 0x0818507d in Ffuncall (nargs=4, args=0xbfda50c0) at eval.c:3059 fun = <value optimized out> original_fun = <value optimized out> funcar = <value optimized out> numargs = 3 val = <value optimized out> backtrace = {next = 0xbfda5218, function = 0xbfda50c0, args = 0xbfda50c4, nargs = 3, evalargs = 0 '\0', debug_on_exit = 0 '\0'} internal_args = 0xbfda5020 i = 0 #74 0x081bae89 in Fbyte_code (bytestr=136739427, vector=136739444, maxdepth=80) at bytecode.c:678 op = <value optimized out> stack = { pc = 0x832d686 "\210*\202\276\3\16Lë#\2\347\16N\206\16\2\f\211A\24@!\36S\346\16S!\36T\352\16T\314Ù$\210*\202\276\3\16LìL\2\331\26Q\16N\206\67\2\f\211A\24@\211\26F;\204B\2\333\355!\210\356\347\16F!!\210\202\276\3\16LïZ\2\360\331!\210\202\276\3\16L\361\232\203h\2\362\363!\210\202\276\3\321\364\16L\"\203y\2\365\16L!\26B\202\276\3\321\366\16L\"\203\226\2\365\325\326\16L\"!\26B\365\325\367\16L\"!\26A\202\276\3\332\16L\16H\"\211\26F\203\254\2\16FA@\f\233\24\202\276\3\332\16L\16J\"\211\26F\203\302\2\16FA@\f\233\24"..., top = 0xbfda50cc, bottom = 0xbfda50c0, byte_string = 136739427, byte_string_start = 0x832d48f "\306 \210\b\203\21", constants = 136739444, next = 0xbfda52d0} top = 0xbfda50c0 result = <value optimized out> #75 0x08186f14 in funcall_lambda (fun=<value optimized out>, nargs=<value optimized out>, arg_vector=0x0) at eval.c:3232 val = <value optimized out> syms_left = 138051073 next = <value optimized out> i = 1 optional = 0 rest = 0 #76 0x08184edb in Ffuncall (nargs=2, args=0xbfda5260) at eval.c:3102 fun = 0 original_fun = 138988161 funcar = <value optimized out> numargs = 1 val = <value optimized out> backtrace = {next = 0xbfda53a8, function = 0xbfda5260, args = 0xbfda5264, nargs = 1, evalargs = 0 '\0', debug_on_exit = 0 '\0'} ---Type <return> to continue, or q <return> to quit--- internal_args = <value optimized out> i = <value optimized out> #77 0x081bae89 in Fbyte_code (bytestr=136725691, vector=136725708, maxdepth=56) at bytecode.c:678 op = <value optimized out> stack = { pc = 0x832fdf0 "\210\16L\203\32\6\201", <incomplete sequence \334>, top = 0xbfda5264, bottom = 0xbfda5260, byte_string = 136725691, byte_string_start = 0x832f7e2 "\306 \20\307\21\n\23\310\311!\210\310\312!\210\310\313!\210\314\315!\211\34\307=\204;", constants = 136725708, next = 0xbfda5460} top = 0xbfda5260 result = <value optimized out> #78 0x08186f14 in funcall_lambda (fun=<value optimized out>, nargs=<value optimized out>, arg_vector=0x0) at eval.c:3232 val = <value optimized out> syms_left = 138051073 next = <value optimized out> i = 0 optional = 0 rest = 0 #79 0x08184edb in Ffuncall (nargs=1, args=0xbfda53f0) at eval.c:3102 fun = 0 original_fun = 138870409 funcar = <value optimized out> numargs = 0 val = <value optimized out> backtrace = {next = 0xbfda55a0, function = 0xbfda53f0, args = 0xbfda53f4, nargs = 0, evalargs = 0 '\0', debug_on_exit = 0 '\0'} internal_args = <value optimized out> i = <value optimized out> #80 0x081bae89 in Fbyte_code (bytestr=136722315, vector=136722332, maxdepth=48) at bytecode.c:678 op = <value optimized out> stack = { pc = 0x833069a "\210+\340\341\342\"\210\343\321\344\"\211\36$;\203\254", top = 0xbfda53f0, bottom = 0xbfda53f0, byte_string = 136722315, byte_string_start = 0x8330609 "\b\203\b", constants = 136722332, next = 0x0} top = 0xbfda53f0 result = <value optimized out> #81 0x08186f14 in funcall_lambda (fun=<value optimized out>, nargs=<value optimized out>, arg_vector=0x0) at eval.c:3232 ---Type <return> to continue, or q <return> to quit--- val = <value optimized out> syms_left = 138051073 next = <value optimized out> i = 0 optional = -1076210292 rest = 2682433 #82 0x0818711b in apply_lambda (fun=136722292, args=138051073, eval_flag=1) at eval.c:3156 args_left = 138051073 i = <value optimized out> tem = 138593888 #83 0x08186804 in Feval (form=138620021) at eval.c:2436 fun = 0 val = <value optimized out> original_fun = 138958121 original_args = 138051073 funcar = <value optimized out> backtrace = {next = 0x0, function = 0xbfda55b8, args = 0xbfda5500, nargs = 0, evalargs = 0 '\0', debug_on_exit = 0 '\0'} #84 0x0811d453 in top_level_2 () at keyboard.c:1368 No locals. #85 0x08184491 in internal_condition_case (bfun=0x811d440 <top_level_2>, handlers=138094225, hfun=0x8120850 <cmd_error>) at eval.c:1512 val = 0 c = {tag = 138051073, val = 138051073, next = 0xbfda5738, gcpro = 0x0, jmp = {{__jmpbuf = {138593872, 138593872, 138593888, -1076209928, -1795785607, 282255126}, __mask_was_saved = 0, __saved_mask = { __val = {27, 27, 3218757240, 135724656, 2774624, 0, 2775064, 3218757360, 3218757288, 3218757300, 1, 1, 0, 134540224, 3087905304, 0, 138377389, 138377389, 3218757320, 135444720, 138377389, 0, 0, 0, 0, 0, 2817468, 3087925248, 3218757328, 4294967295, 2772932, 134540224}}}}, backlist = 0x0, handlerlist = 0x0, lisp_eval_depth = 0, pdlcount = 2, poll_suppress_count = 1, interrupt_input_blocked = 0, byte_stack = 0x0} h = {handler = 138094225, var = 138051073, chosen_clause = 134526964, tag = 0xbfda5614, next = 0x0} #86 0x08120605 in top_level_1 () at keyboard.c:1376 No locals. #87 0x08184571 in internal_catch (tag=138090249, func=0x81205a0 <top_level_1>, arg=138051073) at eval.c:1248 c = {tag = 138090249, val = 138051073, next = 0x0, gcpro = 0x0, jmp = { {__jmpbuf = {138593872, 138593872, 138593888, -1076209656, -1795933063, 282126102}, __mask_was_saved = 0, __saved_mask = { ---Type <return> to continue, or q <return> to quit--- __val = {3218757620, 3218757768, 135396002, 3218757632, 0, 0, 0, 3253566, 0, 0, 138076928, 138051073, 138291416, 3218757608, 135750692, 138291417, 138288674, 138051073, 138076928, 6, 110, 119, 4077456, 91, 110, 119, 138051097, 58, 22, 0, 138291417, 138051073}}}}, backlist = 0x0, handlerlist = 0x0, lisp_eval_depth = 0, pdlcount = 2, poll_suppress_count = 1, interrupt_input_blocked = 0, byte_stack = 0x0} #88 0x08120681 in command_loop () at keyboard.c:1331 No locals. #89 0x08120a4a in recursive_edit_1 () at keyboard.c:953 val = <value optimized out> #90 0x08120b72 in Frecursive_edit () at keyboard.c:1015 buffer = 138051073 #91 0x08116ef2 in main (argc=0, argv=<value optimized out>) at emacs.c:1852 dummy = -1076208744 stack_bottom_variable = 8 '\b' do_initial_setlocale = 138593872 skip_args = 1 rlim = {rlim_cur = 10485760, rlim_max = 18446744073709551615} no_loadup = 0 junk = 0x0 dname_arg = 0x0 Sadness. Any ideas?
That's annoying. The workaround fixed the hang with 64-bit XEmacs, and 64-bit Emacs never seemed to have a problem. So what's up with 32-bit Emacs? I don't know, off the top of my head. Can you try setting PVSEMACS=xemacs and see if you get the same hang? If so, it really is a 32-bit versus 64-bit issue somehow, although I still fail to see how that could have anything to do with it. If not, we'll just set PVSEMACS in the spec file to make sure we don't get a hung build for now, and I'll talk to the Emacs developers to see if they have any ideas. Incidentally, there's another bug somewhere. I was just working on a proof, tried to prove a TCC, and Lisp threw an error, claiming that *EXPRS-GENERATING-ACTUAL-TCCS* is unbound. That isn't possible, since it is defvar'd in globals.lisp and given an initial value of nil. I did a setq to nil, and was able to continue with the proof, but that shouldn't have happened...
Okay, as you suggested I'm about to fire this off: export PVSEMACS=xemacs rpmbuild -ba pvs-sbcl.spec I have to run an errand, but when I return, *hopefully* this will be done. I don't know why *EXPRS-GENERATING-ACTUAL-TCCS* was unbound, but for all the world that looks like some sort of namespace issue (where the namespace used when reading globals.lisp isn't being used properly later). There's actually a remarkable number of warnings when sbcl compiles PVS; the few that I looked at seemed to be just hints about how to generate faster code, and not real issues, but it's possible that at least one of those warnings is more serious.
Drat, and double-drat. Doing "export PVSEMACS=xemacs" has a useless effect... it merely means that xemacs gets stuck in an endless loop instead of emacs. "top" reports that "xemacs" is very busy, essentially using the entire CPU: 31372 dwheeler 20 0 21724 12m 3552 R 97.3 2.5 164:51.99 xemacs Note the "TIME" value of >164minutes. Sure isn't 10 minutes. Doing a ps -ef, I see: dwheeler 30543 29115 0 19:56 pts/0 00:00:00 rpmbuild -ba pvs-sbcl.spec dwheeler 30544 29115 0 19:56 pts/0 00:01:05 tee ,pvs-results dwheeler 30645 30543 0 19:56 pts/0 00:00:00 /bin/sh -e /var/tmp/rpm-tmp.8WyTz0 dwheeler 31195 30645 0 19:57 pts/0 00:00:00 make SBCLISP_HOME=/home/dwheeler/rpmbuild/BUILD/pvs-4.2 PVSPATH=/home/dwheeler/rpmbuild/BUILD/pvs-4.2/ dwheeler 31366 31195 0 20:48 pts/0 00:00:00 /bin/sh ./pvs -batch -l emacs/emacs-src/pvs-set-prelude-info.el -f set-prelude-files-and-regions dwheeler 31372 31366 99 20:48 pts/0 02:43:13 xemacs -batch -load /home/dwheeler/rpmbuild/BUILD/pvs-4.2/emacs/go-pvs.el -l emacs/emacs-src/pvs-set-prelude-info.el -f set-prelude-files-and-regions dwheeler 31374 31372 0 20:48 ? 00:00:00 /home/dwheeler/rpmbuild/BUILD/pvs-4.2/bin/ix86-Linux/devel/pvs-sbclisp --noinform --no-userinit I don't actually *know* if this is a 32-bit vs. 64-bit issue, but IIRC you tested on 64-bit, while I'm testing on 32-bit, so it's an obvious difference in the test environment that *might* explain the difference in results. This looks like exactly the same problem as before. There is an interesting oddity, though I don't know if it's important. I though I might need to search through the build output later, so I ran the build through "tee" like this: rpmbuild -ba 2>&1 > ,pvs-results Just like last time, it reported that it was loading "rpmdev-init.el" just before it got hung, but then it reported one additional line. Its *last* line reported: Loading leim-list... (*without* a terminating newline, oddly enough.) So I got one extra line of output. I'm not sure that is significant; that may be simply because I changed (slightly) how I invoked rpmbuild. But maybe that's important. Anyway, here's the tail of the build report: ; caught STYLE-WARNING: ; undefined function: SB-RUNTIME::PRINT-STRUCT ; (SB-RUNTIME::PRINT-STRUCT SB-RUNTIME::SELF STREAM SB-RUNTIME::TOKEN :KIND ; :SUBKIND :VALUE :STR-VALUE) ; ; caught WARNING: ; undefined variable: SB-RUNTIME:TOKEN ; ; compilation unit finished ; Undefined functions: ; SB-RUNTIME:AW-TERM ERGO-DISKSAVE SB-RUNTIME::PRINT-STRUCT ; Undefined variables: ; SB-RUNTIME:*FORMATTING-OFF* PVS::*UNTYPECHECK-HOOK* SB-RUNTIME::BP SB-RUNTIME::CHARNUMBER SB-RUNTIME::LINENUMBER SB-RUNTIME::LINETEXT SB-RUNTIME:TOKEN ; caught 8 WARNING conditions ; caught 8 STYLE-WARNING conditions [undoing binding stack and other enclosing state... done] [saving current Lisp image into bin/ix86-Linux/runtime/pvs-sbclisp: writing 3432 bytes from the read-only space at 0x01000000 writing 2256 bytes from the static space at 0x01100000 writing 92459008 bytes from the dynamic space at 0x09000000 done] rm /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.* rm: cannot remove `/home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/bdd-sbcl.*': No such file or directory make: [bin/ix86-Linux/runtime/pvs-sbclisp] Error 1 (ignored) cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/sbcl bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/ix86-Linux/mu.so bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/bdd-sbcl.lisp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/BDD/mu-sbcl.lisp bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/ix86-Linux/ws1s.so bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp bin/ix86-Linux/runtime/ cp /home/dwheeler/rpmbuild/BUILD/pvs-4.2/src/utils/ix86-Linux/b64 bin/ix86-Linux ./pvs -batch -l emacs/emacs-src/pvs-set-prelude-info.el \ -f set-prelude-files-and-regions Loading /usr/share/xemacs/site-packages/lisp/site-start.d/rpmdev-init.el... Loading leim-list... I have no idea why it's getting hung.
The hangs you are experiencing all appear to be happening in the same code where I initially experienced the hang. If Stephen Turnbull is right, this is a bug in X, and if my attempted workaround doesn't do the job, then we're just sunk ... with an X build. Let's try using emacs-nox or xemacs-nox. I'll work up the necessary spec file changes tomorrow after a good night's rest.
> Let's try using emacs-nox or xemacs-nox. Agree. That's an unfortunate solution if it's long-term, but it's a reasonable short-term solution *AND* it would definitely help narrow down where the bug is. Please modify the spec so that it'll be easy to switch back to "normal" emacs or xemacs. It's my hope that using *emacs-nox is a relatively temporary solution. Your earlier patch modified "exit-pvs-process" by replacing (sit-for 1) with (accept-process-output nil 1). Although it's a nasty hack, you could instead repeatedly (1) wait for 1 second using sleep, then (2) use "system" to invoke "ps" directly and see if the process is gone. Yeah, that's a nasty hack. Might work, though.
Argh. The elisp code calls add-submenu AT COMPILE TIME! Since this function doesn't exist in (x)emacs-nox, the compilation fails. I still don't understand why the accept-process-output hack isn't working for you, though. It runs code that is supposed to check for process statuses, on both emacsen. Since it solved the problem I was having with XEmacs, I know that code is being run. I'm going to make a virtual 32-bit machine and see if I can debug the hang you're seeing. It looks like the same hang, but may not be.
I have no idea if this is related, but I found that someone had to specially patch interaction between GIMP and emacs when using emacs' sit-for. Maybe this would help?: http://github.com/pft/gimpmode/commit/296ca334d510975a5d271fb151e4250676f61ae3
I've been hunting for other reports about problems with sit-for. You may have seen all this, but perhaps I've found something you haven't seen. Anyway, I found this PVS bug report: http://pvs.csl.sri.com/cgi-bin/pvs-bug?id=440 And maybe this is useful too: http://emacs-w3m.namazu.org/ml/msg09645.html Good luck, and Merry Christmas!
While you worked on the 32-bit issue, I tried the package out on a 64-bit install. I tried 2.20091008svn.fc12 on Fedora 12 as x64_64 (64-bit), and PVS worked just fine. But I did have some questions/issues after doing it. First, my simple smoke tests look good. After building and installing, I used my trivial "mortability.pvs" file from <http://www.dwheeler.com/trusting-trust/mortality.pvs> and invoked the program as: pvs-sbcl mortality.pvs I left-clicked on the socrates_mortal claim, invoked "PVS/Prover Invocation/prove", and when the interactive prover area popped up, I typed in: (grind :rewrites ("all_men_mortal")) That proved it, so it printed "Q.E.D." and wrote the proof file "mortality.prf". Now for a few comments on the RPM packaging... I think it is CRITICALLY important that the rpm Description state something like this: Note that the main executable "pvs" has been renamed to "pvs-sbcl". *ALL* the docs say that to invoke pvs you type "pvs", but that would invoke /sbin/pvs on a Fedora system instead. That's a nasty gotcha, and since I don't think we can/should rename /sbin/pvs, I think clearly stating that up-front is necessary. A few more comments about the "Description" text. I think you should simply drop the last sentence of the RPM description (everybody improves programs as they learn stuff, nothing special here). The next-to-last sentence doesn't add much, but its mention of "formal methods" is probably useful (someone searching for "formal methods" would correctly find PVS). I would also add to the description something about SRI; that way, someone searching on "SRI" would find this too. I did an rpmlint, and got some warnings. Specifically, I did: rpmlint pvs-sbcl.spec `find .. -name 'pvs*.rpm'` and got these warnings: pvs-sbcl.x86_64: W: unstripped-binary-or-object /usr/lib64/pvs/bin/ix86_64-Linux/runtime/ws1s.so pvs-sbcl.x86_64: W: unstripped-binary-or-object /usr/lib64/pvs/bin/ix86_64-Linux/b64 pvs-sbcl.x86_64: W: unstripped-binary-or-object /usr/lib64/pvs/bin/ix86_64-Linux/runtime/mu.so pvs-sbcl.x86_64: W: executable-stack /usr/lib64/pvs/bin/ix86_64-Linux/runtime/pvs-sbclisp 2 packages and 1 specfiles checked; 0 errors, 4 warnings. These are all semi-unavoidable due to the Lisp implementation, correct? Good luck on figuring out the 32-bit issue!
Thanks for the comments. I'll address those some time tomorrow. I have figured out the problem with the 32-bit platform, and it is, in fact, a different hang than the one I was seeing on the 64-bit platform. On the 32-bit platforms, Emacs is waiting for PVS forever, because the PVS process isn't exiting. It looks like the immediate problem is that my patch to use the system Mona library isn't quite right. I don't know why this didn't manifest on the 64-bit platform (maybe it would later on during the execution). Anyway, I've got to figure out how to do this correctly now. I'll try to do that tomorrow, too.
Congrats for figuring out the 32-bit platform problem, that's great news! Sounds like it needed fixing for 64-bit as well. I can't wait for the next package revision! Good luck.
Now that I'm done making merry, I had a chance to work on this again. I found several more SBCL-specific changes that needed to be made to the PVS code base, so I've reworked the patches. Give this a try: http://jjames.fedorapeople.org/pvs/pvs-sbcl.spec http://jjames.fedorapeople.org/pvs/pvs-sbcl-4.2-2.20091229svn.fc12.src.rpm This includes changes that were checked into PVS subversion over the last couple of weeks.
Hooray!! This updated package now works on 32-bit (using Fedora 11). It builds without hanging. I also used the "mortality.pvs" demo, and PVS quickly proves "Socrates is mortal". That's good, since Socrates has been dead a long time :-). Anyway, that worked in 64-bit, now it works (again) in 32-bit. I found no rpmlint warnings in this version (at least for the 32-bit version). I did "rpmlint ./RPMS/i586/pvs-sbcl-4.2-2.20091229svn.fc11.i586.rpm ./SRPMS/pvs-sbcl-4.2-2.20091229svn.fc11.src.rpm ./SPECS/pvs-sbcl.spec" and it reported: 2 packages and 1 specfiles checked; 0 errors, 0 warnings. I'll try 64-bit Fedora 12 next; presuming that works, I'll then walk through the package guideline checklist.
This PVS also seems to work on 64-bit Fedora 12. It builds fine. There are no rpmlint warnings or errors on this one, either: rpmlint pvs-sbcl.spec ../RPMS/x86_64/pvs-sbcl-4.2-2.20091229svn.fc12.x86_64.rpm ../SRPMS/pvs-sbcl-4.2-2.20091229svn.fc12.src.rpm 2 packages and 1 specfiles checked; 0 errors, 0 warnings.
Okay, I reviewed the package using the guideline checklist at: https://fedoraproject.org/wiki/Packaging:ReviewGuidelines I have questions/issues for two points: * MUST: Every binary RPM package (or subpackage) which stores shared library files (not just symlinks) in any of the dynamic linker's default paths, must call ldconfig in %post and %postun. [10] NO. There are some files that are stored as shared library files: /usr/lib64/pvs/bin/ix86_64-Linux/runtime/ Granted, these probably aren't shared by other packages, but they MIGHT be. * MUST: If a package contains library files with a suffix (e.g. libfoo.so.1.1), then library files that end in .so (without suffix) must go in a -devel package. [20] ??? NOT SURE. There are ".so" files not in a -devel package, but it's not clear that they SHOULD be in a -devel package. Comments? Perhaps I'm misunderstanding something? There are a few things I need to do, too. I can't check the svn version at this instant (can't download), so I hope to do that soon. I also intend to do a koji build, which will answer some. Other than that, looks like we're off. Here's the guideline checklist results: * MUST: rpmlint must be run on every package. The output should be posted in the review.[1] OK. No warnings or errors. * MUST: The package must be named according to the Package Naming Guidelines. OK. * MUST: The spec file name must match the base package %{name}, in the format %{name}.spec unless your package has an exemption. [2]. OK. * MUST: The package must meet the Packaging Guidelines. OK. At least, I don't see any violations. * MUST: The package must be licensed with a Fedora approved license and meet the Licensing Guidelines. OK (GPLv2+). * MUST: The License field in the package spec file must match the actual license. [3] OK. It has the usual GPL LICENSE file. The PVS website also specifically states that it is GPL-licensed: http://pvs.csl.sri.com/download.shtml * MUST: If (and only if) the source package includes the text of the license(s) in its own file, then that file, containing the text of the license(s) for the package must be included in %doc.[4] OK. See /usr/share/doc/pvs-sbcl-4.2/LICENSE * MUST: The spec file must be written in American English. [5] OK. * MUST: The spec file for the package MUST be legible. [6] OK. * MUST: The sources used to build the package must match the upstream source, as provided in the spec URL. Reviewers should use md5sum for this task. If no upstream URL can be specified for this package, please see the Source URL Guidelines for how to deal with this. ??? I need to check this later. This package uses an SVN version, to pick up necessary patches. The spec file documents that the extraction uses: svn export -r 5477 https://spartan.csl.sri.com/svn/public/pvs/trunk pvs-4.2 I'm having trouble downloading from SVN at this moment; I'll try again later. * MUST: The package MUST successfully compile and build into binary rpms on at least one primary architecture. [7] OK. * MUST: If the package does not successfully compile, build or work on an architecture, then those architectures should be listed in the spec in ExcludeArch. Each architecture listed in ExcludeArch MUST have a bug filed in bugzilla, describing the reason that the package does not compile/build/work on that architecture. The bug number MUST be placed in a comment, next to the corresponding ExcludeArch line. [8] OK to my knowledge. I only tried x86, 32-bit and 64-bit. Koji would answer this. * MUST: All build dependencies must be listed in BuildRequires, except for any that are listed in the exceptions section of the Packaging Guidelines ; inclusion of those as BuildRequires is optional. Apply common sense. OK to my knowledge. Koji would answer this. * MUST: The spec file MUST handle locales properly. This is done by using the %find_lang macro. Using %{_datadir}/locale/* is strictly forbidden.[9] NA. Only English. * MUST: Every binary RPM package (or subpackage) which stores shared library files (not just symlinks) in any of the dynamic linker's default paths, must call ldconfig in %post and %postun. [10] NO. There are some files that are stored as shared library files: /usr/lib64/pvs/bin/ix86_64-Linux/runtime/ Granted, these probably aren't shared by other packages, but they MIGHT be. * MUST: Packages must NOT bundle copies of system libraries.[11] OK. There's a "/usr/lib64/pvs/wish", but this is a *directory* not wish itself. * MUST: If the package is designed to be relocatable, the packager must state this fact in the request for review, along with the rationalization for relocation of that specific package. Without this, use of Prefix: /usr is considered a blocker. [12] NA. * MUST: A package must own all directories that it creates. If it does not create a directory that it uses, then it should require a package which does create that directory. [13] OK. I looked at %files, looks okay. * MUST: A Fedora package must not list a file more than once in the spec file's %files listings. [14] OK. Again, %files looks okay. * MUST: Permissions on files must be set properly. Executables should be set with executable permissions, for example. Every %files section must include a %defattr(...) line. [15] The %files section has %defattr(); rpmls looks okay. * MUST: Each package must have a %clean section, which contains rm -rf %{buildroot} (or $RPM_BUILD_ROOT). [16] OK * MUST: Each package must consistently use macros. [17] OK * MUST: The package must contain code, or permissable content. [18] OK * MUST: Large documentation files must go in a -doc subpackage. (The definition of large is left up to the packager's best judgement, but is not restricted to size. Large can refer to either size or quantity). [19] NA * MUST: If a package includes something as %doc, it must not affect the runtime of the application. To summarize: If it is in %doc, the program must run properly if it is not present. [19] NA * MUST: Header files must be in a -devel package. [20] NA * MUST: Static libraries must be in a -static package. [21] NA * MUST: Packages containing pkgconfig(.pc) files must 'Requires: pkgconfig' (for directory ownership and usability). [22] NA * MUST: If a package contains library files with a suffix (e.g. libfoo.so.1.1), then library files that end in .so (without suffix) must go in a -devel package. [20] ??? NOT SURE. There are ".so" files not in a -devel package, but it's not clear that they SHOULD be in a -devel package. Comments? * MUST: In the vast majority of cases, devel packages must require the base package using a fully versioned dependency: Requires: %{name} = %{version}-%{release} [23] NA * MUST: Packages must NOT contain any .la libtool archives, these must be removed in the spec if they are built.[21] NA * MUST: Packages containing GUI applications must include a %{name}.desktop file, and that file must be properly installed with desktop-file-install in the %install section. If you feel that your packaged GUI application does not need a .desktop file, you must put a comment in the spec file with your explanation. [24] OK. This was added recently as part of the packaging process. * MUST: Packages must not own files or directories already owned by other packages. The rule of thumb here is that the first package to be installed should own the files or directories that other packages may rely upon. This means, for example, that no package in Fedora should ever share ownership with any of the files or directories owned by the filesystem or man package. If you feel that you have a good reason to own a file or directory that another package owns, then please present that at package review time. [25] OK. * MUST: At the beginning of %install, each package MUST run rm -rf %{buildroot} (or $RPM_BUILD_ROOT). [26] OK. * MUST: All filenames in rpm packages must be valid UTF-8. [27] OK. ASCII. * SHOULD: If the source package does not include license text(s) as a separate file from upstream, the packager SHOULD query upstream to include it. [28] NA * SHOULD: The description and summary sections in the package spec file should contain translations for supported Non-English languages, if available. [29] Don't, but not required. * SHOULD: The reviewer should test that the package builds in mock. [30] I'll try to do this later. * SHOULD: The package should compile and build into binary rpms on all supported architectures. [31] ??? Partly done. I used two. Mock/koji should help determine for the others. * SHOULD: The reviewer should test that the package functions as described. A package should not segfault instead of running, for example. OK. I did smoke tests for 32-bit and 64-bit. * SHOULD: If scriptlets are used, those scriptlets must be sane. This is vague, and left up to the reviewers judgement to determine sanity. [32] NA. * SHOULD: Usually, subpackages other than devel should require the base package using a fully versioned dependency. [23] NA * SHOULD: The placement of pkgconfig(.pc) files depends on their usecase, and this is usually for development purposes, so should be placed in a -devel pkg. A reasonable exception is that the main pkg itself is a devel tool not installed in a user runtime, e.g. gcc or gdb. [22] NA * SHOULD: If the package has file dependencies outside of /etc, /bin, /sbin, /usr/bin, or /usr/sbin consider requiring the package which provides the file instead of the file itself. [33] NA
I've resolved most other questions, other than the library-file items above (the 2 MUSTs), but I got a weird difference between the svn version and what you sent. First, though, the good news. Koji (scratch) build with dist-f12 worked correctly: $ koji build --scratch dist-f12 ./pvs-sbcl-4.2-2.20091229svn.fc12.src.rpm ... 1899006 build (dist-f12, pvs-sbcl-4.2-2.20091229svn.fc12.src.rpm): open (ppc04.phx2.fedoraproject.org) -> closed 0 free 0 open 3 done 0 failed 1899006 build (dist-f12, pvs-sbcl-4.2-2.20091229svn.fc12.src.rpm) completed successfully Also, silly me, the spec uses "ExclusiveArch" and I've tested both of them, so obviously we're fine in terms of architectural support. HOWEVER, when I downloaded the source code using the spec directions (including svn), I found this incredibly tiny difference: [dwheeler@eve SOURCES]$ diff -u -r pvs-4.2 ~/temp/pvs-4.2 diff -u -r pvs-4.2/lib/bitvectors/bv_mult_div_rem.pvs /home/dwheeler/temp/pvs-4.2/lib/bitvectors/bv_mult_div_rem.pvs --- pvs-4.2/lib/bitvectors/bv_mult_div_rem.pvs 2002-12-18 20:23:50.000000000 -0500 +++ /home/dwheeler/temp/pvs-4.2/lib/bitvectors/bv_mult_div_rem.pvs 2002-12-18 20:23:50.000000000 -0500 @@ -9,7 +9,7 @@ % % Author: Bart Jacobs % Started: Wednesday 24 May 00 10:59:26 bart@frustratie -% Last-modified: $Date: 2002-12-18 18:23:50 -0700 (Wed, 18 Dec 2002) $ +% Last-modified: $Date: 2002-12-18 20:23:50 -0500 (Wed, 18 Dec 2002) $ % Last-modified by: $Author: owre $ I can't see how this change makes a *difference*, but it's still a difference.
David, thanks for reviewing the package so thoroughly. The packaging guidelines say, in section 1.24, "In addition, every binary RPM package which contains shared library files (not just symlinks) in any of the dynamic linker's default paths, must call ldconfig in %post and %postun." This package does not put a shared library file in any of the dynamic linker's default paths, so this requirement is vacuously satisfied. The .so files are covered by section 1.22. Since the shared libraries are for PVS's use only, this section is also vacuously satisfied. I can't account for the timestamp difference you see, but since the time is off by 2 hours in one direction and the time zone is off by 2 hours in the other direction, they represent the same time. I live in the -0700 timezone. I'm guessing you live in the -0500 timezone.
> I can't account for the timestamp difference you see, but since the time is off by 2 hours in one direction and the time zone is off by 2 hours in the other direction, they represent the same time. You're right! They're the same time, and that text is the only "difference". That is a weird thing that svn does, but that's a clear explanation... it appears that in certain cases, svn uses the local timezone when retrieving, and thus I see a "difference" that isn't really a difference at all. Great; that means that that MUST is resolved. And I see what you mean about the .so files. You're right, those "MUST"s are vacuously satisfied. So: all requirements are met. Thank you SO MUCH for packaging PVS; this one required real work to make it 64-bit-ready, and was *tricky* for other reasons too. Great job. APPROVED.
New Package CVS Request ======================= Package Name: pvs-sbcl Short Description: Interactive theorem prover from SRI Owners: jjames Branches: F-11 F-12 InitialCC:
Hi, I've been following this review for some time now as I'm not aware of any existing self-executable CL-based packages in Fedora besides CL implementations themselves so this could well be the very first one; I would like to see things learned from the review in the wiki as I'm going to package CL stuff myself sometime in the future and I find the existing Lisp-related guidelines sparse; e.g. I'd conclude from what is written down right now that providing self-executable Lisp machines that are not the original implementations themselves is impossible, instead it looks like Lisp is treated like scripting languages in Fedora (which is - of course - utterly wrong) since the guidelines force use of cl- prefixes for both libs (OK) and programs (bad) and source code distribution only. I could be wrong here since the guidelines mentions "Libraries and Programs" in the headline but doesn't refer to the latter in the following body. Source: http://fedoraproject.org/wiki/Packaging/Lisp#Guidelines_for_Libraries_and_Programs_written_in_Common_Lisp Would you mind starting a discussion about this in fedora-devel? I'd really like to see this resolved in an official manner and make Lisp-based projects first-level citizens in Fedora.
The second sentence of: http://fedoraproject.org/wiki/Packaging/Lisp#Guidelines_for_Libraries_and_Programs_written_in_Common_Lisp is: "This document does not describe conventions and customs for application programs that are written in Common Lisp." So that document doesn't apply. To my knowledge, there are *no* special written guidelines for packaging applications *written* in Common Lisp (CL). You just follow the usual conventions for packages (adding WHICH CL implementation you used in the package name). I know that "maxima" is another packaged application written in CL, so PVS isn't unique. It might be nice to have guidelines, but someone will have to figure out good guidelines first :-).
Hi David, (In reply to comment #31) > The second sentence of: > > http://fedoraproject.org/wiki/Packaging/Lisp#Guidelines_for_Libraries_and_Programs_written_in_Common_Lisp > is: > "This document does not describe conventions and customs for application > programs that are written in Common Lisp." > So that document doesn't apply. Ooh I must have missed that - thanks for pointing that out! > To my knowledge, there are *no* special written guidelines for packaging > applications *written* in Common Lisp (CL). You just follow the usual > conventions for packages (adding WHICH CL implementation you used in the > package name). I know that "maxima" is another packaged application written in > CL, so PVS isn't unique. Didn't know 'bout that one, thanks again. > It might be nice to have guidelines, but someone will have to figure out good > guidelines first :-). The original ones seem to have been written by Spot, I wonder if he just took over those from Debian or whether he really knows about coding Lisps. Well the only "someones" in question is Fedorans who can code Lisp (or here CL in particular), right? So why not make something up?
I just started a thread to discuss the issues on fedora-devel, as requested. Let's discuss the issues there, where others can see the discussion, instead of hidden away in this bug.
cvs done.
pvs-sbcl-4.2-2.20100104svn.fc12 has been submitted as an update for Fedora 12. http://admin.fedoraproject.org/updates/pvs-sbcl-4.2-2.20100104svn.fc12
pvs-sbcl-4.2-2.20100104svn.fc11 has been submitted as an update for Fedora 11. http://admin.fedoraproject.org/updates/pvs-sbcl-4.2-2.20100104svn.fc11
David: I'd really appreciate if you'd also join the discussion Jerry started at fedora-devel :)
pvs-sbcl-4.2-2.20100104svn.fc12 has been pushed to the Fedora 12 stable repository. If problems still persist, please make note of it in this bug report.
pvs-sbcl-4.2-2.20100104svn.fc11 has been pushed to the Fedora 11 stable repository. If problems still persist, please make note of it in this bug report.