Name:           pvs-sbcl
Version:        4.2
Release:        4.20100126svn%{?dist}
Summary:        Interactive theorem prover from SRI

Group:          Applications/Engineering
License:        GPLv2+
URL:            http://pvs.csl.sri.com/
# SBCL support is only available in the post-4.2 release subversion repository.
# Use the following commands to generate the source tarball corresponding to
# this release:
#   svn export -r 5502 https://spartan.csl.sri.com/svn/public/pvs/trunk pvs-4.2
#   tar cf pvs-4.2.tar pvs-4.2
#   xz pvs-4.2.tar
Source0:        pvs-4.2.tar.xz
#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 was sent upstream on 4 Jan 2010.  Use the fancyhdr package instead
# of the obsolete fancyheadings package.  Don't make Emacs kill an already
# dead process.  Refer to the bibliography file in the sources.
Patch0:         pvs-4.2-latex.patch
# This patch was sent upstream on 4 Jan 2010.  Make a couple of minor updates
# to configure.in to allow processing by autoconf 2.62 and later.  In
# particular, the invocation of AC_INIT needs to happen sooner.
Patch1:         pvs-4.2-autoconf.patch
# This patch was sent upstream on 4 Jan 2010.  Run sbcl as 'sbcl' instead of
# 'run-sbcl.sh'.  Make source code changes required by recent versions of SBCL.
Patch2:         pvs-4.2-sbcl.patch
# This patch was sent upstream on 4 Jan 2010.  Add support for Emacs 23.
Patch3:         pvs-4.2-emacs.patch
# This patch was sent upstream on 4 Jan 2010.  Fix a few ANSI CL constructs
# that aren't quite ANSI.
Patch4:         pvs-4.2-ansi.patch
# This patch will not be sent upstream, as it is Fedora-specific.  Link with
# gcc instead of ld to get a build-id and link against libc.
Patch5:         pvs-4.2-build-id.patch
# This patch will not be sent upstream, as it is Fedora-specific.  Link
# against a system copy of the mona library, rather than compiling in the
# mona sources embedded in the PVS sources.
Patch6:         pvs-4.2-mona.patch
BuildRoot:      %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)

BuildRequires:  autoconf, sbcl, texinfo-tex, tex(latex), mona-devel
BuildRequires:  emacs, emacs-el, xemacs-devel, xemacs-packages-extra
BuildRequires:  desktop-file-utils
Requires:       tex(latex)
Requires(postun): tex(tex)
Provides:       pvs = %{version}-%{release}, pvsio = %{version}-%{release}

# requires the same version it was built against
%global sbcl_ver %(sbcl --version 2>/dev/null | cut -d' ' -f2 | cut -d- -f1)
%if "x%{?sbcl_ver}" != "x%{nil}"
Requires: sbcl = %{sbcl_ver}
%else
Requires: sbcl
%endif

# Fedora SBCL is only available on Intel platforms
ExclusiveArch:  %ix86 x86_64

%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 -n pvs-4.2
%patch0 -p1
%patch1 -p1
%patch2 -p1
%patch3 -p1
%patch4 -p1
%patch5 -p1
%patch6 -p1

autoconf

%build
%configure CFLAGS="$RPM_OPT_FLAGS -fPIC -fno-strict-aliasing"
make SBCLISP_HOME=%{_bindir}

# 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

# Now that we're done building, we don't want the devel version
rm -fr bin/*/devel

# We also don't want the useless copy of the sbcl binary
rm -f bin/*/runtime/sbcl

# 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

# Get rid of some emacs save files and CVS control files
find . -name .cvsignore -o -name \*~ | xargs rm -f

# 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
make -C doc/release-notes pvs-release-notes.info
make -C doc/release-notes pvs-release-notes.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

%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%{_datadir}/texmf/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%{_datadir}/texmf/tex/latex/pvs
cp -a pvs $RPM_BUILD_ROOT%{_bindir}/pvs-sbcl
cp -a pvsio $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}/pvs*
%{_libdir}/pvs
%{_datadir}/applications/*.desktop
%{_datadir}/texmf/tex/latex/pvs

%changelog
* Sat May 08 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