rpms/why3
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

New upstream release.

Browse source 
Add -proofgeneral subpackage.
Add desktop and AppData files.
This commit is contained in:
Jerry James 2019-10-29 08:23:16 -06:00
commit d9fe992ded
5 changed files with 136 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
sources
View file

@ -1,2 +1,2 @@
SHA512 (why3-man.tar.xz) = 8355776ac8a67a56ae7354f8fd40dc5d2057022d1035090a3e38e139fbfe3c258fe3ccbed6e333cb005e66c7b4cdbbf6580e3420170fd08384cc9b36ce5ec2a1
SHA512 (why3-1.2.0.tar.gz) = bc7dd11ef0ac80a86de9944bf4691011c6aa5f211280cbc7740ef6cfbf77657dd87106bc3197e41e404d808014bbff8fed2d209dc70deeca4566ade69cf33b5d
SHA512 (why3-1.2.1.tar.gz) = 7a5d4403bda5a9c88490d83803a6c3d30b80b9949398de6d35b92df80a90980235c014d59afb46dd1bdd3028f20252ae1f59756a3d6978228e5c8fd9aefa1b3d

43
why3.appdata.xml Normal file
View file

@ -0,0 +1,43 @@
<?xml version="1.0" encoding="UTF-8"?>
<component type="desktop">
<id>why3.desktop</id>
<metadata_license>0BSD</metadata_license>
<project_license>LGPL-2.1-only WITH OCaml-LGPL-linking-exception</project_license>
<name>Why3</name>
<summary>Software verification platform</summary>
<description>
<p>
Why3 is the next generation of the Why software verification platform. Why3
clearly separates the purely logical specification part from generation of
verification conditions for programs. It features a rich library of proof
task transformations that can be chained to produce a suitable input for a
large set of theorem provers, including SMT solvers, TPTP provers, as well as
interactive proof assistants.
</p>
</description>
<screenshots>
<screenshot type="default">
<image>http://why3.lri.fr/doc/gui-1.png</image>
<caption>Initial Why3 GUI window</caption>
</screenshot>
<screenshot>
<image>http://why3.lri.fr/doc/gui-2.png</image>
<image>The Why3 GUI with goal G1 selected</image>
</screenshot>
<screenshot>
<image>http://why3.lri.fr/doc/gui-3.png</image>
<image>The Why3 GUI after running Alt-Ergo on each goal</image>
</screenshot>
<screenshot>
<image>http://why3.lri.fr/doc/gui-4.png</image>
<image>The Why3 GUI after splitting goal G2</image>
</screenshot>
<screenshot>
<image>http://why3.lri.fr/doc/gui-5.png</image>
<image>File reloaded after modifying goal G2</image>
</screenshot>
</screenshots>
<updatecontact>loganjerry@gmail.com</updatecontact>
<url type="homepage">http://why3.lri.fr/</url>
<url type="bugtracker">https://gitlab.inria.fr/why3/why3/issues</url>
</component>

9
why3.desktop Normal file
View file

@ -0,0 +1,9 @@
[Desktop Entry]
Name=Why3
GenericName=Software Verifier
Comment=Software verification platform
Exec=why3 ide %f
Icon=why3
Type=Application
Terminal=false
Categories=Development;

28
why3.rpmlintrc Normal file
View file

@ -0,0 +1,28 @@
# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON
# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors
# The dictionary lacks some technical words
addFilter(r'W: spelling-error .* provers')
# Caused by ocaml; this package cannot fix it
addFilter(r'why3\.[^:]+: E: missing-call-to-chdir-with-chroot')
# Indeed there is no documentation
addFilter(r'ocaml-why3(|-devel).[^:]+: W: no-documentation')
addFilter(r'why3-(all|emacs|xemacs).[^:]+: W: no-documentation')
# This file is not a text file
addFilter(r'W: file-not-utf8 .*\.mlw')
# The TeX input carries its own character encoding declaration
addFilter(r'why3-examples\.noarch: W: file-not-utf8 .*digit_sum\.tex')
# The .notempty files are markers
addFilter(r'why3-examples\.noarch: W: hidden-file-or-dir .*/\.notempty')
addFilter(r'why3-examples\.noarch: E: zero-length .*/\.notempty')
# We use the version of jquery provided by ocamldoc
addFilter(r'W: unversioned-explicit-provides bundled\(jquery\)')
# The man pages were created by the Fedora packager; there is no URL
addFilter(r'why3\.spec: W: invalid-url Source1: why3-man\.tar\.xz')

62
why3.spec
View file

@ -8,23 +8,28 @@
%endif
Name: why3
Version: 1.2.0
Release: 6%{?dist}
Version: 1.2.1
Release: 1%{?dist}
Summary: Software verification platform
# See LICENSE for the terms of the exception
License: LGPLv2 with exceptions
URL: http://why3.lri.fr/
Source0: https://gforge.inria.fr/frs/download.php/file/37903/%{name}-%{version}.tar.gz
Source0: https://gforge.inria.fr/frs/download.php/file/38185/%{name}-%{version}.tar.gz
# Man pages written by Jerry James using text found in the sources. Hence,
# the copyright and license are the same as for the upstream sources.
Source1: %{name}-man.tar.xz
# Desktop file written by Jerry James
Source2: %{name}.desktop
# AppData file written by Jerry James
Source3: %{name}.appdata.xml
BuildRequires: coq
BuildRequires: emacs-proofgeneral
BuildRequires: evince
BuildRequires: flocq
BuildRequires: gtksourceview2-devel
BuildRequires: hevea
BuildRequires: libappstream-glib
BuildRequires: ocaml
BuildRequires: ocaml-camlp5-devel
BuildRequires: ocaml-findlib
@ -36,6 +41,7 @@ BuildRequires: ocaml-num-devel
BuildRequires: ocaml-sqlite-devel
BuildRequires: ocaml-zarith-devel
BuildRequires: ocaml-zip-devel
BuildRequires: pkgconfig(gtksourceview-2.0)
BuildRequires: rubber
BuildRequires: tex(comment.sty)
BuildRequires: tex(upquote.sty)
@ -43,6 +49,7 @@ BuildRequires: tex-urlbst
BuildRequires: emacs xemacs xemacs-packages-extra
Requires: gtksourceview2
Requires: hicolor-icon-theme
Requires: texlive-base
Requires: vim-filesystem
Provides: bundled(jquery)
@ -111,6 +118,15 @@ Requires: ocaml-zip-devel%{?_isa}
This package contains development files needed to build applications
that use the ocaml-%{name} library.
%package proofgeneral
Summary: Why3 integration with ProofGeneral
Requires: %{name} = %{version}-%{release}
Requires: emacs-proofgeneral
BuildArch: noarch
%description proofgeneral
This package provides a why3 plugin for ProofGeneral.
%prep
%setup -q
%setup -q -T -D -a 1
@ -124,13 +140,14 @@ fixtimestamp() {
# network use
# Link the binaries with runtime compiled with -fPIC.
# This avoids many link-time errors.
sed -e "s|-Wall|$RPM_OPT_FLAGS|" \
sed -e "s|-Wall|$RPM_OPT_FLAGS|;s/ -O -g//" \
-e "s/cp /cp -p /" \
-e "s|^OLINKFLAGS =.*|& -runtime-variant _pic -ccopt \"$RPM_LD_FLAGS\"|" \
-i Makefile.in
# Remove spurious executable bits
find -O3 examples -type f -perm /0111 -exec chmod a-x {} \+
chmod a+x examples/*.sh
# Remove spurious shebangs
sed -i.orig '/#!.*/d' examples/use_api/runstrat/{echo,run}_wait.ml
@ -141,6 +158,10 @@ fixtimestamp examples/use_api/runstrat/run_wait.ml
sed -i.orig 's/\r//' examples/bts/20881.why
fixtimestamp examples/bts/20881.why
# Update the ProofGeneral integration instructions
sed -i.orig 's,(MY_PATH_TO_WHY3)/share/whyitp,%{_emacs_sitelispdir},' share/whyitp/README
fixtimestamp share/whyitp/README
%build
%configure --enable-verbose-make
make #%%{?_smp_mflags}
@ -176,20 +197,35 @@ mkdir -p %{buildroot}%{_datadir}/gtksourceview-2.0
mv %{buildroot}%{_datadir}/%{name}/lang \
%{buildroot}%{_datadir}/gtksourceview-2.0/language-specs
# Install the desktop file
mkdir -p %{buildroot}%{_datadir}/applications
desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE2}
# Install the icon
mkdir -p %{buildroot}%{_datadir}/icons/hicolor/scalable
cp -p share/images/src/logo-kim.svg \
%{buildroot}%{_datadir}/icons/hicolor/scalable/%{name}.svg
# Install the AppStream metadata
mkdir -p %{buildroot}%{_metainfodir}
cp -p %{SOURCE3} %{buildroot}%{_metainfodir}
appstream-util validate-relax --nonet %{buildroot}%{_metainfodir}/%{name}.appdata.xml
# Move the vim file to the right place
mkdir -p %{buildroot}%{_datadir}/vim/vimfiles
mv %{buildroot}%{_datadir}/%{name}/vim/ftdetect \
%{buildroot}%{_datadir}/%{name}/vim/syntax \
%{buildroot}%{_datadir}/vim/vimfiles
# Byte compile the (X)Emacs support file
# Byte compile the (X)Emacs support files
mkdir -p %{buildroot}%{_xemacs_sitelispdir}
cp -p %{buildroot}%{_emacs_sitelispdir}/%{name}.el \
%{buildroot}%{_xemacs_sitelispdir}
cp -p share/whyitp/whyitp.el %{buildroot}%{_emacs_sitelispdir}
pushd %{buildroot}%{_xemacs_sitelispdir}
%{_xemacs_bytecompile} %{name}.el
cd %{buildroot}%{_emacs_sitelispdir}
%{_emacs_bytecompile} %{name}.el
%{_emacs_bytecompile} %{name}.el whyitp.el
popd
# Remove misplaced documentation
@ -206,14 +242,17 @@ chmod 0755 %{buildroot}%{_bindir}/* \
%license LICENSE
%{_bindir}/%{name}
%{_datadir}/%{name}/
%{_datadir}/applications/%{name}.desktop
%{_datadir}/bash-completion/
%{_datadir}/gtksourceview-2.0/language-specs/%{name}.lang
%{_datadir}/icons/hicolor/scalable/%{name}.svg
%{_datadir}/vim/vimfiles/ftdetect/%{name}.vim
%{_datadir}/vim/vimfiles/syntax/%{name}.vim
%{_datadir}/zsh/
%{_texmf}/tex/latex/why3/
%{_libdir}/%{name}/
%{_mandir}/man1/%{name}*
%{_metainfodir}/%{name}.appdata.xml
%files -n ocaml-%{name}
%dir %{_libdir}/ocaml/%{name}/
@ -241,11 +280,20 @@ chmod 0755 %{buildroot}%{_bindir}/* \
%files xemacs
%{_xemacs_sitelispdir}/%{name}.el*
%files proofgeneral
%doc share/whyitp/README
%{_emacs_sitelispdir}/whyitp.el*
# "why3-all" is a meta-package; it just depends on other packages, so that
# it's easier to install a useful suite of tools. Thus, it has no files:
%files all
%changelog
* Tue Oct 29 2019 Jerry James <loganjerry@gmail.com> - 1.2.1-1
- New upstream release
- Add -proofgeneral subpackage
- Add desktop and AppData files
* Fri Oct 11 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-6
- Rebuild for ocaml-menhir 20190924