Name: pvs-sbcl
Version: 5.0
Release: 4%{?dist}
Summary: Interactive theorem prover from SRI
Group: Applications/Engineering
License: GPLv2+ and BSD and Public Domain
URL: http://pvs.csl.sri.com/
Source0: http://pvs.csl.sri.com/download-open/pvs-%{version}-source.tgz
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
BuildRequires: automake
BuildRequires: desktop-file-utils
BuildRequires: ghostscript
BuildRequires: mona-devel
BuildRequires: sbcl
BuildRequires: texi2html
BuildRequires: texinfo-tex
BuildRequires: tex(latex)
BuildRequires: emacs
BuildRequires: emacs-el
BuildRequires: xemacs-devel
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 /sbin/pvs in
the lvm2 package.
%prep
%setup -q -c
%patch0
# Upstream didn't give us a configure script
autoreconf -i
# Fix a permission problem
chmod a-x emacs/emacs-src/pvs-prover-manip.el
%build
%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
echo -e '(sb-ext:quit :recklessly-p t)' | ./pvs -raw
# 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
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
rm -rf $RPM_BUILD_ROOT
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 -rf $RPM_BUILD_ROOT
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
%defattr(-,root,root,-)
%doc *.ps.gz *.pdf LICENSE NOTICES README Examples
%doc doc/PVSio-2.d.pdf doc/api/pvs-api.pdf
%doc doc/language/language.pdf
%doc doc/prover/prover.pdf doc/release-notes/pvs-release-notes.pdf
%{_bindir}/*
%{_libdir}/pvs
%{_datadir}/applications/*.desktop
%{_texmf_main}/tex/latex/pvs
%changelog
* 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