# workaround https://bugzilla.redhat.com/1268054 %{?!_texmf_main:%global _texmf_main %{_datadir}/texmf} Name: pvs-sbcl Version: 6.0 Release: 38%{?dist} Summary: Interactive theorem prover from SRI Group: Applications/Engineering License: GPLv2+ and BSD and Public Domain URL: http://pvs.csl.sri.com/ # SRI no longer provides source tarballs. Generate one from git as follows: # git clone https://github.com/samowre/PVS.git pvs-6.0 # cd pvs-6.0 # git reset --hard 42a7aae6c6d477dd2c25b846757274176092b08d # rm -fr .git* # find . -name .cvsignore | xargs rm -f # cd .. # tar cvJf pvs-6.0.tar.xz pvs-6.0 Source0: pvs-%{version}.tar.xz Source1: http://pvs.csl.sri.com/doc/pvs-prelude.pdf Source2: http://pvs.csl.sri.com/doc/interpretations.pdf Source3: http://pvs.csl.sri.com/papers/csl-97-2/csl-97-2.ps.gz Source4: http://pvs.csl.sri.com/papers/csl-93-9/csl-93-9.ps.gz Source5: pvs-sbcl.desktop # This patch will not be sent upstream. It adapts the SBCL support to the # needs of SELinux-enabled Fedora systems, links against the system mona # library instead of building the included sources, and enables building on # architectures that the original sources do not support. Patch0: pvs-fedora.patch # This patch was sent upstream 20 Jan 2012. It adapts to the changed number # of bits in a fixnum, starting with SBCL 1.0.53. Patch1: pvs-hashfn.patch # This patch was sent upstream 20 Jan 2012. It fixes a case where a relative # path is passed to a function that expects an absolute path, thereby breaking # the chmod function Patch2: pvs-chmod.patch # Workaround http://bugzilla.redhat.com/886158 Patch3: pvs-makeindex.patch # This patch was sent upstream 22 Feb 2013. It fixes processing of Unicode # symbols in the language documentation. Patch4: pvs-unicode.patch # This patch was sent upstream 22 Feb 2013. It removes an obsolete workaround # for a missing glibc function; the workaround now fails the build. Patch5: pvs-siglongjmp.patch # This patch was sent upstream 10 Mar 2014. It simplifies the file-exists-p # function to no longer call sb-impl::remove-backslashes, which was renamed in # SBCL 1.1.16. Patch6: pvs-remove-backslashes.patch BuildRequires: automake BuildRequires: desktop-file-utils BuildRequires: gcc-c++ BuildRequires: ghostscript BuildRequires: mona-devel BuildRequires: sbcl BuildRequires: texinfo-tex BuildRequires: tex(latex) BuildRequires: tex(boxedminipage.sty) BuildRequires: tex(relsize.sty) BuildRequires: tex(stmaryrd.sty) BuildRequires: tex(tocbibind.sty) BuildRequires: emacs BuildRequires: xemacs BuildRequires: xemacs-packages-extra Requires: tex(latex) Requires(postun): tex(tex) Provides: pvs = %{version}-%{release}, pvsio = %{version}-%{release} # This should match the corresponding tag in the sbcl spec ExclusiveArch: %{ix86} x86_64 ppc sparcv9 # requires the same sbcl it was built against %global sbcl_vr %(sbcl --version 2>/dev/null | cut -d' ' -f2) %if "x%{?sbcl_vr}" != "x%{nil}" Requires: sbcl = %{sbcl_vr} %else Requires: sbcl %endif %description PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover. It is intended to capture the state-of-the-art in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications. This build of PVS must be invoked as "pvs-sbcl", both to distinguish it from builds with other Common Lisp engines, and to distinguish it from /usr/sbin/pvs in the lvm2 package. %prep %setup -q -n pvs-%{version} %patch0 %patch1 %patch2 %patch3 %patch4 %patch5 %patch6 # Upstream didn't give us a configure script autoreconf -i # Fix a permission problem chmod a-x emacs/emacs-src/pvs-prover-manip.el # Fix building the language documentation ln -s ../makebnf.sty doc/language # Adapt the release notes to texi2any sed -i 's/\$(TEXI2HTML).*-nav/texi2any --html --no-number-sections/' \ doc/release-notes/Makefile %build # SBCL defaults to an external format of ASCII in mock builds, which breaks # the build when PVS tries to read Unicode-encoded files. export LANG=en_US.UTF-8 %configure make SBCLISP_HOME=%{_bindir} make SBCLISP_HOME=%{_bindir} make-release-notes # We don't want the empty emacs19 directory rm -fr emacs/emacs19 # And we also want to compile with XEmacs mkdir emacs/xemacs21 pushd emacs/xemacs21 ln -sf ../emacs-src/*.el . ln -sf ../emacs-src/ilisp/*.el . %{_bindir}/xemacs -batch -l pvs-byte-compile.el popd # Run it once to force Lisp compilation of the native interfaces bin/relocate > /dev/null ./pvs -raw <<<'(sb-ext:exit :code 0 :abort t)' # We don't want the useless copy of the sbcl binary rm -f bin/linux/runtime/sbcl # Get rid of some temporary files we no longer need rm -f doc/release-notes/pvs-release-notes.{pg,ky,tp,fn,cp,vr} # Build the documentation make -C doc/api pvs-api.pdf make -C doc/language language.pdf make -C doc/prover prover.pdf # Replace a damaged PDF file ps2pdf doc/user-guide/pvs-screen1.ps doc/user-guide/pvs-screen1.pdf touch doc/user-guide/user-guide.ind make -C doc/user-guide user-guide.pdf # No sources for the prelude docs cp -p %{SOURCE1} . # Cannot be built: needs cslreport.cls # pushd doc/interpretations # pdflatex interpretations # popd cp -p %{SOURCE2} . # Cannot be built: missing cslreport.cls # make -C doc/semantics semantics.pdf cp -p %{SOURCE3} . # Cannot be built: missing /homes/rushby/tex/prelude # make -C doc/datatypes datatypes.pdf cp -p %{SOURCE4} . # Mimic the effects of the relocate script for the installed location sed -i -e "s,^PVSPATH=.*$,PVSPATH=%{_libdir}/pvs," pvs sed -i -e "s,^PVSPATH=.*$,PVSPATH=%{_libdir}/pvs," pvsio sed -i -e "s,^PVSPATH=.*$,PVSPATH=%{_libdir}/pvs," proveit sed -i -e "s,^\$PVSPATH=.*$,\$PVSPATH=%{_libdir}/pvs," provethem %install mkdir -p $RPM_BUILD_ROOT%{_bindir} mkdir -p $RPM_BUILD_ROOT%{_libdir}/pvs/doc/release-notes mkdir -p $RPM_BUILD_ROOT%{_datadir}/applications mkdir -p $RPM_BUILD_ROOT%{_texmf_main}/tex/latex/pvs cp -a bin emacs lib pvs-tex.sub wish $RPM_BUILD_ROOT%{_libdir}/pvs cp -a doc/release-notes/pvs-release-notes.info $RPM_BUILD_ROOT%{_libdir}/pvs/doc/release-notes cp -a pvs.sty $RPM_BUILD_ROOT%{_texmf_main}/tex/latex/pvs cp -a pvs $RPM_BUILD_ROOT%{_bindir}/pvs-sbcl cp -a pvsio proveit provethem $RPM_BUILD_ROOT%{_bindir} # We don't need the make-dist or relocate scripts rm -f $RPM_BUILD_ROOT%{_libdir}/pvs/bin/make-dist rm -f $RPM_BUILD_ROOT%{_libdir}/pvs/bin/relocate # Remove a left-over make artifact rm -f $RPM_BUILD_ROOT%{_libdir}/pvs/emacs/*/.readme # Install the desktop file desktop-file-install --mode=644 --dir=$RPM_BUILD_ROOT%{_datadir}/applications \ %{SOURCE5} %clean rm -f /tmp/pvs-*.p1 %postun if [ $1 -eq 0 ]; then /usr/bin/mktexlsr update-desktop-database %{_datadir}/applications &>/dev/null ||: fi %posttrans /usr/bin/mktexlsr update-desktop-database %{_datadir}/applications &>/dev/null ||: %files %doc *.ps.gz *.pdf NOTICES README Examples doc/*.pdf %doc doc/api/pvs-api.pdf doc/language/language.pdf %doc doc/prover/prover.pdf doc/release-notes/pvs-release-notes.pdf %doc doc/user-guide/user-guide.pdf %license LICENSE %{_bindir}/* %{_libdir}/pvs %{_datadir}/applications/*.desktop %{_texmf_main}/tex/latex/pvs %changelog * Mon Apr 04 2016 Rex Dieter - 6.0-38 - rebuild (sbcl) * Mon Mar 28 2016 Jerry James - 6.0-37 - rebuild (mona) * Mon Mar 07 2016 Rex Dieter 6.0-36 - rebuild (sbcl) * Sat Mar 05 2016 Rex Dieter 6.0-35 - rebuild (sbcl) * Wed Feb 10 2016 Jerry James - 6.0-34 - rebuild (sbcl) * Thu Feb 04 2016 Fedora Release Engineering - 6.0-33 - Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild * Mon Feb 01 2016 Rex Dieter 6.0-32 - rebuild (sbcl) * Wed Nov 11 2015 Rex Dieter 6.0-31 - rebuild (sbcl) * Thu Oct 01 2015 Rex Dieter 6.0-30 - rebuild (sbcl) - workaround botched texlive.macros (#1268054) * Mon Sep 14 2015 Rex Dieter 6.0-29 - rebuild (sbcl) * Mon Jun 22 2015 Rex Dieter 6.0-28 - rebuild (sbcl) * Mon Jun 22 2015 Jerry James - 6.0-27 - Use license macro - Build an index for the user guide * Thu Jun 18 2015 Fedora Release Engineering - 6.0-26 - Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild * Thu Apr 30 2015 Rex Dieter 6.0-25 - rebuild (sbcl) * Fri Feb 13 2015 Rex Dieter 6.0-24 - rebuild (sbcl) * Sat Jan 03 2015 Rex Dieter 6.0-23 - rebuild (sbcl) * Wed Dec 17 2014 Rex Dieter 6.0-22 - rebuild (sbcl) * Thu Oct 9 2014 Jerry James - 6.0-21 - Build documentation with texi2any instead of texi2html (bz 1151213) * Thu Oct 09 2014 Rex Dieter 6.0-21 - rebuild (sbcl) * Thu Aug 21 2014 Rex Dieter 6.0-20 - rebuild (sbcl) * Sun Aug 17 2014 Fedora Release Engineering - 6.0-19 - Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild * Sat Jun 28 2014 Rex Dieter 6.0-18 - rebuild (sbcl) * Thu Jun 12 2014 Rex Dieter 6.0-17 - rebuild (sbcl) * Tue Jun 10 2014 Jerry James - 6.0-16 - rebuild (sbcl) * Sat Jun 07 2014 Fedora Release Engineering - 6.0-15 - Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild * Wed May 14 2014 Rex Dieter 6.0-14 - rebuild (sbcl) * Mon Mar 10 2014 Jerry James - 6.0-13 - Add pvs-remove-backslashes.patch to fix the build with SBCL 1.1.16 * Fri Mar 07 2014 Rex Dieter 6.0-13 - rebuild (sbcl) * Wed Jan 29 2014 Rex Dieter 6.0-12 - rebuild (sbcl) * Tue Dec 03 2013 Rex Dieter 6.0-11 - rebuild (sbcl) * Mon Nov 04 2013 Jerry James - 6.0-10 - Update -fedora patch to fix ASDF failure (bz 1026454) * Mon Nov 04 2013 Rex Dieter 6.0-10 - rebuild (sbcl) * Mon Sep 30 2013 Rex Dieter 6.0-9 - rebuild (sbcl) * Sun Sep 08 2013 Rex Dieter 6.0-8 - rebuild (sbcl) * Mon Aug 05 2013 Rex Dieter 6.0-7 - rebuild (sbcl) * Sun Aug 04 2013 Fedora Release Engineering - 6.0-6 - Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild * Wed Jul 17 2013 Petr Pisar - 6.0-5 - Perl 5.18 rebuild * Sun Jun 02 2013 Rex Dieter 6.0-4 - rebuild (sbcl) * Mon Apr 29 2013 Rex Dieter 6.0-3 - rebuild (sbcl) * Tue Feb 26 2013 Rex Dieter 6.0-2 - rebuild (sbcl) * Thu Feb 21 2013 Jerry James - 6.0-1 - New upstream release - Drop unnecessary emacs patch - Define LANG while building and add -unicode patch to get Unicode support - Add the -siglongjmp patch to fix a build failure * Wed Feb 20 2013 Rex Dieter 5.0-20 - rebuild (sbcl) * Thu Feb 14 2013 Fedora Release Engineering - 5.0-19 - Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild * Wed Jan 09 2013 Rex Dieter 5.0-18 - rebuild (sbcl) * Tue Dec 11 2012 Jerry James - 5.0-17 - Alternate fix for the index problem - Distribute the user guide * Sat Dec 08 2012 Rex Dieter 5.0-16 - rebuild (sbcl) * Fri Nov 02 2012 Rex Dieter 5.0-15 - rebuild (sbcl) * Sat Oct 27 2012 Rex Dieter 5.0-14 - rebuild (sbcl) * Tue Aug 07 2012 Rex Dieter 5.0-13 - rebuild (sbcl) * Mon Jul 23 2012 Rex Dieter 5.0-12 - rebuild (sbcl) * Sat Jul 21 2012 Fedora Release Engineering - 5.0-11 - Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild * Tue May 29 2012 Rex Dieter 5.0-10 - rebuild (sbcl) * Thu Apr 12 2012 Rex Dieter 5.0-9 - rebuild (sbcl) * Thu Apr 05 2012 Rex Dieter 5.0-8 - rebuild (sbcl) * Wed Jan 18 2012 Jerry James - 5.0-7 - rebuild (sbcl) - Adapt to new fixnum size - Fix the (chmod) function - Adapt to Emacs 24 - Minor spec file cleanups * Sat Jan 14 2012 Fedora Release Engineering - 5.0-6 - Rebuilt for https://fedoraproject.org/wiki/Fedora_17_Mass_Rebuild * Tue Dec 6 2011 Jerry James - 5.0-5 - Fix building on non-Intel architectures * Mon Nov 07 2011 Rex Dieter 5.0-4 - rebuild (sbcl) * Sat Oct 15 2011 Rex Dieter 5.0-3 - rebuild (sbcl) * Mon Aug 22 2011 Rex Dieter 5.0-2 - fix %%sbcl_vr macro usage * Sat Apr 16 2011 Jerry James - 5.0-1 - New upstream release * Wed Feb 09 2011 Fedora Release Engineering - 4.2-12.20100126svn - Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild * Wed Dec 8 2010 Jerry James - 4.2-11.20100126svn - Update patches for new SBCL * Thu Sep 30 2010 Rex Dieter - 4.2-10.20100126svn - rebuild (sbcl) * Wed Sep 29 2010 jkeating - 4.2-9.20100126svn - Rebuilt for gcc bug 634757 * Sat Sep 18 2010 Rex Dieter - 4.2-8.20100126svn - rebuild (sbcl) * Mon Aug 16 2010 Rex Dieter - 4.2-7.20100126svn - rebuild (sbcl) * Sat Jul 17 2010 Rex Dieter - 4.2-6.20100126svn - rebuild (sbcl) * Sat May 08 2010 Rex Dieter - 4.2-5.20100126svn - rebuild (sbcl) * Sat Apr 10 2010 Rex Dieter - 4.2-4.20100126svn - rebuild (sbcl) * Mon Feb 01 2010 Rex Dieter - 4.2-3.20100126svn - rebuild (sbcl) - drop Requires(post): desktop-file-utils (not needed) * Fri Jan 29 2010 Jerry James - 4.2-2.20100126svn - Update to 20100126 snapshot - Fix several Emacs bugs, including bz 553023 * Mon Jan 4 2010 Jerry James - 4.2-2.20100104svn - Update to 20100104 snapshot. - Fix mona patch. - Dump a non-executable SBCL image to avoid prelink and strip issues. - Solve the build-time hang in (X)Emacs. * Tue Dec 22 2009 Jerry James - 4.2-2.20091008svn - Attempt to solve build-time hang in (X)Emacs. - Don't fail if sbcl has not been prelinked. * Mon Dec 21 2009 Jerry James - 4.2-1.20091008svn - Initial RPM