ExclusiveOS:    linux solaris macosx
ExclusiveArch:  %ix86 sparc ppc

Name:           pvs-cmucl
Version:        4.1
Release:        1%{?dist}
Summary:        The PVS Verification System, CMUCL build

Group:          Applications/Engineering
License:        GPLv2+
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-system-guide.pdf
Source2:        http://pvs.csl.sri.com/doc/pvs-language-reference.pdf
Source3:        http://pvs.csl.sri.com/doc/pvs-prover-guide.pdf
Source4:        http://pvs.csl.sri.com/doc/pvs-prelude.pdf
Source5:        http://pvs.csl.sri.com/papers/csl-97-2/csl-97-2.ps.gz
Source6:        http://pvs.csl.sri.com/papers/csl-93-9/csl-93-9.ps.gz
Source7:        http://pvs.csl.sri.com/doc/interpretations.pdf
Patch0:         pvs-4.1-make.patch
Patch1:         pvs-4.1-unused.patch
Patch2:         pvs-4.1-nth-value.patch
BuildRoot:      %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)

BuildRequires:  cmucl >= 19c
Requires:       cmucl >= 19c, info, tetex-latex, tetex-fonts
Provides:       pvs = %{version}-%{release}, pvsio = %{version}-%{release}

%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.

%prep
%setup -q -c
cp -p %{SOURCE1} %{SOURCE2} %{SOURCE3} %{SOURCE4} %{SOURCE5} %{SOURCE6} \
  %{SOURCE7} .

# Fix a problem with embedded backslashes in strings passed to Lisp.
%patch0 -p1

# Get rid of an unused variable warning
%patch1 -p1

# Newer CMU Lisps crash without this patch; I don't know why yet
%patch2 -p1

%build
./configure CFLAGS="$RPM_OPT_FLAGS -fPIC"
make %{?_smp_mflags} CMULISP_HOME=/usr

# Mimic the effects of the relocate script
chmod u+w,a+x pvs pvsio
sed -i -e "s,^PVSPATH=.*$,PVSPATH=%{_datadir}/pvs," pvs
sed -i -e "s,^PVSPATH=.*$,PVSPATH=%{_datadir}/pvs," pvsio

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

%install
rm -rf $RPM_BUILD_ROOT
mkdir -p $RPM_BUILD_ROOT%{_bindir}
mkdir -p $RPM_BUILD_ROOT%{_datadir}/pvs/doc/release-notes
mkdir -p $RPM_BUILD_ROOT%{_datadir}/texmf/tex/latex/pvs
mv bin emacs lib pvs-tex.sub wish $RPM_BUILD_ROOT%{_datadir}/pvs
mv doc/release-notes/pvs-release-notes.info $RPM_BUILD_ROOT%{_datadir}/pvs/doc/release-notes
mv pvs.sty $RPM_BUILD_ROOT%{_datadir}/texmf/tex/latex/pvs
rm -f $RPM_BUILD_ROOT%{_datadir}/pvs/bin/relocate
mv pvs pvsio $RPM_BUILD_ROOT%{_bindir}

%clean
rm -rf $RPM_BUILD_ROOT

%post -p /usr/bin/texhash

%postun -p /usr/bin/texhash

%files
%defattr(-,root,root,-)
%doc *.pdf *.ps.gz LICENSE NOTICES README doc/* Examples
%{_bindir}/pvs*
%{_datadir}/pvs
%{_datadir}/texmf/tex/latex/pvs

%changelog
* Mon Nov  5 2007 Jerry James <loganjerry@gmail.com> - 4.1-1
- Update to 4.1

* Thu Feb 22 2007 Jerry James <Jerry.James@usu.edu> - 4.0-1
- Initial package