Version 1.4.0.

- Drop all patches.
- Validate with appstreamcli instead of appstream-util.

fr.lri.why3.metainfo.xml

@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <component type="desktop-application">
-  <id>why3.desktop</id>
+  <id>fr.lri.why3.desktop</id>
   <metadata_license>0BSD</metadata_license>
   <project_license>LGPL-2.1-only WITH OCaml-LGPL-linking-exception</project_license>
   <name>Why3</name>
@@ -15,27 +15,27 @@
       TPTP provers, as well as interactive proof assistants.
     </p>
   </description>
-  <launchable type="desktop-id">why3.desktop</launchable>
+  <launchable type="desktop-id">fr.lri.why3.desktop</launchable>
   <screenshots>
     <screenshot type="default">
-      <image>http://why3.lri.fr/doc/gui-1.png</image>
+      <image>http://why3.lri.fr/doc/_images/gui-1.png</image>
       <caption>Initial Why3 GUI window</caption>
     </screenshot>
     <screenshot>
-      <image>http://why3.lri.fr/doc/gui-2.png</image>
+      <image>http://why3.lri.fr/doc/_images/gui-2.png</image>
-      <image>The Why3 GUI with goal G1 selected</image>
+      <caption>The Why3 GUI with goal G1 selected</caption>
     </screenshot>
     <screenshot>
-      <image>http://why3.lri.fr/doc/gui-3.png</image>
+      <image>http://why3.lri.fr/doc/_images/gui-3.png</image>
-      <image>The Why3 GUI after running Alt-Ergo on each goal</image>
+      <caption>The Why3 GUI after running Alt-Ergo on each goal</caption>
     </screenshot>
     <screenshot>
-      <image>http://why3.lri.fr/doc/gui-4.png</image>
+      <image>http://why3.lri.fr/doc/_images/gui-4.png</image>
-      <image>The Why3 GUI after splitting goal G2</image>
+      <caption>The Why3 GUI after splitting goal G2</caption>
     </screenshot>
     <screenshot>
-      <image>http://why3.lri.fr/doc/gui-5.png</image>
+      <image>http://why3.lri.fr/doc/_images/gui-5.png</image>
-      <image>File reloaded after modifying	 goal G2</image>
+      <caption>File reloaded after modifying goal G2</caption>
     </screenshot>
   </screenshots>
   <update_contact>loganjerry@gmail.com</update_contact>

sources

@@ -1,2 +1,2 @@
 SHA512 (why3-man.tar.xz) = 8355776ac8a67a56ae7354f8fd40dc5d2057022d1035090a3e38e139fbfe3c258fe3ccbed6e333cb005e66c7b4cdbbf6580e3420170fd08384cc9b36ce5ec2a1
-SHA512 (why3-1.3.3.tar.gz) = a2dc95691cea29bbd20843a05add3985f777085086b654b53566ecdb752ba892366da703e232c85d5e0237d0e59564527aed55f6ccae9118d49e5f2cf93a53ce
+SHA512 (why3-1.4.0.tar.gz) = b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a

why3-coq8.13.patch

@@ -1,99 +0,0 @@
---- configure.in.orig	2020-09-11 08:06:19.000000000 -0600
-+++ configure.in	2021-02-06 20:18:51.197299198 -0700
-@@ -869,6 +869,9 @@ if test "$enable_coq_support" = yes; the
-       8.12*)
-          coq_compat_version="COQ812"
-          ;;
-+      8.13*)
-+         coq_compat_version="COQ813"
-+         ;;
-       *)
-          enable_coq_support=no
-          AC_MSG_WARN(You need Coq 8.6 or later; Coq discarded)
---- configure.orig	2020-09-11 08:06:19.000000000 -0600
-+++ configure	2021-02-06 20:19:13.736250432 -0700
-@@ -5365,6 +5365,9 @@ $as_echo "$COQVERSION" >&6; }
-       8.12*)
-          coq_compat_version="COQ812"
-          ;;
-+      8.13*)
-+         coq_compat_version="COQ813"
-+         ;;
-       *)
-          enable_coq_support=no
-          { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: You need Coq 8.6 or later; Coq discarded" >&5
---- lib/coq/ieee_float/GenericFloat.v.orig	2020-09-11 08:06:19.000000000 -0600
-+++ lib/coq/ieee_float/GenericFloat.v	2021-02-06 20:19:40.687192153 -0700
-@@ -3726,7 +3726,8 @@ Proof.
-   assert (- pow2sb <= pow2sb <= pow2sb)%Z.
-   split; auto with zarith.
-   assert (0 < pow2sb)%Z.
--  apply (Z.pow_pos_nonneg 2 sb); auto with zarith.
-+  apply (Z.pow_pos_nonneg 2 sb).
-+  easy.
-   apply Z.lt_le_incl, Hsb'.
-   auto with zarith.
- 
---- lib/coq/set/FsetInt.v.orig	2020-09-11 08:06:19.000000000 -0600
-+++ lib/coq/set/FsetInt.v	2021-02-06 20:21:15.476987120 -0700
-@@ -166,15 +166,13 @@ induction len; eauto.
- intros. simpl. rewrite IHlen. reflexivity.
- Qed.
- 
--(* Why3 goal *)
--Definition interval :
--  Numbers.BinNums.Z -> Numbers.BinNums.Z -> set.Fset.fset Numbers.BinNums.Z.
-+Lemma interval_proof :
-+  forall l r : int, exists s : list int,
-+  List.NoDup s /\
-+  forall e : int, List.In e s <->
-+   (if Z_le_dec l e then if Z_lt_dec e r then true else false else false) = true.
- Proof.
- intros l r.
--exists (fun x => if Z_le_dec l x then 
--                   if Z_lt_dec x r then true 
--                   else false 
--                 else false).
- destruct (Z_le_dec l r).
- + exists (seqZ l (Z.to_nat (r - l))%Z).
-   split. 
-@@ -185,8 +183,8 @@ destruct (Z_le_dec l r).
-     destruct Z_le_dec.
-     * destruct Z_lt_dec. split; intros; [reflexivity|].
-       intuition.
--      intuition. inversion H.
--    * intuition. inversion H.
-+      intuition ; try inversion H.
-+    * intuition ; try inversion H.
- + exists List.nil. 
-   split.
-   - constructor.
-@@ -195,6 +193,18 @@ destruct (Z_le_dec l r).
-     omega.
-     inversion H.
-     inversion H.
-+Qed.
-+
-+(* Why3 goal *)
-+Definition interval :
-+  Numbers.BinNums.Z -> Numbers.BinNums.Z -> set.Fset.fset Numbers.BinNums.Z.
-+Proof.
-+intros l r.
-+exists (fun x =>
-+  if Z_le_dec l x then
-+    if Z_lt_dec x r then true else false
-+  else false).
-+apply interval_proof.
- Defined.
- 
- (* Why3 goal *)
---- share/provers-detection-data.conf.orig	2020-09-11 08:06:19.000000000 -0600
-+++ share/provers-detection-data.conf	2021-02-06 20:21:48.348916001 -0700
-@@ -751,6 +751,7 @@ support_library = "%l/coq/version"
- exec = "coqtop"
- version_switch = "-v"
- version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
-+version_ok = "^8\.13\.[0-9]+$"
- version_ok = "^8\.12\.[0-9]+$"
- version_ok = "^8\.11\.[0-9]+$"
- version_ok = "^8\.10\.[0-9]+$"

why3-sphinxcontrib-bibtex.patch

@@ -1,10 +0,0 @@
---- doc/conf.py.orig	2020-09-11 08:06:19.000000000 -0600
-+++ doc/conf.py	2020-12-23 08:29:46.914254118 -0700
-@@ -50,6 +50,7 @@ master_doc = 'index'
- project = 'Why3'
- copyright = '2020, The Why3 Development Team'
- author = 'The Why3 Development Team'
-+bibtex_bibfiles = ['manual.bib']
- 
- # The version info for the project you're documenting, acts as replacement for
- # |version| and |release|, also used in various other places throughout the

why3.spec

@@ -8,35 +8,30 @@
 %endif
 
 Name:           why3
-Version:        1.3.3
+Version:        1.4.0
-Release:        6%{?dist}
+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/38367/%{name}-%{version}.tar.gz
+Source0:        https://gforge.inria.fr/frs/download.php/file/38425/%{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
+Source2:        fr.lri.%{name}.desktop
 # AppData file written by Jerry James
-Source3:        %{name}.metainfo.xml
+Source3:        fr.lri.%{name}.metainfo.xml
-# Adapt to sphinxcontrib-bibtex 2.x
-Patch0:         %{name}-sphinxcontrib-bibtex.patch
-# Permit use of coq 8.13.0
-# https://gitlab.inria.fr/why3/why3/-/commit/31b5bf527804793c10f26acd2a14045be71d256c
-Patch1:         %{name}-coq8.13.patch
 
 # https://bugzilla.redhat.com/show_bug.cgi?id=1874879
 ExcludeArch: s390x
 
+BuildRequires:  appstream
 BuildRequires:  coq
 BuildRequires:  emacs-proofgeneral
 BuildRequires:  flocq
 BuildRequires:  latexmk
-BuildRequires:  libappstream-glib
 BuildRequires:  make
 BuildRequires:  ocaml
 BuildRequires:  ocaml-camlp5-devel
@@ -244,7 +239,8 @@ cp -p share/images/src/logo-kim.svg \
 # Install the AppStream metadata
 mkdir -p %{buildroot}%{_metainfodir}
 cp -p %{SOURCE3} %{buildroot}%{_metainfodir}
-appstream-util validate-relax --nonet %{buildroot}%{_metainfodir}/%{name}.metainfo.xml
+appstreamcli validate --no-net \
+  %{buildroot}%{_metainfodir}/fr.lri.%{name}.metainfo.xml
 
 # Move the vim file to the right place
 mkdir -p %{buildroot}%{_datadir}/vim/vimfiles
@@ -277,7 +273,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %license LICENSE
 %{_bindir}/%{name}
 %{_datadir}/%{name}/
-%{_datadir}/applications/%{name}.desktop
+%{_datadir}/applications/fr.lri.%{name}.desktop
 %{_datadir}/bash-completion/completions/why3
 %{_datadir}/gtksourceview-3.0/language-specs/%{name}.lang
 %{_datadir}/gtksourceview-3.0/language-specs/%{name}c.lang
@@ -289,7 +285,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %{_texmf}/tex/latex/why3/
 %{_libdir}/%{name}/
 %{_mandir}/man1/%{name}*
-%{_metainfodir}/%{name}.metainfo.xml
+%{_metainfodir}/fr.lri.%{name}.metainfo.xml
 
 %files -n ocaml-%{name}
 %dir %{_libdir}/ocaml/%{name}/
@@ -307,6 +303,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %else
 %{_libdir}/ocaml/%{name}/*.cma
 %endif
+%{_libdir}/ocaml/%{name}/*.cmt
 
 %files examples
 %doc examples
@@ -326,6 +323,17 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %files all
 
 %changelog
+* Wed Jul 14 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-1
+- Version 1.4.0
+- Drop all patches
+- Validate with appstreamcli instead of appstream-util
+
+* Tue Jun  8 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-8
+- Rebuild for ocaml-menhir 20210419
+
+* Wed Mar  3 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-7
+- Rebuild for coq 8.13.1 and ocaml-zarith 1.12
+
 * Sat Feb 20 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-6
 - Rebuild for coq 8.13.0
 - Update metainfo and install in metainfodir