diff --git a/why3.desktop b/fr.lri.why3.desktop similarity index 100% rename from why3.desktop rename to fr.lri.why3.desktop diff --git a/why3.metainfo.xml b/fr.lri.why3.metainfo.xml similarity index 66% rename from why3.metainfo.xml rename to fr.lri.why3.metainfo.xml index f6c8bda..0c44545 100644 --- a/why3.metainfo.xml +++ b/fr.lri.why3.metainfo.xml @@ -1,6 +1,6 @@ - why3.desktop + fr.lri.why3.desktop 0BSD LGPL-2.1-only WITH OCaml-LGPL-linking-exception Why3 @@ -15,27 +15,27 @@ TPTP provers, as well as interactive proof assistants.

- why3.desktop + fr.lri.why3.desktop - http://why3.lri.fr/doc/gui-1.png + http://why3.lri.fr/doc/_images/gui-1.png Initial Why3 GUI window - http://why3.lri.fr/doc/gui-2.png - The Why3 GUI with goal G1 selected + http://why3.lri.fr/doc/_images/gui-2.png + The Why3 GUI with goal G1 selected - http://why3.lri.fr/doc/gui-3.png - The Why3 GUI after running Alt-Ergo on each goal + http://why3.lri.fr/doc/_images/gui-3.png + The Why3 GUI after running Alt-Ergo on each goal - http://why3.lri.fr/doc/gui-4.png - The Why3 GUI after splitting goal G2 + http://why3.lri.fr/doc/_images/gui-4.png + The Why3 GUI after splitting goal G2 - http://why3.lri.fr/doc/gui-5.png - File reloaded after modifying goal G2 + http://why3.lri.fr/doc/_images/gui-5.png + File reloaded after modifying goal G2 loganjerry@gmail.com diff --git a/sources b/sources index a66b83d..8b12354 100644 --- a/sources +++ b/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 diff --git a/why3-coq8.13.patch b/why3-coq8.13.patch deleted file mode 100644 index 8d63618..0000000 --- a/why3-coq8.13.patch +++ /dev/null @@ -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]+$" diff --git a/why3-sphinxcontrib-bibtex.patch b/why3-sphinxcontrib-bibtex.patch deleted file mode 100644 index 9939fd8..0000000 --- a/why3-sphinxcontrib-bibtex.patch +++ /dev/null @@ -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 diff --git a/why3.spec b/why3.spec index 8a8875c..3928724 100644 --- a/why3.spec +++ b/why3.spec @@ -8,35 +8,30 @@ %endif Name: why3 -Version: 1.3.3 -Release: 6%{?dist} +Version: 1.4.0 +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 -# 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 +Source3: fr.lri.%{name}.metainfo.xml # 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 - 1.4.0-1 +- Version 1.4.0 +- Drop all patches +- Validate with appstreamcli instead of appstream-util + +* Tue Jun 8 2021 Jerry James - 1.3.3-8 +- Rebuild for ocaml-menhir 20210419 + +* Wed Mar 3 2021 Jerry James - 1.3.3-7 +- Rebuild for coq 8.13.1 and ocaml-zarith 1.12 + * Sat Feb 20 2021 Jerry James - 1.3.3-6 - Rebuild for coq 8.13.0 - Update metainfo and install in metainfodir