# workaround https://bugzilla.redhat.com/1268054
%{?!_texmf_main:%global _texmf_main %{_datadir}/texmf}
Name: pvs-sbcl
Version: 6.0
Release: 37%{?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 Mar 28 2016 Jerry James <loganjerry@gmail.com> - 6.0-37
- rebuild (mona)
* Mon Mar 07 2016 Rex Dieter <rdieter@fedoraproject.org> 6.0-36
- rebuild (sbcl)
* Sat Mar 05 2016 Rex Dieter <rdieter@fedoraproject.org> 6.0-35
- rebuild (sbcl)
* Wed Feb 10 2016 Jerry James <loganjerry@gmail.com> - 6.0-34
- rebuild (sbcl)
* Thu Feb 04 2016 Fedora Release Engineering <releng@fedoraproject.org> - 6.0-33
- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
* Mon Feb 01 2016 Rex Dieter <rdieter@fedoraproject.org> 6.0-32
- rebuild (sbcl)
* Wed Nov 11 2015 Rex Dieter <rdieter@fedoraproject.org> 6.0-31
- rebuild (sbcl)
* Thu Oct 01 2015 Rex Dieter <rdieter@fedoraproject.org> 6.0-30
- rebuild (sbcl)
- workaround botched texlive.macros (#1268054)
* Mon Sep 14 2015 Rex Dieter <rdieter@fedoraproject.org> 6.0-29
- rebuild (sbcl)
* Mon Jun 22 2015 Rex Dieter <rdieter@fedoraproject.org> 6.0-28
- rebuild (sbcl)
* Mon Jun 22 2015 Jerry James <loganjerry@gmail.com> - 6.0-27
- Use license macro
- Build an index for the user guide
* Thu Jun 18 2015 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 6.0-26
- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild
* Thu Apr 30 2015 Rex Dieter <rdieter@fedoraproject.org> 6.0-25
- rebuild (sbcl)
* Fri Feb 13 2015 Rex Dieter <rdieter@fedoraproject.org> 6.0-24
- rebuild (sbcl)
* Sat Jan 03 2015 Rex Dieter <rdieter@fedoraproject.org> 6.0-23
- rebuild (sbcl)
* Wed Dec 17 2014 Rex Dieter <rdieter@fedoraproject.org> 6.0-22
- rebuild (sbcl)
* Thu Oct 9 2014 Jerry James <loganjerry@gmail.com> - 6.0-21
- Build documentation with texi2any instead of texi2html (bz 1151213)
* Thu Oct 09 2014 Rex Dieter <rdieter@fedoraproject.org> 6.0-21
- rebuild (sbcl)
* Thu Aug 21 2014 Rex Dieter <rdieter@fedoraproject.org> 6.0-20
- rebuild (sbcl)
* Sun Aug 17 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 6.0-19
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
* Sat Jun 28 2014 Rex Dieter <rdieter@fedoraproject.org> 6.0-18
- rebuild (sbcl)
* Thu Jun 12 2014 Rex Dieter <rdieter@fedoraproject.org> 6.0-17
- rebuild (sbcl)
* Tue Jun 10 2014 Jerry James <loganjerry@gmail.com> - 6.0-16
- rebuild (sbcl)
* Sat Jun 07 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 6.0-15
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
* Wed May 14 2014 Rex Dieter <rdieter@fedoraproject.org> 6.0-14
- rebuild (sbcl)
* Mon Mar 10 2014 Jerry James <loganjerry@gmail.com> - 6.0-13
- Add pvs-remove-backslashes.patch to fix the build with SBCL 1.1.16
* Fri Mar 07 2014 Rex Dieter <rdieter@fedoraproject.org> 6.0-13
- rebuild (sbcl)
* Wed Jan 29 2014 Rex Dieter <rdieter@fedoraproject.org> 6.0-12
- rebuild (sbcl)
* Tue Dec 03 2013 Rex Dieter <rdieter@fedoraproject.org> 6.0-11
- rebuild (sbcl)
* Mon Nov 04 2013 Jerry James <loganjerry@gmail.com> - 6.0-10
- Update -fedora patch to fix ASDF failure (bz 1026454)
* Mon Nov 04 2013 Rex Dieter <rdieter@fedoraproject.org> 6.0-10
- rebuild (sbcl)
* Mon Sep 30 2013 Rex Dieter <rdieter@fedoraproject.org> 6.0-9
- rebuild (sbcl)
* Sun Sep 08 2013 Rex Dieter <rdieter@fedoraproject.org> 6.0-8
- rebuild (sbcl)
* Mon Aug 05 2013 Rex Dieter <rdieter@fedoraproject.org> 6.0-7
- rebuild (sbcl)
* Sun Aug 04 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 6.0-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild
* Wed Jul 17 2013 Petr Pisar <ppisar@redhat.com> - 6.0-5
- Perl 5.18 rebuild
* Sun Jun 02 2013 Rex Dieter <rdieter@fedoraproject.org> 6.0-4
- rebuild (sbcl)
* Mon Apr 29 2013 Rex Dieter <rdieter@fedoraproject.org> 6.0-3
- rebuild (sbcl)
* Tue Feb 26 2013 Rex Dieter <rdieter@fedoraproject.org> 6.0-2
- rebuild (sbcl)
* Thu Feb 21 2013 Jerry James <loganjerry@gmail.com> - 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 <rdieter@fedoraproject.org> 5.0-20
- rebuild (sbcl)
* Thu Feb 14 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 5.0-19
- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild
* Wed Jan 09 2013 Rex Dieter <rdieter@fedoraproject.org> 5.0-18
- rebuild (sbcl)
* Tue Dec 11 2012 Jerry James <loganjerry@gmail.com> - 5.0-17
- Alternate fix for the index problem
- Distribute the user guide
* Sat Dec 08 2012 Rex Dieter <rdieter@fedoraproject.org> 5.0-16
- rebuild (sbcl)
* Fri Nov 02 2012 Rex Dieter <rdieter@fedoraproject.org> 5.0-15
- rebuild (sbcl)
* Sat Oct 27 2012 Rex Dieter <rdieter@fedoraproject.org> 5.0-14
- rebuild (sbcl)
* Tue Aug 07 2012 Rex Dieter <rdieter@fedoraproject.org> 5.0-13
- rebuild (sbcl)
* Mon Jul 23 2012 Rex Dieter <rdieter@fedoraproject.org> 5.0-12
- rebuild (sbcl)
* Sat Jul 21 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 5.0-11
- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
* Tue May 29 2012 Rex Dieter <rdieter@fedoraproject.org> 5.0-10
- rebuild (sbcl)
* Thu Apr 12 2012 Rex Dieter <rdieter@fedoraproject.org> 5.0-9
- rebuild (sbcl)
* Thu Apr 05 2012 Rex Dieter <rdieter@fedoraproject.org> 5.0-8
- rebuild (sbcl)
* Wed Jan 18 2012 Jerry James <loganjerry@gmail.com> - 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 <rel-eng@lists.fedoraproject.org> - 5.0-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_17_Mass_Rebuild
* Tue Dec 6 2011 Jerry James <loganjerry@gmail.com> - 5.0-5
- Fix building on non-Intel architectures
* Mon Nov 07 2011 Rex Dieter <rdieter@fedoraproject.org> 5.0-4
- rebuild (sbcl)
* Sat Oct 15 2011 Rex Dieter <rdieter@fedoraproject.org> 5.0-3
- rebuild (sbcl)
* Mon Aug 22 2011 Rex Dieter <rdieter@fedoraproject.org> 5.0-2
- fix %%sbcl_vr macro usage
* Sat Apr 16 2011 Jerry James <loganjerry@gmail.com> - 5.0-1
- New upstream release
* Wed Feb 09 2011 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 4.2-12.20100126svn
- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
* Wed Dec 8 2010 Jerry James <loganjerry@gmail.com> - 4.2-11.20100126svn
- Update patches for new SBCL
* Thu Sep 30 2010 Rex Dieter <rdieter@fedoraproject.org> - 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 <rdieter@fedoraproject.org> - 4.2-8.20100126svn
- rebuild (sbcl)
* Mon Aug 16 2010 Rex Dieter <rdieter@fedoraproject.org> - 4.2-7.20100126svn
- rebuild (sbcl)
* Sat Jul 17 2010 Rex Dieter <rdieter@fedoraproject.org> - 4.2-6.20100126svn
- rebuild (sbcl)
* Sat May 08 2010 Rex Dieter <rdieter@fedoraproject.org> - 4.2-5.20100126svn
- rebuild (sbcl)
* Sat Apr 10 2010 Rex Dieter <rdieter@fedoraproject.org> - 4.2-4.20100126svn
- rebuild (sbcl)
* Mon Feb 01 2010 Rex Dieter <rdieter@fedoraproject.org> - 4.2-3.20100126svn
- rebuild (sbcl)
- drop Requires(post): desktop-file-utils (not needed)
* Fri Jan 29 2010 Jerry James <loganjerry@gmail.com> - 4.2-2.20100126svn
- Update to 20100126 snapshot
- Fix several Emacs bugs, including bz 553023
* Mon Jan 4 2010 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 4.2-1.20091008svn
- Initial RPM