From c96ac3b16a9ccc22c8e75027a7c63611e8d1f0b9 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 4 Oct 2023 23:18:14 -0600 Subject: [PATCH 01/47] Remove old obsoletes --- why3.spec | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/why3.spec b/why3.spec index d9c2622..1472867 100644 --- a/why3.spec +++ b/why3.spec @@ -84,14 +84,6 @@ Provides: bundled(js-jquery) # The corresponding Provides is not generated, so filter this out %global __requires_exclude ocaml\\\((Driver_ast|Why3)\\\) -# This can be removed when F36 reaches EOL -Obsoletes: why < 2.41-12 -Provides: why = 2.41-12%{?dist} -Obsoletes: why-jessie < 2.41-12 -Provides: why-jessie = 2.41-12%{?dist} -Obsoletes: why-pvs-support < 2.41-12 -Provides: why-pvs-support = 2.41-12%{?dist} - # This can be removed when F39 reaches EOL Obsoletes: %{name}-xemacs < 1.4.0-4 @@ -125,10 +117,6 @@ Summary: Complete Why3 software verification platform suite Requires: %{name}%{?_isa} = %{version}-%{release} Requires: alt-ergo coq cvc5 E gappa yices-tools z3 zenon -# This can be removed when F36 reaches EOL -Obsoletes: why-all < 2.41-12 -Provides: why-all = 2.41-12%{?dist} - %description all This package provides a complete software verification platform suite based on Why3, including various automated and interactive provers. From b3fca63993ac0cbbcf9988bc44f7d01716b44c96 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Thu, 5 Oct 2023 21:46:07 +0100 Subject: [PATCH 02/47] OCaml 5.1 rebuild for Fedora 40 --- why3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why3.spec b/why3.spec index 1472867..89e634b 100644 --- a/why3.spec +++ b/why3.spec @@ -18,7 +18,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.6.0 -Release: 6%{?dist} +Release: 7%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -296,6 +296,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Thu Oct 05 2023 Richard W.M. Jones - 1.6.0-7 +- OCaml 5.1 rebuild for Fedora 40 + * Sat Sep 9 2023 Jerry James - 1.6.0-6 - Rebuild for ocaml-ocamlgraph 2.1.0 From 8b5401104dfcddbdba42b4459edadf8042ecfdca Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 12 Dec 2023 19:17:54 +0000 Subject: [PATCH 03/47] OCaml 5.1.1 rebuild for Fedora 40 --- why3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why3.spec b/why3.spec index 89e634b..04cab31 100644 --- a/why3.spec +++ b/why3.spec @@ -18,7 +18,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.6.0 -Release: 7%{?dist} +Release: 8%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -296,6 +296,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Tue Dec 12 2023 Richard W.M. Jones - 1.6.0-8 +- OCaml 5.1.1 rebuild for Fedora 40 + * Thu Oct 05 2023 Richard W.M. Jones - 1.6.0-7 - OCaml 5.1 rebuild for Fedora 40 From 8d82ad63f7db0e720f47f0c2c5d17d92b7a9eee5 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 18 Dec 2023 19:26:12 +0000 Subject: [PATCH 04/47] OCaml 5.1.1 + s390x code gen fix for Fedora 40 --- why3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why3.spec b/why3.spec index 04cab31..2c34db9 100644 --- a/why3.spec +++ b/why3.spec @@ -18,7 +18,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.6.0 -Release: 8%{?dist} +Release: 9%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -296,6 +296,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Mon Dec 18 2023 Richard W.M. Jones - 1.6.0-9 +- OCaml 5.1.1 + s390x code gen fix for Fedora 40 + * Tue Dec 12 2023 Richard W.M. Jones - 1.6.0-8 - OCaml 5.1.1 rebuild for Fedora 40 From e86bfd31127088031a55fdb7508ed8de3e54877a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 2 Jan 2024 12:34:03 -0700 Subject: [PATCH 05/47] Version 1.7.0. Drop upstreamed coq patch. --- sources | 2 +- why3-coq-8.17.patch | 82 --------------------------------------------- why3.spec | 14 ++++---- 3 files changed, 8 insertions(+), 90 deletions(-) delete mode 100644 why3-coq-8.17.patch diff --git a/sources b/sources index 026cfc6..2c57c42 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (why3-1.6.0.tar.gz) = 60d61b8337ab9f2fd2e6c7174eb0bab063f122417738cd75990c5c53120dd535bcedccb670567f5753853d6bc9f8efebb563d079e4d368372a7687193f1346b1 +SHA512 (why3-1.7.0.tar.gz) = 1fb458e58b75662e3cc4f3cdb42b0e2229d5c73e44a182370ce8beca3a2e18ac8b6c9a403ba94f9391d46cb9bd47cd37cfc9592c77cc2164a7f92124f6f557b6 diff --git a/why3-coq-8.17.patch b/why3-coq-8.17.patch deleted file mode 100644 index 2503ce7..0000000 --- a/why3-coq-8.17.patch +++ /dev/null @@ -1,82 +0,0 @@ ---- why3-1.6.0/configure.in.orig 2023-03-07 02:15:31.000000000 -0700 -+++ why3-1.6.0/configure.in 2023-06-26 14:21:56.361457115 -0600 -@@ -993,6 +993,10 @@ if test "$enable_coq_support" = yes; the - 8.16*) - coq_compat_version="COQ816" - ;; -+ 8.17*) -+ coq_compat_version="COQ817" -+ COQFLAGS="-w deprecated-instance-without-locality,deprecated-hint-without-locality" -+ ;; - *) - enable_coq_support=no - AC_MSG_WARN([You need Coq 8.7 or later; Coq discarded.]) -@@ -1242,6 +1246,7 @@ AC_SUBST(COQC) - AC_SUBST(COQDEP) - AC_SUBST(COQLIB) - AC_SUBST(COQVERSION) -+AC_SUBST(COQFLAGS) - - AC_SUBST(enable_pvs_libs) - AC_SUBST(PVS) ---- why3-1.6.0/configure.orig 2023-03-07 02:15:31.000000000 -0700 -+++ why3-1.6.0/configure 2023-06-26 14:35:07.856280739 -0600 -@@ -696,6 +696,7 @@ PVSVERSION - enable_pvs_libs - COQVERSION - COQLIB -+COQFLAGS - coq_compat_version - enable_coq_fp_libs - enable_coq_libs -@@ -5926,6 +5927,10 @@ printf "%s\n" "$COQVERSION" >&6; } - 8.16*) - coq_compat_version="COQ816" - ;; -+ 8.17*) -+ coq_compat_version="COQ817" -+ COQFLAGS="-w deprecated-instance-without-locality,deprecated-hint-without-locality" -+ ;; - *) - enable_coq_support=no - { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: You need Coq 8.7 or later; Coq discarded." >&5 ---- why3-1.6.0/Makefile.in.orig 2023-03-07 02:15:31.000000000 -0700 -+++ why3-1.6.0/Makefile.in 2023-06-26 14:21:12.426061732 -0600 -@@ -62,6 +62,7 @@ OCAMLBEST = @OCAMLBEST@ - OCAMLVERSION = @OCAMLVERSION@ - COQC = @COQC@ - COQDEP = @COQDEP@ -+COQFLAGS = @COQFLAGS@ - FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@ - MENHIR = @MENHIR@ - -@@ -1068,7 +1069,7 @@ COQLIBS_FILES = lib/coq/BuiltIn lib/coq/ - - %.vo: %.v - $(SHOW) 'Coqc $<' -- $(HIDE)$(COQC) -R lib/coq Why3 $< -+ $(HIDE)$(COQC) $(COQFLAGS) -R lib/coq Why3 $< - - %.vd: %.v - $(SHOW) 'Coqdep $<' ---- why3-1.6.0/share/provers-detection-data.conf.orig 2023-03-07 02:15:31.000000000 -0700 -+++ why3-1.6.0/share/provers-detection-data.conf 2023-06-26 14:22:52.768680868 -0600 -@@ -838,16 +838,8 @@ support_library = "%l/coq/version" - exec = "coqtop" - version_switch = "-v" - version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)" --version_ok = "^8\.16\.[0-9]+$" --version_ok = "^8\.15\.[0-9]+$" --version_ok = "^8\.14\.[0-9]+$" --version_ok = "^8\.13\.[0-9]+$" --version_ok = "^8\.12\.[0-9]+$" --version_ok = "^8\.11\.[0-9]+$" --version_ok = "^8\.10\.[0-9]+$" --version_ok = "^8\.9\.[0-9]+$" --version_ok = "^8\.8\.[0-9]+$" --version_ok = "^8\.7\.[0-9]+$" -+version_ok = "^8\.1[0-7]\.[0-9]+$" -+version_ok = "^8\.[7-9]\.[0-9]+$" - version_old = "8.6.1" - version_old = "8.6" - version_old = "^8\.5pl[1-3]$" diff --git a/why3.spec b/why3.spec index 2c34db9..2729d7b 100644 --- a/why3.spec +++ b/why3.spec @@ -17,8 +17,8 @@ ExclusiveArch: %{ocaml_native_compiler} %endif Name: why3 -Version: 1.6.0 -Release: 9%{?dist} +Version: 1.7.0 +Release: 1%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -29,10 +29,6 @@ Source1: fr.lri.%{name}.desktop # AppData file written by Jerry James Source2: fr.lri.%{name}.metainfo.xml -# Support coq 8.17. See -# https://gitlab.inria.fr/why3/why3/-/commit/64facc03bdc2bc4ce0586ff2f458bcd87f646ba8 -Patch0: %{name}-coq-8.17.patch - BuildRequires: coq BuildRequires: emacs-nox BuildRequires: emacs-proofgeneral @@ -258,7 +254,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %{_datadir}/icons/hicolor/scalable/%{name}.svg %{_datadir}/vim/vimfiles/ftdetect/%{name}.vim %{_datadir}/vim/vimfiles/syntax/%{name}.vim -%{_datadir}/zsh/ +%{_datadir}/zsh/site-functions/_why3 %{_texmf}/tex/latex/why3/ %{_libdir}/%{name}/ %{_metainfodir}/fr.lri.%{name}.metainfo.xml @@ -296,6 +292,10 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Tue Jan 2 2024 Jerry James - 1.7.0-1 +- Version 1.7.0 +- Drop upstreamed coq patch + * Mon Dec 18 2023 Richard W.M. Jones - 1.6.0-9 - OCaml 5.1.1 + s390x code gen fix for Fedora 40 From 12c78c7f05b31de36332863414128ebafd6dd47f Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 27 Jan 2024 08:45:59 +0000 Subject: [PATCH 06/47] Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild --- why3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why3.spec b/why3.spec index 2729d7b..efeb26f 100644 --- a/why3.spec +++ b/why3.spec @@ -18,7 +18,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.7.0 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -292,6 +292,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Sat Jan 27 2024 Fedora Release Engineering - 1.7.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild + * Tue Jan 2 2024 Jerry James - 1.7.0-1 - Version 1.7.0 - Drop upstreamed coq patch From 8d5ff06bc5e290fc7ff4499417dd832aa80749e0 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 2 Feb 2024 16:41:48 -0700 Subject: [PATCH 07/47] Version 1.7.1 --- sources | 2 +- why3.spec | 13 +++++-------- 2 files changed, 6 insertions(+), 9 deletions(-) diff --git a/sources b/sources index 2c57c42..8b5ff60 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (why3-1.7.0.tar.gz) = 1fb458e58b75662e3cc4f3cdb42b0e2229d5c73e44a182370ce8beca3a2e18ac8b6c9a403ba94f9391d46cb9bd47cd37cfc9592c77cc2164a7f92124f6f557b6 +SHA512 (why3-1.7.1.tar.gz) = 3b1636e9459aced943a6b895aa7a6db3552adcf9878c2fa2b67913d6b555b67b00f6f1c9b28ffa80cbdf3fa01007aa7f8c9c4fa6c8c56dee579955cf5d57980b diff --git a/why3.spec b/why3.spec index efeb26f..00a128d 100644 --- a/why3.spec +++ b/why3.spec @@ -1,12 +1,6 @@ # Coq's plugin architecture requires cmxs files, so: ExclusiveArch: %{ocaml_native_compiler} -# ANTLR is unavailable on i686, so coq is also unavailable. We could build -# without coq support, but choose to forgo i686 support entirely. -# See https://fedoraproject.org/wiki/Changes/Drop_i686_JDKs -# See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval -#ExclusiveArch: %%{java_arches} - # NOTE: Upstream has said that the Frama-C support is still experimental, and # less functional than the corresponding support in why2. They recommend not # enabling it for now. We abide by their wishes. Revisit this decision each @@ -17,8 +11,8 @@ ExclusiveArch: %{ocaml_native_compiler} %endif Name: why3 -Version: 1.7.0 -Release: 2%{?dist} +Version: 1.7.1 +Release: 1%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -292,6 +286,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Fri Feb 2 2024 Jerry James - 1.7.1-1 +- Version 1.7.1 + * Sat Jan 27 2024 Fedora Release Engineering - 1.7.0-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild From 84cb61b8ea83632f544fbefc84545ec0c79557d1 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 2 Feb 2024 18:44:17 -0700 Subject: [PATCH 08/47] Build again because koji ran out of disk space --- why3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why3.spec b/why3.spec index 00a128d..af6117c 100644 --- a/why3.spec +++ b/why3.spec @@ -12,7 +12,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.7.1 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -286,6 +286,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Fri Feb 2 2024 Jerry James - 1.7.1-2 +- Build again because koji ran out of disk space + * Fri Feb 2 2024 Jerry James - 1.7.1-1 - Version 1.7.1 From 44636b45553fd57d03d62ea25cc84cca28214877 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 25 Mar 2024 11:19:18 +0000 Subject: [PATCH 09/47] Use %{bash_completions_dir} macro --- why3.spec | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/why3.spec b/why3.spec index af6117c..ef5a413 100644 --- a/why3.spec +++ b/why3.spec @@ -12,7 +12,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.7.1 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -182,8 +182,8 @@ cd - %endif # Install the bash completion file -mkdir -p %{buildroot}%{_datadir}/bash-completion/completions -cp -p share/bash/%{name} %{buildroot}%{_datadir}/bash-completion/completions +mkdir -p %{buildroot}%{bash_completions_dir} +cp -p share/bash/%{name} %{buildroot}%{bash_completions_dir} # Install the zsh completion file mkdir -p %{buildroot}%{_datadir}/zsh/site-functions @@ -241,7 +241,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %{_bindir}/isabelle_client %{_datadir}/%{name}/ %{_datadir}/applications/fr.lri.%{name}.desktop -%{_datadir}/bash-completion/completions/why3 +%{bash_completions_dir}/why3 %{_datadir}/gtksourceview-3.0/language-specs/%{name}.lang %{_datadir}/gtksourceview-3.0/language-specs/%{name}c.lang %{_datadir}/gtksourceview-3.0/language-specs/%{name}py.lang @@ -286,6 +286,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Mon Mar 25 2024 Richard W.M. Jones - 1.7.1-3 +- Use %%{bash_completions_dir} macro + * Fri Feb 2 2024 Jerry James - 1.7.1-2 - Build again because koji ran out of disk space From 8000f2ad4af141f76026c5822c8ec889dba63864 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 18 Apr 2024 09:47:00 -0600 Subject: [PATCH 10/47] Version 1.7.2 --- sources | 2 +- why3.spec | 22 +++++++++++----------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/sources b/sources index 8b5ff60..a941d8e 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (why3-1.7.1.tar.gz) = 3b1636e9459aced943a6b895aa7a6db3552adcf9878c2fa2b67913d6b555b67b00f6f1c9b28ffa80cbdf3fa01007aa7f8c9c4fa6c8c56dee579955cf5d57980b +SHA512 (why3-1.7.2.tar.gz) = 7e80671480ce0dc3c69514bea2836f5899c686b43a4e8607c27d28e63f78150150dc45fcac5760dbee9721d363e456b1dcaeb1501fc9f63f360722a1021f675f diff --git a/why3.spec b/why3.spec index ef5a413..33b01f7 100644 --- a/why3.spec +++ b/why3.spec @@ -6,17 +6,14 @@ ExclusiveArch: %{ocaml_native_compiler} # enabling it for now. We abide by their wishes. Revisit this decision each # release. -%ifnarch %{ocaml_native_compiler} -%global debug_package %{nil} -%endif - Name: why3 -Version: 1.7.1 -Release: 3%{?dist} +Version: 1.7.2 +Release: 1%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception URL: https://why3.lri.fr/ +VCS: https://gitlab.inria.fr/why3/why3 Source0: https://why3.gitlabpages.inria.fr/releases/%{name}-%{version}.tar.gz # Desktop file written by Jerry James Source1: fr.lri.%{name}.desktop @@ -24,7 +21,7 @@ Source1: fr.lri.%{name}.desktop Source2: fr.lri.%{name}.metainfo.xml BuildRequires: coq -BuildRequires: emacs-nox +BuildRequires: emacs-nw BuildRequires: emacs-proofgeneral BuildRequires: flocq BuildRequires: graphviz @@ -186,8 +183,8 @@ mkdir -p %{buildroot}%{bash_completions_dir} cp -p share/bash/%{name} %{buildroot}%{bash_completions_dir} # Install the zsh completion file -mkdir -p %{buildroot}%{_datadir}/zsh/site-functions -cp -p share/zsh/_why3 %{buildroot}%{_datadir}/zsh/site-functions +mkdir -p %{buildroot}%{zsh_completions_dir} +cp -p share/zsh/_why3 %{buildroot}%{zsh_completions_dir} # Install the LaTeX style mkdir -p %{buildroot}%{_texmf}/tex/latex/why3 @@ -239,16 +236,16 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %license LICENSE %{_bindir}/%{name} %{_bindir}/isabelle_client +%{bash_completions_dir}/why3 +%{zsh_completions_dir}/_why3 %{_datadir}/%{name}/ %{_datadir}/applications/fr.lri.%{name}.desktop -%{bash_completions_dir}/why3 %{_datadir}/gtksourceview-3.0/language-specs/%{name}.lang %{_datadir}/gtksourceview-3.0/language-specs/%{name}c.lang %{_datadir}/gtksourceview-3.0/language-specs/%{name}py.lang %{_datadir}/icons/hicolor/scalable/%{name}.svg %{_datadir}/vim/vimfiles/ftdetect/%{name}.vim %{_datadir}/vim/vimfiles/syntax/%{name}.vim -%{_datadir}/zsh/site-functions/_why3 %{_texmf}/tex/latex/why3/ %{_libdir}/%{name}/ %{_metainfodir}/fr.lri.%{name}.metainfo.xml @@ -286,6 +283,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Thu Apr 18 2024 Jerry James - 1.7.2-1 +- Version 1.7.2 + * Mon Mar 25 2024 Richard W.M. Jones - 1.7.1-3 - Use %%{bash_completions_dir} macro From 0aeedb81c597ea0247a15450b25c5d092a6db472 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Thu, 30 May 2024 10:30:35 +0100 Subject: [PATCH 11/47] OCaml 5.2.0 for Fedora 41 --- why3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why3.spec b/why3.spec index 33b01f7..b045f08 100644 --- a/why3.spec +++ b/why3.spec @@ -8,7 +8,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.7.2 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -283,6 +283,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Thu May 30 2024 Richard W.M. Jones - 1.7.2-2 +- OCaml 5.2.0 for Fedora 41 + * Thu Apr 18 2024 Jerry James - 1.7.2-1 - Version 1.7.2 From 356eda9812df2a090b2453d7483e90a1eaa10537 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 13 Jun 2024 14:38:24 -0600 Subject: [PATCH 12/47] Rebuild for apron 0.9.15 - New upstream URL --- why3.spec | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/why3.spec b/why3.spec index b045f08..81e3754 100644 --- a/why3.spec +++ b/why3.spec @@ -8,11 +8,11 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.7.2 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception -URL: https://why3.lri.fr/ +URL: https://www.why3.org/ VCS: https://gitlab.inria.fr/why3/why3 Source0: https://why3.gitlabpages.inria.fr/releases/%{name}-%{version}.tar.gz # Desktop file written by Jerry James @@ -283,6 +283,10 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Thu Jun 13 2024 Jerry James - 1.7.2-3 +- Rebuild for apron 0.9.15 +- New upstream URL + * Thu May 30 2024 Richard W.M. Jones - 1.7.2-2 - OCaml 5.2.0 for Fedora 41 From c6f768199271c3973f867e7ccab35f40f9ce90d5 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 19 Jun 2024 19:28:35 +0100 Subject: [PATCH 13/47] OCaml 5.2.0 ppc64le fix OCaml 5.2.0 ppc64le fix OCaml 5.2.0 ppc64le fix OCaml 5.2.0 ppc64le fix OCaml 5.2.0 ppc64le fix OCaml 5.2.0 ppc64le fix OCaml 5.2.0 ppc64le fix --- why3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why3.spec b/why3.spec index 81e3754..10fb90f 100644 --- a/why3.spec +++ b/why3.spec @@ -8,7 +8,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.7.2 -Release: 3%{?dist} +Release: 4%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -283,6 +283,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Wed Jun 19 2024 Richard W.M. Jones - 1.7.2-4 +- OCaml 5.2.0 ppc64le fix + * Thu Jun 13 2024 Jerry James - 1.7.2-3 - Rebuild for apron 0.9.15 - New upstream URL From b4ad7f2eed50d6ee7f5e4d90e82f2f9b5854b921 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 3 Jul 2024 16:58:56 -0600 Subject: [PATCH 14/47] Rebuild for ocaml-ppx-sexp-conv 0.17.0 --- why3.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/why3.spec b/why3.spec index 10fb90f..0c7d2ac 100644 --- a/why3.spec +++ b/why3.spec @@ -8,12 +8,12 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.7.2 -Release: 4%{?dist} +Release: 5%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception URL: https://www.why3.org/ -VCS: https://gitlab.inria.fr/why3/why3 +VCS: git:https://gitlab.inria.fr/why3/why3.git Source0: https://why3.gitlabpages.inria.fr/releases/%{name}-%{version}.tar.gz # Desktop file written by Jerry James Source1: fr.lri.%{name}.desktop @@ -283,6 +283,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Wed Jul 3 2024 Jerry James - 1.7.2-5 +- Rebuild for ocaml-ppx-sexp-conv 0.17.0 + * Wed Jun 19 2024 Richard W.M. Jones - 1.7.2-4 - OCaml 5.2.0 ppc64le fix From 664bbc3564880339a44c8299eb1f7fb4a0766b42 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 16 Jul 2024 11:13:09 -0600 Subject: [PATCH 15/47] Rebuild for ocaml-zarith 1.14 --- why3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why3.spec b/why3.spec index 0c7d2ac..180f048 100644 --- a/why3.spec +++ b/why3.spec @@ -8,7 +8,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.7.2 -Release: 5%{?dist} +Release: 6%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -283,6 +283,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Tue Jul 16 2024 Jerry James - 1.7.2-6 +- Rebuild for ocaml-zarith 1.14 + * Wed Jul 3 2024 Jerry James - 1.7.2-5 - Rebuild for ocaml-ppx-sexp-conv 0.17.0 From 2daac66f5789e4b479b3317757786f84197486d5 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 20 Jul 2024 09:20:04 +0000 Subject: [PATCH 16/47] Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild --- why3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why3.spec b/why3.spec index 180f048..b01a89b 100644 --- a/why3.spec +++ b/why3.spec @@ -8,7 +8,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.7.2 -Release: 6%{?dist} +Release: 7%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -283,6 +283,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Sat Jul 20 2024 Fedora Release Engineering - 1.7.2-7 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild + * Tue Jul 16 2024 Jerry James - 1.7.2-6 - Rebuild for ocaml-zarith 1.14 From acda593bf2d76e32878cd05b0c91c7b15d265de9 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 5 Aug 2024 11:24:06 -0600 Subject: [PATCH 17/47] Rebuild for ocaml-menhir 20240715, ocaml-ppxlib 0.33.0, and ocaml-zip 1.1.2 --- why3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why3.spec b/why3.spec index b01a89b..1dcd287 100644 --- a/why3.spec +++ b/why3.spec @@ -8,7 +8,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.7.2 -Release: 7%{?dist} +Release: 8%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -283,6 +283,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Mon Aug 5 2024 Jerry James - 1.7.2-8 +- Rebuild for ocaml-menhir 20240715, ocaml-ppxlib 0.33.0, and ocaml-zip 1.1.2 + * Sat Jul 20 2024 Fedora Release Engineering - 1.7.2-7 - Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild From b798c9103b1b445b23a81a3693e0d0d540465666 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 6 Oct 2024 15:16:41 -0600 Subject: [PATCH 18/47] Rebuild for ocaml-re 1.13.3 --- why3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why3.spec b/why3.spec index 1dcd287..01f9e0b 100644 --- a/why3.spec +++ b/why3.spec @@ -8,7 +8,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.7.2 -Release: 8%{?dist} +Release: 9%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -283,6 +283,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Sun Oct 6 2024 Jerry James - 1.7.2-9 +- Rebuild for ocaml-re 1.13.3 + * Mon Aug 5 2024 Jerry James - 1.7.2-8 - Rebuild for ocaml-menhir 20240715, ocaml-ppxlib 0.33.0, and ocaml-zip 1.1.2 From 88b9f2e9c7492aad9a7ddc5fe33796ea023f4204 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 14 Oct 2024 15:14:21 -0600 Subject: [PATCH 19/47] Fix the location of the icon --- why3.spec | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/why3.spec b/why3.spec index 01f9e0b..9a05440 100644 --- a/why3.spec +++ b/why3.spec @@ -8,7 +8,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.7.2 -Release: 9%{?dist} +Release: 10%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -200,9 +200,9 @@ mkdir -p %{buildroot}%{_datadir}/applications desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE1} # Install the icon -mkdir -p %{buildroot}%{_datadir}/icons/hicolor/scalable +mkdir -p %{buildroot}%{_datadir}/icons/hicolor/scalable/apps cp -p share/images/src/logo-kim.svg \ - %{buildroot}%{_datadir}/icons/hicolor/scalable/%{name}.svg + %{buildroot}%{_datadir}/icons/hicolor/scalable/apps/%{name}.svg # Install the AppStream metadata mkdir -p %{buildroot}%{_metainfodir} @@ -243,7 +243,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %{_datadir}/gtksourceview-3.0/language-specs/%{name}.lang %{_datadir}/gtksourceview-3.0/language-specs/%{name}c.lang %{_datadir}/gtksourceview-3.0/language-specs/%{name}py.lang -%{_datadir}/icons/hicolor/scalable/%{name}.svg +%{_datadir}/icons/hicolor/scalable/apps/%{name}.svg %{_datadir}/vim/vimfiles/ftdetect/%{name}.vim %{_datadir}/vim/vimfiles/syntax/%{name}.vim %{_texmf}/tex/latex/why3/ @@ -283,6 +283,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Mon Oct 14 2024 Jerry James - 1.7.2-10 +- Fix the location of the icon + * Sun Oct 6 2024 Jerry James - 1.7.2-9 - Rebuild for ocaml-re 1.13.3 From 98156958f8b58a70bc592b23e2f63161f5469056 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 10 Jan 2025 10:28:18 -0700 Subject: [PATCH 20/47] Convert to %autorelease and %autochangelog [skip changelog] --- changelog | 534 +++++++++++++++++++++++++++++++++++++++++++++++++++++ why3.spec | 537 +----------------------------------------------------- 2 files changed, 536 insertions(+), 535 deletions(-) create mode 100644 changelog diff --git a/changelog b/changelog new file mode 100644 index 0000000..0856a59 --- /dev/null +++ b/changelog @@ -0,0 +1,534 @@ +* Mon Oct 14 2024 Jerry James - 1.7.2-10 +- Fix the location of the icon + +* Sun Oct 6 2024 Jerry James - 1.7.2-9 +- Rebuild for ocaml-re 1.13.3 + +* Mon Aug 5 2024 Jerry James - 1.7.2-8 +- Rebuild for ocaml-menhir 20240715, ocaml-ppxlib 0.33.0, and ocaml-zip 1.1.2 + +* Sat Jul 20 2024 Fedora Release Engineering - 1.7.2-7 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild + +* Tue Jul 16 2024 Jerry James - 1.7.2-6 +- Rebuild for ocaml-zarith 1.14 + +* Wed Jul 3 2024 Jerry James - 1.7.2-5 +- Rebuild for ocaml-ppx-sexp-conv 0.17.0 + +* Wed Jun 19 2024 Richard W.M. Jones - 1.7.2-4 +- OCaml 5.2.0 ppc64le fix + +* Thu Jun 13 2024 Jerry James - 1.7.2-3 +- Rebuild for apron 0.9.15 +- New upstream URL + +* Thu May 30 2024 Richard W.M. Jones - 1.7.2-2 +- OCaml 5.2.0 for Fedora 41 + +* Thu Apr 18 2024 Jerry James - 1.7.2-1 +- Version 1.7.2 + +* Mon Mar 25 2024 Richard W.M. Jones - 1.7.1-3 +- Use %%{bash_completions_dir} macro + +* Fri Feb 2 2024 Jerry James - 1.7.1-2 +- Build again because koji ran out of disk space + +* Fri Feb 2 2024 Jerry James - 1.7.1-1 +- Version 1.7.1 + +* Sat Jan 27 2024 Fedora Release Engineering - 1.7.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild + +* Tue Jan 2 2024 Jerry James - 1.7.0-1 +- Version 1.7.0 +- Drop upstreamed coq patch + +* Mon Dec 18 2023 Richard W.M. Jones - 1.6.0-9 +- OCaml 5.1.1 + s390x code gen fix for Fedora 40 + +* Tue Dec 12 2023 Richard W.M. Jones - 1.6.0-8 +- OCaml 5.1.1 rebuild for Fedora 40 + +* Thu Oct 05 2023 Richard W.M. Jones - 1.6.0-7 +- OCaml 5.1 rebuild for Fedora 40 + +* Sat Sep 9 2023 Jerry James - 1.6.0-6 +- Rebuild for ocaml-ocamlgraph 2.1.0 + +* Sat Jul 29 2023 Jerry James - 1.6.0-5 +- Require cvc5 instead of cvc4 + +* Thu Jul 27 2023 Jerry James - 1.6.0-4 +- Rebuild for ocaml-zarith 1.13 + +* Sat Jul 22 2023 Fedora Release Engineering - 1.6.0-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild + +* Tue Jul 18 2023 Jerry James - 1.6.0-2 +- Validate metadata with appstream-util + +* Thu Jul 13 2023 Jerry James - 1.6.0-2 +- Rebuild for mpfr 4.2.0 + +* Mon Jul 10 2023 Jerry James - 1.6.0-1 +- Version 1.6.0 +- Enable inference with BDDs +- Add patch for coq 8.17 support + +* Sat Apr 1 2023 Jerry James - 1.5.1-7 +- Rebuild for coq 8.17.0 + +* Tue Jan 24 2023 Richard W.M. Jones - 1.5.1-6 +- Rebuild OCaml packages for F38 + +* Sat Jan 21 2023 Fedora Release Engineering - 1.5.1-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild + +* Fri Jan 6 2023 Jerry James - 1.5.1-4 +- BR tex(tgtermes.sty) to fix FTBFS with TeXLive 2022 + +* Sat Nov 26 2022 Jerry James - 1.5.1-3 +- Rebuild for coq 8.16.1 + +* Tue Nov 1 2022 Jerry James - 1.5.1-2 +- Rebuild for ocaml-ppxlib 0.28.0 + +* Fri Sep 16 2022 Jerry James - 1.5.1-1 +- Version 1.5.1 + +* Thu Aug 18 2022 Jerry James - 1.5.0-3 +- Rebuild to fix coq dependency +- Convert License tag to SPDX + +* Sat Jul 23 2022 Fedora Release Engineering - 1.5.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild + +* Tue Jul 19 2022 Jerry James - 1.5.0-1 +- Remove i686 support + +* Thu Jul 7 2022 Jerry James - 1.5.0-1 +- Version 1.5.0 +- Add ocaml-mlmpfr support +- Drop unmaintained man pages +- Use new OCaml macros + +* Sun Jun 19 2022 Richard W.M. Jones - 1.4.1-3 +- OCaml 4.14.0 rebuild + +* Fri Mar 25 2022 Jerry James - 1.4.1-2 +- Rebuild for coq 8.15.1 + +* Mon Feb 28 2022 Jerry James - 1.4.1-1 +- Version 1.4.1 + +* Fri Feb 04 2022 Richard W.M. Jones - 1.4.0-11 +- OCaml 4.13.1 rebuild to remove package notes + +* Sat Jan 22 2022 Fedora Release Engineering - 1.4.0-10 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild + +* Mon Jan 17 2022 Jerry James - 1.4.0-9 +- Rebuild for menhir 20211230 + +* Mon Dec 27 2021 Jerry James - 1.4.0-8 +- Rebuild for alt-ergo 2.3.0 and ocaml-zip 1.11 + +* Tue Nov 30 2021 Jerry James - 1.4.0-7 +- Rebuild for coq 8.14.1, sexplib0 0.15.0 and menhir 20211128 + +* Thu Oct 21 2021 Jerry James - 1.4.0-6 +- Rebuild for coq 8.14.0 and menhir 20211012 +- Add -coq8.14 patch +- Drop XEmacs support + +* Tue Oct 05 2021 Richard W.M. Jones - 1.4.0-5 +- OCaml 4.13.1 build + +* Mon Oct 04 2021 Richard W.M. Jones - 1.4.0-4 +- Try to build on s390x with OCaml 4.13 + +* Fri Jul 30 2021 Jerry James - 1.4.0-3 +- Rebuild for rebuilt coq + +* Fri Jul 23 2021 Fedora Release Engineering - 1.4.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild + +* 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-9 +- Rebuild for ocaml-menhir 20210419 + +* Wed Mar 3 2021 Jerry James - 1.3.3-8 +- Rebuild for coq 8.13.1 and ocaml-zarith 1.12 + +* Tue Mar 2 11:18:12 GMT 2021 Richard W.M. Jones - 1.3.3-7 +- OCaml 4.12.0 build + +* Sat Feb 20 2021 Jerry James - 1.3.3-6 +- Rebuild for coq 8.13.0 +- Update metainfo and install in metainfodir + +* Wed Jan 27 2021 Fedora Release Engineering - 1.3.3-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild + +* Sat Jan 2 2021 Jerry James - 1.3.3-4 +- Rebuild for flocq 3.4.0 + +* Wed Dec 23 2020 Jerry James - 1.3.3-3 +- Rebuild for coq 8.12.2 + +* Wed Dec 2 2020 Jerry James - 1.3.3-2 +- Rebuild for coq 8.12.1 and menhir 20201201 + +* Fri Sep 25 2020 Jerry James - 1.3.3-1 +- Version 1.3.3 + +* Wed Sep 02 2020 Richard W.M. Jones - 1.3.1-14 +- OCaml 4.11.1 rebuild + +* Tue Sep 1 2020 Jerry James - 1.3.1-13 +- Rebuild for coq 8.12.0 + +* Mon Aug 24 2020 Richard W.M. Jones - 1.3.1-13 +- OCaml 4.11.0 rebuild + +* Thu Aug 6 2020 Jerry James - 1.3.1-12 +- Rebuild for ocaml-lablgtk3 3.1.1 and ocaml-menhir 20200624 + +* Wed Jul 29 2020 Fedora Release Engineering - 1.3.1-11 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild + +* Mon Jun 15 2020 Jerry James - 1.3.1-10 +- Rebuild for coq 8.11.2 + +* Sat Jun 13 2020 Jerry James - 1.3.1-9 +- Rebuild for flocq 3.3.1 +- Build the coq files with the native compiler when possible + +* Wed May 20 2020 Jerry James - 1.3.1-8 +- Rebuild for coq 8.11.1 + +* Tue May 05 2020 Richard W.M. Jones - 1.3.1-7 +- OCaml 4.11.0+dev2-2020-04-22 rebuild + +* Sun Apr 12 2020 Jerry James - 1.3.1-6 +- Make the dependencies on ocaml-num and ocaml-zip explicit (bz 1795083) + +* Wed Apr 8 2020 Jerry James - 1.3.1-5 +- Rebuild for flocq 3.2.1 + +* Sun Apr 05 2020 Richard W.M. Jones - 1.3.1-4 +- Update all OCaml dependencies for RPM 4.16. + +* Wed Apr 1 2020 Jerry James - 1.3.1-3 +- Do not build with mlmpfr; symbols clash with mlgmpidl, causing frama-c to + fail to start +- Obsolete the why2 packages + +* Sat Mar 28 2020 Jerry James - 1.3.1-2 +- Remove useless BRs and Rs (bz 1817878) + +* Wed Mar 25 2020 Jerry James - 1.3.1-1 +- Version 1.3.1 + +* Fri Jan 31 2020 Fedora Release Engineering - 1.2.1-4 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild + +* Wed Jan 22 2020 Jerry James - 1.2.1-3 +- OCaml 4.10.0+beta1 rebuild. + +* Fri Dec 06 2019 Richard W.M. Jones - 1.2.1-2 +- OCaml 4.09.0 (final) rebuild. + +* Tue Oct 29 2019 Jerry James - 1.2.1-1 +- New upstream release +- Add -proofgeneral subpackage +- Add desktop and AppData files + +* Fri Oct 11 2019 Jerry James - 1.2.0-6 +- Rebuild for ocaml-menhir 20190924 + +* Fri Sep 6 2019 Jerry James - 1.2.0-5 +- Rebuild for ocaml-zarith 1.9 + +* Thu Aug 1 2019 Jerry James - 1.2.0-4 +- Also install the library, for consumption by frama-c + +* Thu Aug 1 2019 Jerry James - 1.2.0-3 +- Rebuild for flocq 3.2.0 + +* Sat Jul 27 2019 Fedora Release Engineering - 1.2.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild + +* Wed Jun 5 2019 Jerry James - 1.2.0-1 +- New upstream release + +* Sun Feb 03 2019 Fedora Release Engineering - 1.1.1-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild + +* Sat Jan 26 2019 Jerry James - 1.1.1-1 +- New upstream release + +* Sat Jul 14 2018 Fedora Release Engineering - 0.88.3-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild + +* Thu Jul 12 2018 Richard W.M. Jones - 0.88.3-4 +- OCaml 4.07.0 (final) rebuild. + +* Wed Jun 20 2018 Richard W.M. Jones - 0.88.3-3 +- Bump release and rebuild. + +* Wed Jun 20 2018 Richard W.M. Jones - 0.88.3-2 +- OCaml 4.07.0-rc1 rebuild. + +* Mon Feb 12 2018 Jerry James - 0.88.3-1 +- New upstream release + +* Fri Feb 09 2018 Fedora Release Engineering - 0.88.2-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild + +* Sat Dec 9 2017 Jerry James - 0.88.2-1 +- New upstream release + +* Fri Nov 17 2017 Richard W.M. Jones - 0.88.1-1 +- New upstream version 0.88.1. +- OCaml 4.06.0 rebuild. + +* Sat Oct 7 2017 Jerry James - 0.88.0-1 +- New usptream release + +* Thu Oct 5 2017 Jerry James - 0.87.3-12 +- Rebuild for flocq 2.6.0 + +* Wed Sep 06 2017 Richard W.M. Jones - 0.87.3-11 +- OCaml 4.05.0 rebuild. + +* Thu Aug 03 2017 Fedora Release Engineering - 0.87.3-10 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild + +* Thu Jul 27 2017 Fedora Release Engineering - 0.87.3-9 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild + +* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-8 +- Bump release and rebuild. + +* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-7 +- Bump release and rebuild. + +* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-6 +- Bump release and rebuild. + +* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-5 +- OCaml 4.04.2 rebuild. + +* Fri May 12 2017 Richard W.M. Jones - 0.87.3-4 +- OCaml 4.04.1 rebuild. + +* Fri Mar 24 2017 Jerry James - 0.87.3-3 +- Rebuild to fix coq consistency issue + +* Sat Feb 11 2017 Fedora Release Engineering - 0.87.3-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild + +* Thu Jan 12 2017 Jerry James - 0.87.3-1 +- New upstream release + +* Mon Nov 07 2016 Richard W.M. Jones - 0.87.2-4 +- Rebuild for OCaml 4.04.0. + +* Fri Oct 28 2016 Jerry James - 0.87.2-3 +- Rebuild for coq 8.5pl3 +- Remove obsolete scriptlets +- Fix install location of why3lang.sty + +* Thu Sep 29 2016 Jerry James - 0.87.2-2 +- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1 + +* Fri Sep 2 2016 Jerry James - 0.87.2-1 +- New upstream release + +* Wed Jul 13 2016 Jerry James - 0.87.1-2 +- Rebuild for coq 8.5pl2 + +* Wed Jun 1 2016 Jerry James - 0.87.1-1 +- New upstream release + +* Fri Apr 22 2016 Jerry James - 0.87.0-3 +- Rebuild for coq 8.5pl1 + +* Sat Apr 16 2016 Jerry James - 0.87.0-2 +- Rebuild for ocaml-ocamlgraph 1.8.7 + +* Fri Mar 18 2016 Jerry James - 0.87.0-1 +- New upstream release +- Drop boomy icon removal; upstream no longer ships them + +* Fri Feb 12 2016 Jerry James - 0.86.3-1 +- New upstream release +- Use camlp4 in preference to camlp5 + +* Fri Feb 05 2016 Fedora Release Engineering - 0.86.2-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild + +* Wed Nov 25 2015 Jerry James - 0.86.2-2 +- Rebuild for ocaml-zarith 1.4.1 and ocaml-menhir 20151112 + +* Wed Oct 14 2015 Jerry James - 0.86.2-1 +- New upstream release +- Do not ship the nonfree boomy icons + +* Wed Jun 24 2015 Richard W.M. Jones - 0.86.1-2 +- ocaml-4.02.2 final rebuild. + +* Mon Jun 22 2015 Jerry James - 0.86.1-1 +- New upstream release + +* Wed Jun 17 2015 Richard W.M. Jones - 0.86-2 +- ocaml-4.02.2 rebuild. + +* Sat May 16 2015 Jerry James - 0.86-1 +- New upstream release + +* Sat Apr 11 2015 Jerry James - 0.85-9 +- Rebuild for coq 8.4pl6 + +* Wed Mar 18 2015 Jerry James - 0.85-8 +- Rebuild for ocaml-ocamlgraph 1.8.6 + +* Sat Feb 21 2015 Jerry James - 0.85-7 +- Note bundled jquery +- Fix sed expression separators for new RPM_OPT_FLAGS and RPM_LD_FLAGS + +* Wed Feb 18 2015 Richard W.M. Jones - 0.85-6 +- ocaml-4.02.1 rebuild. + +* Thu Nov 6 2014 Jerry James - 0.85-5 +- Rebuild for ocaml-camlp5 6.12 + +* Thu Oct 30 2014 Jerry James - 0.85-4 +- Rebuild for coq 8.4pl5 + +* Tue Oct 14 2014 Jerry James - 0.85-3 +- Rebuild for ocaml-zarith 1.3 + +* Thu Sep 18 2014 Jerry James - 0.85-2 +- Bump and rebuild + +* Wed Sep 17 2014 Jerry James - 0.85-1 +- New upstream release +- New source URL + +* Tue Sep 2 2014 Jerry James - 0.84-1 +- New upstream release +- Fix license handling + +* Mon Aug 25 2014 Jerry James - 0.83-14 +- Rebuild for new gappalib-coq build + +* Sun Aug 24 2014 Richard W.M. Jones - 0.83-13 +- ocaml-4.02.0+rc1 rebuild. + +* Mon Aug 18 2014 Fedora Release Engineering - 0.83-12 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild + +* Mon Aug 4 2014 Jerry James - 0.83-11 +- Rebuild for new gappalib-coq build + +* Sat Aug 02 2014 Richard W.M. Jones - 0.83-10 +- ocaml-4.02.0-0.8.git10e45753.fc22 rebuild. + +* Fri Aug 01 2014 Richard W.M. Jones - 0.83-9 +- OCaml 4.02.0 beta rebuild. + +* Thu Jun 26 2014 Jerry James - 0.83-8 +- Linking with -z relro -z now breaks plugins; omit "-z now" + +* Sun Jun 08 2014 Fedora Release Engineering - 0.83-7 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild + +* Tue May 13 2014 Jerry James - 0.83-6 +- Rebuild for coq 8.4pl4 + +* Mon Apr 21 2014 Jerry James - 0.83-5 +- Rebuild for flocq 2.3.0 and ocamlgraph 1.8.5 +- Drop unnecessary sqlite-devel BR + +* Tue Apr 15 2014 Richard W.M. Jones - 0.83-4 +- Remove ocaml_arches macro (RHBZ#1087794). + +* Mon Mar 24 2014 Jerry James - 0.83-3 +- Apply upstream fix for building with ocaml-zarith +- Fix file encodings +- Fix permission bits + +* Tue Mar 18 2014 Jerry James - 0.83-2 +- Back out the post-release fix to the Coq printer, which breaks Frama-C + +* Fri Mar 14 2014 Jerry James - 0.83-1 +- New upstream release +- Use cvc4 instead of cvc3 + +* Wed Feb 26 2014 Jerry James - 0.82-2 +- Rebuild for ocamlgraph 1.8.4 +- BR ocaml-findlib instead of ocaml-findlib-devel + +* Fri Dec 13 2013 Jerry James - 0.82-1 +- New upstream release +- Drop upstreamed patches +- Add -examples subpackage +- Install LaTeX style +- Turn off frama-c support at upstream's request + +* Mon Sep 30 2013 Jerry James - 0.81-6 +- Apply upstream fix for change in the alt-ergo timelimit option + +* Tue Sep 17 2013 Jerry James - 0.81-5 +- Rebuild for OCaml 4.01.0 +- Enable debuginfo for the ocaml sources + +* Sun Aug 04 2013 Fedora Release Engineering - 0.81-4 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild + +* Fri Jun 21 2013 Jerry James - 0.81-3 +- Rebuild for frama-c Fluorine 20130601 + +* Thu May 23 2013 Jerry James - 0.81-2 +- Rebuild for frama-c Fluorine 20130501 + +* Fri May 10 2013 Jerry James - 0.81-1 +- New upstream release +- Disable PVS support for now; it requires the NASA libraries +- Fix the conflict between the why and why3 Emacs packages (bz 913522) +- Disable parallel builds due to intermittent build failures + +* Fri Feb 15 2013 Fedora Release Engineering - 0.73-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild + +* Mon Jan 7 2013 Jerry James - 0.73-4 +- Rebuild for coq 8.4pl1 + +* Fri Dec 14 2012 Richard W.M. Jones - 0.73-3 +- Rebuild for OCaml 4.00.1. + +* Thu Aug 23 2012 Jerry James - 0.73-2 +- Rebuild for coq 8.4 + +* Thu Aug 2 2012 Jerry James - 0.73-1 +- New upstream release + +* Sun Jul 22 2012 Fedora Release Engineering - 0.71-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild + +* Thu Apr 19 2012 Jerry James - 0.71-2 +- Add missing sqlite-devel BR +- Do not move the coq plugin +- Generate debuginfo for the sole C program +- Add man pages + +* Fri Dec 16 2011 Jerry James - 0.71-1 +- Initial RPM diff --git a/why3.spec b/why3.spec index 9a05440..c88a5be 100644 --- a/why3.spec +++ b/why3.spec @@ -8,7 +8,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: why3 Version: 1.7.2 -Release: 10%{?dist} +Release: %autorelease Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -283,537 +283,4 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog -* Mon Oct 14 2024 Jerry James - 1.7.2-10 -- Fix the location of the icon - -* Sun Oct 6 2024 Jerry James - 1.7.2-9 -- Rebuild for ocaml-re 1.13.3 - -* Mon Aug 5 2024 Jerry James - 1.7.2-8 -- Rebuild for ocaml-menhir 20240715, ocaml-ppxlib 0.33.0, and ocaml-zip 1.1.2 - -* Sat Jul 20 2024 Fedora Release Engineering - 1.7.2-7 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild - -* Tue Jul 16 2024 Jerry James - 1.7.2-6 -- Rebuild for ocaml-zarith 1.14 - -* Wed Jul 3 2024 Jerry James - 1.7.2-5 -- Rebuild for ocaml-ppx-sexp-conv 0.17.0 - -* Wed Jun 19 2024 Richard W.M. Jones - 1.7.2-4 -- OCaml 5.2.0 ppc64le fix - -* Thu Jun 13 2024 Jerry James - 1.7.2-3 -- Rebuild for apron 0.9.15 -- New upstream URL - -* Thu May 30 2024 Richard W.M. Jones - 1.7.2-2 -- OCaml 5.2.0 for Fedora 41 - -* Thu Apr 18 2024 Jerry James - 1.7.2-1 -- Version 1.7.2 - -* Mon Mar 25 2024 Richard W.M. Jones - 1.7.1-3 -- Use %%{bash_completions_dir} macro - -* Fri Feb 2 2024 Jerry James - 1.7.1-2 -- Build again because koji ran out of disk space - -* Fri Feb 2 2024 Jerry James - 1.7.1-1 -- Version 1.7.1 - -* Sat Jan 27 2024 Fedora Release Engineering - 1.7.0-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild - -* Tue Jan 2 2024 Jerry James - 1.7.0-1 -- Version 1.7.0 -- Drop upstreamed coq patch - -* Mon Dec 18 2023 Richard W.M. Jones - 1.6.0-9 -- OCaml 5.1.1 + s390x code gen fix for Fedora 40 - -* Tue Dec 12 2023 Richard W.M. Jones - 1.6.0-8 -- OCaml 5.1.1 rebuild for Fedora 40 - -* Thu Oct 05 2023 Richard W.M. Jones - 1.6.0-7 -- OCaml 5.1 rebuild for Fedora 40 - -* Sat Sep 9 2023 Jerry James - 1.6.0-6 -- Rebuild for ocaml-ocamlgraph 2.1.0 - -* Sat Jul 29 2023 Jerry James - 1.6.0-5 -- Require cvc5 instead of cvc4 - -* Thu Jul 27 2023 Jerry James - 1.6.0-4 -- Rebuild for ocaml-zarith 1.13 - -* Sat Jul 22 2023 Fedora Release Engineering - 1.6.0-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild - -* Tue Jul 18 2023 Jerry James - 1.6.0-2 -- Validate metadata with appstream-util - -* Thu Jul 13 2023 Jerry James - 1.6.0-2 -- Rebuild for mpfr 4.2.0 - -* Mon Jul 10 2023 Jerry James - 1.6.0-1 -- Version 1.6.0 -- Enable inference with BDDs -- Add patch for coq 8.17 support - -* Sat Apr 1 2023 Jerry James - 1.5.1-7 -- Rebuild for coq 8.17.0 - -* Tue Jan 24 2023 Richard W.M. Jones - 1.5.1-6 -- Rebuild OCaml packages for F38 - -* Sat Jan 21 2023 Fedora Release Engineering - 1.5.1-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild - -* Fri Jan 6 2023 Jerry James - 1.5.1-4 -- BR tex(tgtermes.sty) to fix FTBFS with TeXLive 2022 - -* Sat Nov 26 2022 Jerry James - 1.5.1-3 -- Rebuild for coq 8.16.1 - -* Tue Nov 1 2022 Jerry James - 1.5.1-2 -- Rebuild for ocaml-ppxlib 0.28.0 - -* Fri Sep 16 2022 Jerry James - 1.5.1-1 -- Version 1.5.1 - -* Thu Aug 18 2022 Jerry James - 1.5.0-3 -- Rebuild to fix coq dependency -- Convert License tag to SPDX - -* Sat Jul 23 2022 Fedora Release Engineering - 1.5.0-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild - -* Tue Jul 19 2022 Jerry James - 1.5.0-1 -- Remove i686 support - -* Thu Jul 7 2022 Jerry James - 1.5.0-1 -- Version 1.5.0 -- Add ocaml-mlmpfr support -- Drop unmaintained man pages -- Use new OCaml macros - -* Sun Jun 19 2022 Richard W.M. Jones - 1.4.1-3 -- OCaml 4.14.0 rebuild - -* Fri Mar 25 2022 Jerry James - 1.4.1-2 -- Rebuild for coq 8.15.1 - -* Mon Feb 28 2022 Jerry James - 1.4.1-1 -- Version 1.4.1 - -* Fri Feb 04 2022 Richard W.M. Jones - 1.4.0-11 -- OCaml 4.13.1 rebuild to remove package notes - -* Sat Jan 22 2022 Fedora Release Engineering - 1.4.0-10 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild - -* Mon Jan 17 2022 Jerry James - 1.4.0-9 -- Rebuild for menhir 20211230 - -* Mon Dec 27 2021 Jerry James - 1.4.0-8 -- Rebuild for alt-ergo 2.3.0 and ocaml-zip 1.11 - -* Tue Nov 30 2021 Jerry James - 1.4.0-7 -- Rebuild for coq 8.14.1, sexplib0 0.15.0 and menhir 20211128 - -* Thu Oct 21 2021 Jerry James - 1.4.0-6 -- Rebuild for coq 8.14.0 and menhir 20211012 -- Add -coq8.14 patch -- Drop XEmacs support - -* Tue Oct 05 2021 Richard W.M. Jones - 1.4.0-5 -- OCaml 4.13.1 build - -* Mon Oct 04 2021 Richard W.M. Jones - 1.4.0-4 -- Try to build on s390x with OCaml 4.13 - -* Fri Jul 30 2021 Jerry James - 1.4.0-3 -- Rebuild for rebuilt coq - -* Fri Jul 23 2021 Fedora Release Engineering - 1.4.0-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild - -* 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-9 -- Rebuild for ocaml-menhir 20210419 - -* Wed Mar 3 2021 Jerry James - 1.3.3-8 -- Rebuild for coq 8.13.1 and ocaml-zarith 1.12 - -* Tue Mar 2 11:18:12 GMT 2021 Richard W.M. Jones - 1.3.3-7 -- OCaml 4.12.0 build - -* Sat Feb 20 2021 Jerry James - 1.3.3-6 -- Rebuild for coq 8.13.0 -- Update metainfo and install in metainfodir - -* Wed Jan 27 2021 Fedora Release Engineering - 1.3.3-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild - -* Sat Jan 2 2021 Jerry James - 1.3.3-4 -- Rebuild for flocq 3.4.0 - -* Wed Dec 23 2020 Jerry James - 1.3.3-3 -- Rebuild for coq 8.12.2 - -* Wed Dec 2 2020 Jerry James - 1.3.3-2 -- Rebuild for coq 8.12.1 and menhir 20201201 - -* Fri Sep 25 2020 Jerry James - 1.3.3-1 -- Version 1.3.3 - -* Wed Sep 02 2020 Richard W.M. Jones - 1.3.1-14 -- OCaml 4.11.1 rebuild - -* Tue Sep 1 2020 Jerry James - 1.3.1-13 -- Rebuild for coq 8.12.0 - -* Mon Aug 24 2020 Richard W.M. Jones - 1.3.1-13 -- OCaml 4.11.0 rebuild - -* Thu Aug 6 2020 Jerry James - 1.3.1-12 -- Rebuild for ocaml-lablgtk3 3.1.1 and ocaml-menhir 20200624 - -* Wed Jul 29 2020 Fedora Release Engineering - 1.3.1-11 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild - -* Mon Jun 15 2020 Jerry James - 1.3.1-10 -- Rebuild for coq 8.11.2 - -* Sat Jun 13 2020 Jerry James - 1.3.1-9 -- Rebuild for flocq 3.3.1 -- Build the coq files with the native compiler when possible - -* Wed May 20 2020 Jerry James - 1.3.1-8 -- Rebuild for coq 8.11.1 - -* Tue May 05 2020 Richard W.M. Jones - 1.3.1-7 -- OCaml 4.11.0+dev2-2020-04-22 rebuild - -* Sun Apr 12 2020 Jerry James - 1.3.1-6 -- Make the dependencies on ocaml-num and ocaml-zip explicit (bz 1795083) - -* Wed Apr 8 2020 Jerry James - 1.3.1-5 -- Rebuild for flocq 3.2.1 - -* Sun Apr 05 2020 Richard W.M. Jones - 1.3.1-4 -- Update all OCaml dependencies for RPM 4.16. - -* Wed Apr 1 2020 Jerry James - 1.3.1-3 -- Do not build with mlmpfr; symbols clash with mlgmpidl, causing frama-c to - fail to start -- Obsolete the why2 packages - -* Sat Mar 28 2020 Jerry James - 1.3.1-2 -- Remove useless BRs and Rs (bz 1817878) - -* Wed Mar 25 2020 Jerry James - 1.3.1-1 -- Version 1.3.1 - -* Fri Jan 31 2020 Fedora Release Engineering - 1.2.1-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild - -* Wed Jan 22 2020 Jerry James - 1.2.1-3 -- OCaml 4.10.0+beta1 rebuild. - -* Fri Dec 06 2019 Richard W.M. Jones - 1.2.1-2 -- OCaml 4.09.0 (final) rebuild. - -* Tue Oct 29 2019 Jerry James - 1.2.1-1 -- New upstream release -- Add -proofgeneral subpackage -- Add desktop and AppData files - -* Fri Oct 11 2019 Jerry James - 1.2.0-6 -- Rebuild for ocaml-menhir 20190924 - -* Fri Sep 6 2019 Jerry James - 1.2.0-5 -- Rebuild for ocaml-zarith 1.9 - -* Thu Aug 1 2019 Jerry James - 1.2.0-4 -- Also install the library, for consumption by frama-c - -* Thu Aug 1 2019 Jerry James - 1.2.0-3 -- Rebuild for flocq 3.2.0 - -* Sat Jul 27 2019 Fedora Release Engineering - 1.2.0-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild - -* Wed Jun 5 2019 Jerry James - 1.2.0-1 -- New upstream release - -* Sun Feb 03 2019 Fedora Release Engineering - 1.1.1-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild - -* Sat Jan 26 2019 Jerry James - 1.1.1-1 -- New upstream release - -* Sat Jul 14 2018 Fedora Release Engineering - 0.88.3-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild - -* Thu Jul 12 2018 Richard W.M. Jones - 0.88.3-4 -- OCaml 4.07.0 (final) rebuild. - -* Wed Jun 20 2018 Richard W.M. Jones - 0.88.3-3 -- Bump release and rebuild. - -* Wed Jun 20 2018 Richard W.M. Jones - 0.88.3-2 -- OCaml 4.07.0-rc1 rebuild. - -* Mon Feb 12 2018 Jerry James - 0.88.3-1 -- New upstream release - -* Fri Feb 09 2018 Fedora Release Engineering - 0.88.2-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild - -* Sat Dec 9 2017 Jerry James - 0.88.2-1 -- New upstream release - -* Fri Nov 17 2017 Richard W.M. Jones - 0.88.1-1 -- New upstream version 0.88.1. -- OCaml 4.06.0 rebuild. - -* Sat Oct 7 2017 Jerry James - 0.88.0-1 -- New usptream release - -* Thu Oct 5 2017 Jerry James - 0.87.3-12 -- Rebuild for flocq 2.6.0 - -* Wed Sep 06 2017 Richard W.M. Jones - 0.87.3-11 -- OCaml 4.05.0 rebuild. - -* Thu Aug 03 2017 Fedora Release Engineering - 0.87.3-10 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild - -* Thu Jul 27 2017 Fedora Release Engineering - 0.87.3-9 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild - -* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-8 -- Bump release and rebuild. - -* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-7 -- Bump release and rebuild. - -* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-6 -- Bump release and rebuild. - -* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-5 -- OCaml 4.04.2 rebuild. - -* Fri May 12 2017 Richard W.M. Jones - 0.87.3-4 -- OCaml 4.04.1 rebuild. - -* Fri Mar 24 2017 Jerry James - 0.87.3-3 -- Rebuild to fix coq consistency issue - -* Sat Feb 11 2017 Fedora Release Engineering - 0.87.3-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild - -* Thu Jan 12 2017 Jerry James - 0.87.3-1 -- New upstream release - -* Mon Nov 07 2016 Richard W.M. Jones - 0.87.2-4 -- Rebuild for OCaml 4.04.0. - -* Fri Oct 28 2016 Jerry James - 0.87.2-3 -- Rebuild for coq 8.5pl3 -- Remove obsolete scriptlets -- Fix install location of why3lang.sty - -* Thu Sep 29 2016 Jerry James - 0.87.2-2 -- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1 - -* Fri Sep 2 2016 Jerry James - 0.87.2-1 -- New upstream release - -* Wed Jul 13 2016 Jerry James - 0.87.1-2 -- Rebuild for coq 8.5pl2 - -* Wed Jun 1 2016 Jerry James - 0.87.1-1 -- New upstream release - -* Fri Apr 22 2016 Jerry James - 0.87.0-3 -- Rebuild for coq 8.5pl1 - -* Sat Apr 16 2016 Jerry James - 0.87.0-2 -- Rebuild for ocaml-ocamlgraph 1.8.7 - -* Fri Mar 18 2016 Jerry James - 0.87.0-1 -- New upstream release -- Drop boomy icon removal; upstream no longer ships them - -* Fri Feb 12 2016 Jerry James - 0.86.3-1 -- New upstream release -- Use camlp4 in preference to camlp5 - -* Fri Feb 05 2016 Fedora Release Engineering - 0.86.2-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild - -* Wed Nov 25 2015 Jerry James - 0.86.2-2 -- Rebuild for ocaml-zarith 1.4.1 and ocaml-menhir 20151112 - -* Wed Oct 14 2015 Jerry James - 0.86.2-1 -- New upstream release -- Do not ship the nonfree boomy icons - -* Wed Jun 24 2015 Richard W.M. Jones - 0.86.1-2 -- ocaml-4.02.2 final rebuild. - -* Mon Jun 22 2015 Jerry James - 0.86.1-1 -- New upstream release - -* Wed Jun 17 2015 Richard W.M. Jones - 0.86-2 -- ocaml-4.02.2 rebuild. - -* Sat May 16 2015 Jerry James - 0.86-1 -- New upstream release - -* Sat Apr 11 2015 Jerry James - 0.85-9 -- Rebuild for coq 8.4pl6 - -* Wed Mar 18 2015 Jerry James - 0.85-8 -- Rebuild for ocaml-ocamlgraph 1.8.6 - -* Sat Feb 21 2015 Jerry James - 0.85-7 -- Note bundled jquery -- Fix sed expression separators for new RPM_OPT_FLAGS and RPM_LD_FLAGS - -* Wed Feb 18 2015 Richard W.M. Jones - 0.85-6 -- ocaml-4.02.1 rebuild. - -* Thu Nov 6 2014 Jerry James - 0.85-5 -- Rebuild for ocaml-camlp5 6.12 - -* Thu Oct 30 2014 Jerry James - 0.85-4 -- Rebuild for coq 8.4pl5 - -* Tue Oct 14 2014 Jerry James - 0.85-3 -- Rebuild for ocaml-zarith 1.3 - -* Thu Sep 18 2014 Jerry James - 0.85-2 -- Bump and rebuild - -* Wed Sep 17 2014 Jerry James - 0.85-1 -- New upstream release -- New source URL - -* Tue Sep 2 2014 Jerry James - 0.84-1 -- New upstream release -- Fix license handling - -* Mon Aug 25 2014 Jerry James - 0.83-14 -- Rebuild for new gappalib-coq build - -* Sun Aug 24 2014 Richard W.M. Jones - 0.83-13 -- ocaml-4.02.0+rc1 rebuild. - -* Mon Aug 18 2014 Fedora Release Engineering - 0.83-12 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild - -* Mon Aug 4 2014 Jerry James - 0.83-11 -- Rebuild for new gappalib-coq build - -* Sat Aug 02 2014 Richard W.M. Jones - 0.83-10 -- ocaml-4.02.0-0.8.git10e45753.fc22 rebuild. - -* Fri Aug 01 2014 Richard W.M. Jones - 0.83-9 -- OCaml 4.02.0 beta rebuild. - -* Thu Jun 26 2014 Jerry James - 0.83-8 -- Linking with -z relro -z now breaks plugins; omit "-z now" - -* Sun Jun 08 2014 Fedora Release Engineering - 0.83-7 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild - -* Tue May 13 2014 Jerry James - 0.83-6 -- Rebuild for coq 8.4pl4 - -* Mon Apr 21 2014 Jerry James - 0.83-5 -- Rebuild for flocq 2.3.0 and ocamlgraph 1.8.5 -- Drop unnecessary sqlite-devel BR - -* Tue Apr 15 2014 Richard W.M. Jones - 0.83-4 -- Remove ocaml_arches macro (RHBZ#1087794). - -* Mon Mar 24 2014 Jerry James - 0.83-3 -- Apply upstream fix for building with ocaml-zarith -- Fix file encodings -- Fix permission bits - -* Tue Mar 18 2014 Jerry James - 0.83-2 -- Back out the post-release fix to the Coq printer, which breaks Frama-C - -* Fri Mar 14 2014 Jerry James - 0.83-1 -- New upstream release -- Use cvc4 instead of cvc3 - -* Wed Feb 26 2014 Jerry James - 0.82-2 -- Rebuild for ocamlgraph 1.8.4 -- BR ocaml-findlib instead of ocaml-findlib-devel - -* Fri Dec 13 2013 Jerry James - 0.82-1 -- New upstream release -- Drop upstreamed patches -- Add -examples subpackage -- Install LaTeX style -- Turn off frama-c support at upstream's request - -* Mon Sep 30 2013 Jerry James - 0.81-6 -- Apply upstream fix for change in the alt-ergo timelimit option - -* Tue Sep 17 2013 Jerry James - 0.81-5 -- Rebuild for OCaml 4.01.0 -- Enable debuginfo for the ocaml sources - -* Sun Aug 04 2013 Fedora Release Engineering - 0.81-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild - -* Fri Jun 21 2013 Jerry James - 0.81-3 -- Rebuild for frama-c Fluorine 20130601 - -* Thu May 23 2013 Jerry James - 0.81-2 -- Rebuild for frama-c Fluorine 20130501 - -* Fri May 10 2013 Jerry James - 0.81-1 -- New upstream release -- Disable PVS support for now; it requires the NASA libraries -- Fix the conflict between the why and why3 Emacs packages (bz 913522) -- Disable parallel builds due to intermittent build failures - -* Fri Feb 15 2013 Fedora Release Engineering - 0.73-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild - -* Mon Jan 7 2013 Jerry James - 0.73-4 -- Rebuild for coq 8.4pl1 - -* Fri Dec 14 2012 Richard W.M. Jones - 0.73-3 -- Rebuild for OCaml 4.00.1. - -* Thu Aug 23 2012 Jerry James - 0.73-2 -- Rebuild for coq 8.4 - -* Thu Aug 2 2012 Jerry James - 0.73-1 -- New upstream release - -* Sun Jul 22 2012 Fedora Release Engineering - 0.71-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild - -* Thu Apr 19 2012 Jerry James - 0.71-2 -- Add missing sqlite-devel BR -- Do not move the coq plugin -- Generate debuginfo for the sole C program -- Add man pages - -* Fri Dec 16 2011 Jerry James - 0.71-1 -- Initial RPM +%autochangelog From d46d748db4f410b4117a3991120477b724062201 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 10 Jan 2025 10:30:03 -0700 Subject: [PATCH 21/47] OCaml 5.3.0 rebuild for Fedora 42 - Version 1.8.0 - Disable documentation build due to bugs in 1.8.0 --- sources | 2 +- why3-link-order.patch | 20 ++++++++++++++++++++ why3.spec | 28 ++++++++++++++++++---------- 3 files changed, 39 insertions(+), 11 deletions(-) create mode 100644 why3-link-order.patch diff --git a/sources b/sources index a941d8e..99a1865 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (why3-1.7.2.tar.gz) = 7e80671480ce0dc3c69514bea2836f5899c686b43a4e8607c27d28e63f78150150dc45fcac5760dbee9721d363e456b1dcaeb1501fc9f63f360722a1021f675f +SHA512 (why3-1.8.0.tar.gz) = 8d30ac4a1280a7d7741ef862365e06aa3218a78fd01ca7f969f0d6515245c7259fcc81897bfe08c581c6b37639d1465ab4a96657f3baf4c747988df8201d4549 diff --git a/why3-link-order.patch b/why3-link-order.patch new file mode 100644 index 0000000..25cfeec --- /dev/null +++ b/why3-link-order.patch @@ -0,0 +1,20 @@ +Fixes this error: + +File "_none_", line 1: +Error: Forward reference to "Ptree_helpers" in file "src/bddinfer/why3infer.cmo" + +--- why3-1.8.0/Makefile.in.orig 2024-12-11 06:21:37.000000000 -0700 ++++ why3-1.8.0/Makefile.in 2024-12-16 10:27:14.100846332 -0700 +@@ -318,10 +318,10 @@ LIBMODULES = $(addprefix src/util/, $(L + $(addprefix src/core/, $(LIB_CORE)) \ + $(addprefix src/driver/, $(LIB_DRIVER)) \ + $(addprefix src/mlw/, $(LIB_MLW)) \ +- $(addprefix src/infer/, $(LIB_INFER)) \ +- $(addprefix src/bddinfer/, $(LIB_BDDINFER)) \ + $(addprefix src/extract/, $(LIB_EXTRACT)) \ + $(addprefix src/parser/, $(LIB_PARSER)) \ ++ $(addprefix src/infer/, $(LIB_INFER)) \ ++ $(addprefix src/bddinfer/, $(LIB_BDDINFER)) \ + $(addprefix src/transform/, $(LIB_TRANSFORM)) \ + $(addprefix src/printer/, $(LIB_PRINTER)) \ + $(addprefix src/session/, $(LIB_SESSION)) diff --git a/why3.spec b/why3.spec index c88a5be..df74310 100644 --- a/why3.spec +++ b/why3.spec @@ -7,7 +7,7 @@ ExclusiveArch: %{ocaml_native_compiler} # release. Name: why3 -Version: 1.7.2 +Version: 1.8.0 Release: %autorelease Summary: Software verification platform @@ -19,12 +19,15 @@ Source0: https://why3.gitlabpages.inria.fr/releases/%{name}-%{version}.ta Source1: fr.lri.%{name}.desktop # AppData file written by Jerry James Source2: fr.lri.%{name}.metainfo.xml +# Fix a link order issue +Patch: %{name}-link-order.patch BuildRequires: coq BuildRequires: emacs-nw BuildRequires: emacs-proofgeneral BuildRequires: flocq BuildRequires: graphviz +BuildRequires: java-devel BuildRequires: latexmk BuildRequires: libappstream-glib BuildRequires: make @@ -69,10 +72,7 @@ Recommends: flocq Provides: bundled(js-jquery) # The corresponding Provides is not generated, so filter this out -%global __requires_exclude ocaml\\\((Driver_ast|Why3)\\\) - -# This can be removed when F39 reaches EOL -Obsoletes: %{name}-xemacs < 1.4.0-4 +%global __requires_exclude ocaml\\\(Driver_ast\\\) %description Why3 is the next generation of the Why software verification platform. @@ -141,6 +141,7 @@ This package provides a why3 plugin for ProofGeneral. %prep %autosetup -p1 +%conf fixtimestamp() { touch -r $1.orig $1 rm $1.orig @@ -149,20 +150,26 @@ fixtimestamp() { # Use the correct compiler flags, keep timestamps, and harden the build due to # network use. Link the binaries with runtime compiled with -fPIC. # This avoids many link-time errors. -sed -e "s|-Wall|%{build_cflags}|;s/ -O -g//" \ - -e "s/cp /cp -p /" \ - -e "s|^OLINKFLAGS =.*|& -runtime-variant _pic -ccopt \"%{build_ldflags}\"|" \ +sed -e 's|-Wall|%{build_cflags} %{build_ldflags}|;s/ -O -g//' \ + -e 's/cp /cp -p /' \ + -e 's|^OLINKFLAGS =.*|& -runtime-variant _pic -ccopt "%{build_ldflags}"|' \ -i Makefile.in # Update the ProofGeneral integration instructions sed -i.orig 's,(MY_PATH_TO_WHY3)/share/whyitp,%{_emacs_sitelispdir},' share/whyitp/README fixtimestamp share/whyitp/README +# Fix a configure script typo +sed -i 's/\$(OCAMLC/$(ocamlc/' configure + %build %configure --enable-verbose-make --enable-bddinfer +# Work around a Makefile bug in version 1.8.0 +ln -s why3.opt bin/why3 # FIXME: Parallel make sometimes fails make -make doc +# The documentation build is broken in the 1.8.0 release +# make doc rm -f doc/html/.buildinfo examples/use_api/.merlin.in %install @@ -232,7 +239,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %{buildroot}%{ocamldir}/%{name}/*.cmxs %files -%doc AUTHORS CHANGES.md README.md doc/html doc/latex/manual.pdf +%doc AUTHORS CHANGES.md README.md %license LICENSE %{_bindir}/%{name} %{_bindir}/isabelle_client @@ -240,6 +247,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %{zsh_completions_dir}/_why3 %{_datadir}/%{name}/ %{_datadir}/applications/fr.lri.%{name}.desktop +%{_datadir}/gtksourceview-3.0/language-specs/coma.lang %{_datadir}/gtksourceview-3.0/language-specs/%{name}.lang %{_datadir}/gtksourceview-3.0/language-specs/%{name}c.lang %{_datadir}/gtksourceview-3.0/language-specs/%{name}py.lang From 3d1348dd5660beb4af7da040490f838e24bdd8ac Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sun, 19 Jan 2025 15:00:39 +0000 Subject: [PATCH 22/47] Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild From 7ab80d8d3e5d9831bf3b570fa686a87e281db5b0 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 22 Jan 2025 16:01:25 -0700 Subject: [PATCH 23/47] Add patch for C23 compatibility --- why3-c23.patch | 25 +++++++++++++++++++++++++ why3.spec | 2 ++ 2 files changed, 27 insertions(+) create mode 100644 why3-c23.patch diff --git a/why3-c23.patch b/why3-c23.patch new file mode 100644 index 0000000..736756b --- /dev/null +++ b/why3-c23.patch @@ -0,0 +1,25 @@ +Fixes this error: + +src/server/cpulimit-unix.c: In function ‘main’: +src/server/cpulimit-unix.c:95:23: error: assignment to ‘__sighandler_t’ {aka ‘void (*)(int)’} from incompatible pointer type ‘void (*)(void)’ [-Wincompatible-pointer-types] + 95 | sa.sa_handler = &wallclock_timelimit_reached; + | ^ +src/server/cpulimit-unix.c:45:6: note: ‘wallclock_timelimit_reached’ declared here + 45 | void wallclock_timelimit_reached() { + | ^~~~~~~~~~~~~~~~~~~~~~~~~~~ +In file included from src/server/cpulimit-unix.c:22: +/usr/include/signal.h:72:16: note: ‘__sighandler_t’ declared here + 72 | typedef void (*__sighandler_t) (int); + | ^~~~~~~~~~~~~~ + +--- why3-1.8.0/src/server/cpulimit-unix.c.orig 2024-12-11 06:21:37.000000000 -0700 ++++ why3-1.8.0/src/server/cpulimit-unix.c 2025-01-22 14:48:28.808369208 -0700 +@@ -42,7 +42,7 @@ void show_time() { + } + } + +-void wallclock_timelimit_reached() { ++void wallclock_timelimit_reached([[maybe_unused]] int sig) { + fprintf(stderr, + "Why3cpulimit: wallclock timelimit %d reached, killing command\n", + wallclock_timelimit); diff --git a/why3.spec b/why3.spec index df74310..12b1211 100644 --- a/why3.spec +++ b/why3.spec @@ -21,6 +21,8 @@ Source1: fr.lri.%{name}.desktop Source2: fr.lri.%{name}.metainfo.xml # Fix a link order issue Patch: %{name}-link-order.patch +# Fix an incompatible pointer issue with C23 +Patch: %{name}-c23.patch BuildRequires: coq BuildRequires: emacs-nw From d9a95c61897bdaed6a1adb0b0f1fe6bbd5d9e942 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 13 Feb 2025 14:41:57 -0700 Subject: [PATCH 24/47] Rebuild for flocq 4.2.1 From 525daf1052eea1914832f816692ff94ccd980c7b Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 15 Apr 2025 14:09:32 -0600 Subject: [PATCH 25/47] Rebuild for ocaml-ocamlgraph 2.2.0 From 9ec4d214c637445e124d5f5197dac87d39989de8 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 7 Jun 2025 10:34:13 -0600 Subject: [PATCH 26/47] Rebuild for bumped ocaml-mlgmpidl From 92927d0b7d8189b623450fbb86fdb93ae7e7b8f1 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 9 Jun 2025 15:05:43 -0600 Subject: [PATCH 27/47] Version 1.8.1 - All patches have been upstreamed --- sources | 2 +- why3-c23.patch | 25 ------------------------- why3-link-order.patch | 20 -------------------- why3.spec | 12 ++---------- 4 files changed, 3 insertions(+), 56 deletions(-) delete mode 100644 why3-c23.patch delete mode 100644 why3-link-order.patch diff --git a/sources b/sources index 99a1865..5946fe5 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (why3-1.8.0.tar.gz) = 8d30ac4a1280a7d7741ef862365e06aa3218a78fd01ca7f969f0d6515245c7259fcc81897bfe08c581c6b37639d1465ab4a96657f3baf4c747988df8201d4549 +SHA512 (why3-1.8.1.tar.gz) = b188b64cc8f116c2174e78d1ccb65dede0984265b8ed2fdf8160bf67e74bf9fb24cbb1d5b3c130f924424222b9241f89525cade66f5de7ef66d714eb2e6448b4 diff --git a/why3-c23.patch b/why3-c23.patch deleted file mode 100644 index 736756b..0000000 --- a/why3-c23.patch +++ /dev/null @@ -1,25 +0,0 @@ -Fixes this error: - -src/server/cpulimit-unix.c: In function ‘main’: -src/server/cpulimit-unix.c:95:23: error: assignment to ‘__sighandler_t’ {aka ‘void (*)(int)’} from incompatible pointer type ‘void (*)(void)’ [-Wincompatible-pointer-types] - 95 | sa.sa_handler = &wallclock_timelimit_reached; - | ^ -src/server/cpulimit-unix.c:45:6: note: ‘wallclock_timelimit_reached’ declared here - 45 | void wallclock_timelimit_reached() { - | ^~~~~~~~~~~~~~~~~~~~~~~~~~~ -In file included from src/server/cpulimit-unix.c:22: -/usr/include/signal.h:72:16: note: ‘__sighandler_t’ declared here - 72 | typedef void (*__sighandler_t) (int); - | ^~~~~~~~~~~~~~ - ---- why3-1.8.0/src/server/cpulimit-unix.c.orig 2024-12-11 06:21:37.000000000 -0700 -+++ why3-1.8.0/src/server/cpulimit-unix.c 2025-01-22 14:48:28.808369208 -0700 -@@ -42,7 +42,7 @@ void show_time() { - } - } - --void wallclock_timelimit_reached() { -+void wallclock_timelimit_reached([[maybe_unused]] int sig) { - fprintf(stderr, - "Why3cpulimit: wallclock timelimit %d reached, killing command\n", - wallclock_timelimit); diff --git a/why3-link-order.patch b/why3-link-order.patch deleted file mode 100644 index 25cfeec..0000000 --- a/why3-link-order.patch +++ /dev/null @@ -1,20 +0,0 @@ -Fixes this error: - -File "_none_", line 1: -Error: Forward reference to "Ptree_helpers" in file "src/bddinfer/why3infer.cmo" - ---- why3-1.8.0/Makefile.in.orig 2024-12-11 06:21:37.000000000 -0700 -+++ why3-1.8.0/Makefile.in 2024-12-16 10:27:14.100846332 -0700 -@@ -318,10 +318,10 @@ LIBMODULES = $(addprefix src/util/, $(L - $(addprefix src/core/, $(LIB_CORE)) \ - $(addprefix src/driver/, $(LIB_DRIVER)) \ - $(addprefix src/mlw/, $(LIB_MLW)) \ -- $(addprefix src/infer/, $(LIB_INFER)) \ -- $(addprefix src/bddinfer/, $(LIB_BDDINFER)) \ - $(addprefix src/extract/, $(LIB_EXTRACT)) \ - $(addprefix src/parser/, $(LIB_PARSER)) \ -+ $(addprefix src/infer/, $(LIB_INFER)) \ -+ $(addprefix src/bddinfer/, $(LIB_BDDINFER)) \ - $(addprefix src/transform/, $(LIB_TRANSFORM)) \ - $(addprefix src/printer/, $(LIB_PRINTER)) \ - $(addprefix src/session/, $(LIB_SESSION)) diff --git a/why3.spec b/why3.spec index 12b1211..b08043f 100644 --- a/why3.spec +++ b/why3.spec @@ -7,7 +7,7 @@ ExclusiveArch: %{ocaml_native_compiler} # release. Name: why3 -Version: 1.8.0 +Version: 1.8.1 Release: %autorelease Summary: Software verification platform @@ -19,10 +19,6 @@ Source0: https://why3.gitlabpages.inria.fr/releases/%{name}-%{version}.ta Source1: fr.lri.%{name}.desktop # AppData file written by Jerry James Source2: fr.lri.%{name}.metainfo.xml -# Fix a link order issue -Patch: %{name}-link-order.patch -# Fix an incompatible pointer issue with C23 -Patch: %{name}-c23.patch BuildRequires: coq BuildRequires: emacs-nw @@ -161,13 +157,9 @@ sed -e 's|-Wall|%{build_cflags} %{build_ldflags}|;s/ -O -g//' \ sed -i.orig 's,(MY_PATH_TO_WHY3)/share/whyitp,%{_emacs_sitelispdir},' share/whyitp/README fixtimestamp share/whyitp/README -# Fix a configure script typo -sed -i 's/\$(OCAMLC/$(ocamlc/' configure - %build %configure --enable-verbose-make --enable-bddinfer -# Work around a Makefile bug in version 1.8.0 -ln -s why3.opt bin/why3 + # FIXME: Parallel make sometimes fails make # The documentation build is broken in the 1.8.0 release From eef9515e6d3f9c7585829378f37d5abcbc4cc266 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 12 Jul 2025 16:48:04 -0600 Subject: [PATCH 28/47] Rebuild to fix OCaml dependencies From ddf170d66aea5be37ff01884592f5c6f7ff84da6 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 25 Jul 2025 20:24:57 +0000 Subject: [PATCH 29/47] Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild From 25a38102cfc023541d69de0ba02609e6893a1f13 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 10 Aug 2025 11:02:02 -0600 Subject: [PATCH 30/47] Bump and rebuild From 32bd519ce70092560444c001b8e8fc1becfcef12 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 10 Aug 2025 11:23:17 -0600 Subject: [PATCH 31/47] Use %{vimfiles_root} --- why3.spec | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/why3.spec b/why3.spec index b08043f..331b1cc 100644 --- a/why3.spec +++ b/why3.spec @@ -212,10 +212,10 @@ appstream-util validate-relax --nonet \ %{buildroot}%{_metainfodir}/fr.lri.%{name}.metainfo.xml # Move the vim file to the right place -mkdir -p %{buildroot}%{_datadir}/vim/vimfiles +mkdir -p %{buildroot}%{vimfiles_root} mv %{buildroot}%{_datadir}/%{name}/vim/ftdetect \ %{buildroot}%{_datadir}/%{name}/vim/syntax \ - %{buildroot}%{_datadir}/vim/vimfiles + %{buildroot}%{vimfiles_root} # Byte compile the Emacs support files cp -p share/whyitp/whyitp.el %{buildroot}%{_emacs_sitelispdir} @@ -246,8 +246,8 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %{_datadir}/gtksourceview-3.0/language-specs/%{name}c.lang %{_datadir}/gtksourceview-3.0/language-specs/%{name}py.lang %{_datadir}/icons/hicolor/scalable/apps/%{name}.svg -%{_datadir}/vim/vimfiles/ftdetect/%{name}.vim -%{_datadir}/vim/vimfiles/syntax/%{name}.vim +%{vimfiles_root}/ftdetect/%{name}.vim +%{vimfiles_root}/syntax/%{name}.vim %{_texmf}/tex/latex/why3/ %{_libdir}/%{name}/ %{_metainfodir}/fr.lri.%{name}.metainfo.xml From f24429dc72c9bfb48ed67ff3bc75193053d6a67e Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 10 Aug 2025 11:47:45 -0600 Subject: [PATCH 32/47] BR vim-filesystem for %{vimfiles_root} --- why3.spec | 1 + 1 file changed, 1 insertion(+) diff --git a/why3.spec b/why3.spec index 331b1cc..75df845 100644 --- a/why3.spec +++ b/why3.spec @@ -58,6 +58,7 @@ BuildRequires: tex(tgtermes.sty) BuildRequires: tex(upquote.sty) BuildRequires: tex(wrapfig.sty) BuildRequires: tex-urlbst +BuildRequires: vim-filesystem Requires: gtksourceview3%{?_isa} Requires: hicolor-icon-theme From dfde276402c5a9086b1851e9e336766131057fb2 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 22 Aug 2025 10:25:54 -0600 Subject: [PATCH 33/47] Rebuild for ocaml-unionfind 20250818 --- why3.spec | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/why3.spec b/why3.spec index 75df845..61a7d65 100644 --- a/why3.spec +++ b/why3.spec @@ -189,8 +189,8 @@ mkdir -p %{buildroot}%{zsh_completions_dir} cp -p share/zsh/_why3 %{buildroot}%{zsh_completions_dir} # Install the LaTeX style -mkdir -p %{buildroot}%{_texmf}/tex/latex/why3 -cp -p share/latex/why3lang.sty %{buildroot}%{_texmf}/tex/latex/why3 +mkdir -p %{buildroot}%{_texmf_main}/tex/latex/why3 +cp -p share/latex/why3lang.sty %{buildroot}%{_texmf_main}/tex/latex/why3 # Move the gtksourceview language file to the right place mkdir -p %{buildroot}%{_datadir}/gtksourceview-3.0 @@ -249,7 +249,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %{_datadir}/icons/hicolor/scalable/apps/%{name}.svg %{vimfiles_root}/ftdetect/%{name}.vim %{vimfiles_root}/syntax/%{name}.vim -%{_texmf}/tex/latex/why3/ +%{_texmf_main}/tex/latex/why3/ %{_libdir}/%{name}/ %{_metainfodir}/fr.lri.%{name}.metainfo.xml From 5d0415f73c56af5a5b68b1322b6c07e69d706767 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 5 Sep 2025 11:14:24 -0600 Subject: [PATCH 34/47] Rebuild for ocaml-menhir 20250903 From 10869d3c2e3e17871ea018f5e159a79b3cef5600 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 16 Sep 2025 15:25:39 -0600 Subject: [PATCH 35/47] Version 1.8.2 --- sources | 2 +- why3.spec | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/sources b/sources index 5946fe5..f503a9e 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (why3-1.8.1.tar.gz) = b188b64cc8f116c2174e78d1ccb65dede0984265b8ed2fdf8160bf67e74bf9fb24cbb1d5b3c130f924424222b9241f89525cade66f5de7ef66d714eb2e6448b4 +SHA512 (why3-1.8.2.tar.gz) = a35e88fafe1aa29c36d2248c1a644eae85afa1bb7b3009193f4a5c28ba684d0882717d63733d8581a7c2cd5ec493e2d15c82baabef615b4d00323fa9309875f8 diff --git a/why3.spec b/why3.spec index 61a7d65..7174465 100644 --- a/why3.spec +++ b/why3.spec @@ -7,7 +7,7 @@ ExclusiveArch: %{ocaml_native_compiler} # release. Name: why3 -Version: 1.8.1 +Version: 1.8.2 Release: %autorelease Summary: Software verification platform From c7de9116b86ffb1506e5e56ad42d4cfdaa5fc4a1 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 14 Oct 2025 20:54:37 +0100 Subject: [PATCH 36/47] OCaml 5.4.0 rebuild From e51d1ba9fcf860fc0689885e3385774d47702fa9 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 14 Jan 2026 08:53:03 -0700 Subject: [PATCH 37/47] Reflow the description text --- why3.spec | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/why3.spec b/why3.spec index 7174465..343cec9 100644 --- a/why3.spec +++ b/why3.spec @@ -74,12 +74,12 @@ Provides: bundled(js-jquery) %global __requires_exclude ocaml\\\(Driver_ast\\\) %description -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. +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. %package examples Summary: Example inputs @@ -104,16 +104,16 @@ Requires: %{name}%{?_isa} = %{version}-%{release} Requires: alt-ergo coq cvc5 E gappa yices-tools z3 zenon %description all -This package provides a complete software verification platform suite -based on Why3, including various automated and interactive provers. +This package provides a complete software verification platform suite based on +Why3, including various automated and interactive provers. %package -n ocaml-%{name} Summary: Software verification library for ocaml Requires: ocaml-zip-devel%{?_isa} %description -n ocaml-%{name} -This package contains an ocaml library that exposes the functionality -of why3 to applications. +This package contains an ocaml library that exposes the functionality of why3 +to applications. %package -n ocaml-%{name}-devel Summary: Development files for using the ocaml-%{name} library @@ -125,8 +125,8 @@ Requires: ocaml-sexplib-devel%{?_isa} Requires: ocaml-zip-devel%{?_isa} %description -n ocaml-%{name}-devel -This package contains development files needed to build applications -that use the ocaml-%{name} library. +This package contains development files needed to build applications that use +the ocaml-%{name} library. %package proofgeneral Summary: Why3 integration with ProofGeneral From d3d801816f3931eb255e31ae6affe8b1f17533fd Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 17 Jan 2026 20:13:59 +0000 Subject: [PATCH 38/47] Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild From a4c3815695573390e5bec5846405432fcfe62bd3 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 2 Feb 2026 16:26:22 -0700 Subject: [PATCH 39/47] Rebuild for ocaml-menhir 20260122 From e7d64b7f0f0b63d1490549dbc80b5c47a28a9195 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 6 Feb 2026 17:00:40 -0700 Subject: [PATCH 40/47] Rebuild for ocaml-menhir 20260203 From 5a8173d697f7319ab0238dc45c4de2b942791eb5 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 11 Feb 2026 20:03:06 -0700 Subject: [PATCH 41/47] Rebuild for ocaml-menhir-20260209 From 1889b3d497d0878b590075490921b32dc72abd8a Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Sat, 21 Feb 2026 00:12:57 +0000 Subject: [PATCH 42/47] OCaml 5.4.1 rebuild From f6d80e1a295c47c3582fab0e6bf2f1d5d943a8eb Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 19 Mar 2026 21:38:47 -0600 Subject: [PATCH 43/47] Rebuild for rocq 9.1.1 - Add patch to avoid Zmod, removed in rocq 9.1 --- why3-zmod.patch | 33 +++++++++++++++++++++++++++++++++ why3.spec | 5 ++++- 2 files changed, 37 insertions(+), 1 deletion(-) create mode 100644 why3-zmod.patch diff --git a/why3-zmod.patch b/why3-zmod.patch new file mode 100644 index 0000000..48f3ae4 --- /dev/null +++ b/why3-zmod.patch @@ -0,0 +1,33 @@ +--- why3-1.8.2/lib/coq/bv/BV_Gen.v.orig 2025-09-16 09:37:32.000000000 -0600 ++++ why3-1.8.2/lib/coq/bv/BV_Gen.v 2026-03-03 17:07:31.885655859 -0700 +@@ -994,7 +994,7 @@ match p with + ((Vector.last prev) :: (Vector.shiftout prev)) + end. + +-Lemma mod1_is_mod : forall x y, y > 0 -> mod1 x y = Zmod x y. ++Lemma mod1_is_mod : forall x y, y > 0 -> mod1 x y = Z.modulo x y. + intros; unfold mod1, div. + case Z_le_dec; intro. + rewrite Z.mod_eq by lia; trivial. +--- why3-1.8.2/lib/coq/int/EuclideanDivision.v.orig 2025-09-16 09:37:32.000000000 -0600 ++++ why3-1.8.2/lib/coq/int/EuclideanDivision.v 2026-03-03 17:08:16.588687381 -0700 +@@ -21,7 +21,7 @@ Require Import Lia. + Definition div : Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z. + Proof. + intros x y. +-case (Z_le_dec 0 (Zmod x y)) ; intros H. ++case (Z_le_dec 0 (Z.modulo x y)) ; intros H. + exact (Z.div x y). + exact (Z.div x y + 1)%Z. + Defined. +--- why3-1.8.2/lib/coq/number/Divisibility.v.orig 2025-09-16 09:37:32.000000000 -0600 ++++ why3-1.8.2/lib/coq/number/Divisibility.v 2026-03-03 17:08:33.884500190 -0700 +@@ -203,7 +203,7 @@ Lemma divides_mod_euclidean : + divides b a -> ((int.EuclideanDivision.mod1 a b) = 0%Z). + Proof. + intros a b Zb H. +-assert (Zmod a b = Z0). ++assert (Z.modulo a b = Z0). + now apply Zdivide_mod. + unfold mod1, div. + rewrite H0. diff --git a/why3.spec b/why3.spec index 343cec9..2f0fe19 100644 --- a/why3.spec +++ b/why3.spec @@ -19,8 +19,10 @@ Source0: https://why3.gitlabpages.inria.fr/releases/%{name}-%{version}.ta Source1: fr.lri.%{name}.desktop # AppData file written by Jerry James Source2: fr.lri.%{name}.metainfo.xml +# The deprecated Zmod alias was removed in rocq-stdlib 9.1.0 +Patch: %{name}-zmod.patch -BuildRequires: coq +BuildRequires: coq-core-compat BuildRequires: emacs-nw BuildRequires: emacs-proofgeneral BuildRequires: flocq @@ -47,6 +49,7 @@ BuildRequires: ocaml-zarith-devel BuildRequires: ocaml-zip-devel BuildRequires: %{py3_dist sphinx} BuildRequires: %{py3_dist sphinxcontrib-bibtex} +BuildRequires: rocq BuildRequires: tex(capt-of.sty) BuildRequires: tex(comment.sty) BuildRequires: tex(fncychap.sty) From cfd29ec6fddef49171f54f8ee670c272e6764fbd Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 16 Apr 2026 12:23:41 -0600 Subject: [PATCH 44/47] Rebuild for rocq 9.2.0 --- why3-rocq-9.2.patch | 292 ++++++++++++++++++++++++++++++++++++++++++++ why3.spec | 2 + 2 files changed, 294 insertions(+) create mode 100644 why3-rocq-9.2.patch diff --git a/why3-rocq-9.2.patch b/why3-rocq-9.2.patch new file mode 100644 index 0000000..9b2042c --- /dev/null +++ b/why3-rocq-9.2.patch @@ -0,0 +1,292 @@ +--- why3-1.8.2/lib/coq/ieee_float/GenericFloat.v.orig 2025-09-16 09:37:32.000000000 -0600 ++++ why3-1.8.2/lib/coq/ieee_float/GenericFloat.v 2026-04-12 21:00:50.656964191 -0600 +@@ -476,7 +476,7 @@ Qed. + + Lemma is_nan_dec: forall x, {is_nan x} + {~ is_nan x}. + Proof. +- intro; destruct x; compute; intuition. ++ intro; destruct x; compute; intuition; auto with *. + Qed. + + Lemma eq_not_nan_refl: forall {x : t}, ~ is_nan x -> eq x x. +--- why3-1.8.2/lib/coq/map/Occ.v.orig 2025-09-16 09:37:32.000000000 -0600 ++++ why3-1.8.2/lib/coq/map/Occ.v 2026-04-12 20:11:22.595468204 -0600 +@@ -241,10 +241,10 @@ now rewrite occ_empty; lia. + destruct (why_decidable_eq (m (l + (x-1))%Z) v). + assert (m (l + (x - 1)) <> v)%Z. + apply H1; lia. +-intuition. ++intuition; auto with *. + rewrite occ_right_no_add. + replace (l+x-1)%Z with (l+(x-1))%Z by ring. +-apply H; intuition. ++apply H; intuition; auto with *. + apply (H1 i). lia. assumption. + lia. + replace (l + x - 1)%Z with (l+(x-1))%Z by ring. +--- why3-1.8.2/lib/coq/number/Prime.v.orig 2025-09-16 09:37:32.000000000 -0600 ++++ why3-1.8.2/lib/coq/number/Prime.v 2026-04-11 14:50:08.453344009 -0600 +@@ -34,6 +34,8 @@ intros p. + apply iff_trans with (2 := prime_alt p). + unfold prime, prime'. + intuition. ++lia. ++lia. + Qed. + + (* Why3 goal *) +--- why3-1.8.2/lib/coq/set/Cardinal.v.orig 2025-09-16 09:37:32.000000000 -0600 ++++ why3-1.8.2/lib/coq/set/Cardinal.v 2026-04-11 20:38:44.347517956 -0600 +@@ -165,9 +165,10 @@ destruct (Bool.bool_dec (s x) true) as [ + + exists (List.cons x l1). + split. + - constructor; auto. intro Habs. eapply h1 in Habs. unfold Map.set in Habs. +- destruct why_decidable_eq; intuition. ++ destruct why_decidable_eq; auto with *. + - unfold Map.set in h1. intros. specialize (h1 e). destruct why_decidable_eq; [| intuition]. subst. +- split; intuition. destruct H1; eauto. ++ split; auto with *. destruct H1; eauto. ++ auto with *. + + exists l1. + split; [auto|]. intros. specialize (h1 e). replace (Map.set s x false e) with (s e) in h1. + eauto. +@@ -184,12 +185,15 @@ induction l. + - destruct IHl. destruct H. + destruct (List.in_dec eq_dec a l). + + exists x. split; eauto. intros. rewrite H0. +- split; intuition. inversion H2; eauto. subst. assumption. ++ split; auto with *; intuition. apply List.in_cons. assumption. ++ inversion H2; eauto. subst. assumption. + + destruct (Pdec a). + ++ exists (List.cons a x). split. constructor; eauto. + rewrite H0. intro Habs. destruct Habs; eauto. + intros. simpl. rewrite H0. intuition. subst. assumption. +- ++ exists x. split; eauto. intros. rewrite H0. intuition. simpl in H2. destruct H2; try subst; intuition. ++ ++ exists x. split; eauto. intros. rewrite H0. auto with *; intuition. ++ apply List.in_cons. assumption. ++ simpl in H2. destruct H2; try subst; intuition. + Qed. + + (* Why3 goal *) +@@ -443,7 +447,7 @@ split; intros. + + eapply List.NoDup_incl_length; eauto. apply a0. intros e Hincl. eapply H2. assumption. + + eapply List.NoDup_incl_length; eauto. intros e Hincl. eapply H2. assumption. + } +- intuition. ++ intuition. auto with *. + } + rewrite Hnat. rewrite Nat2Z.inj_succ. ring. + Qed. +@@ -472,6 +476,7 @@ split. + assert (~ set.Set.mem x s'). + { unfold s'. unfold Map.set, set.Set.mem. + destruct why_decidable_eq; intuition. ++ discriminate H1. + } + eapply cardinal_add in H1. rewrite H1. ring. + unfold s'. eapply is_finite_remove. assumption. +--- why3-1.8.2/lib/coq/set/FsetInt.v.orig 2025-09-16 09:37:32.000000000 -0600 ++++ why3-1.8.2/lib/coq/set/FsetInt.v 2026-04-12 12:49:09.882660225 -0600 +@@ -127,8 +127,8 @@ Fixpoint seqZ l len : list Numbers.BinNu + + Lemma seqZ_le: forall len x l, List.In x (seqZ l len) -> (l <= x)%Z. + Proof. +-induction len; simpl; intuition. +-eapply IHlen in H0; intuition. ++induction len; simpl; intuition. auto with *. ++eapply IHlen in H0; intuition. auto with *. + Qed. + + Lemma seqZ_le2: forall len x l, List.In x (seqZ l len) -> (x < l + Z.of_nat len)%Z. +@@ -184,8 +184,9 @@ destruct (Z_le_dec l r). + destruct Z_le_dec. + * destruct Z_lt_dec. split; intros; [reflexivity|]. + intuition. +- intuition ; try inversion H. +- * intuition ; try inversion H. ++ intuition ; auto with *; try inversion H. ++ intuition ; auto with *; try inversion H. ++ * intuition ; auto with *; try inversion H. + + exists List.nil. + split. + - constructor. +@@ -230,9 +231,10 @@ destruct (Z_le_dec l r). + split. apply seqZ_NoDup. + intros. rewrite seqZ_In_iff. + rewrite Z2Nat.id; [|lia]. +- destruct Z_le_dec; try destruct Z_lt_dec; intuition; try inversion H. ++ destruct Z_le_dec; try destruct Z_lt_dec; intuition; auto with *; try inversion H. + + exists nil. split. constructor. + simpl. intros. destruct Z_le_dec; try destruct Z_lt_dec; intuition. ++ auto with *. auto with *. auto with *. + Qed. + + +@@ -265,6 +267,6 @@ split. + + intros. destruct a. + destruct x. reflexivity. + specialize (H2 z). contradict H2. destruct Z_le_dec. +- destruct Z_lt_dec. lia. intuition. intuition. ++ destruct Z_lt_dec. lia. intuition; auto with *. intuition; auto with *. + Qed. + +--- why3-1.8.2/lib/coq/set/FsetSum.v.orig 2025-09-16 09:37:32.000000000 -0600 ++++ why3-1.8.2/lib/coq/set/FsetSum.v 2026-04-12 13:20:34.237382880 -0600 +@@ -101,8 +101,8 @@ destruct ClassicalEpsilon.constructive_i + destruct a0 as (Hx0dup, Hx0eq). destruct a1 as (Hx1dup, Hx1eq). + split. intros. + + eapply fold_left_iff_symm; eauto. +- * intuition. +- * intuition. ++ * intuition; auto with *. ++ * intuition; auto with *. + * intros. rewrite Hx0eq. rewrite Hx1eq. unfold Map.set. + destruct why_decidable_eq; try subst; intuition. + + intros. +@@ -113,19 +113,19 @@ split. intros. + erewrite <- (fold_left_iff_symm (List.app x0' x0'')); eauto. + * rewrite List.fold_left_app. rewrite fold_left_symm. + ++ auto. +- ++ intuition. +- ++ intuition. +- * intuition. +- * intuition. ++ ++ intuition; auto with *. ++ ++ intuition; auto with *. ++ * intuition; auto with *. ++ * intuition; auto with *. + * intros. rewrite List.in_app_iff. rewrite Hx0 in Hx0eq. + specialize (Hx0eq e). rewrite List.in_app_iff in Hx0eq. simpl in Hx0eq. + unfold Map.set in *. split; intros. + ++ destruct H2. + ** apply Hx1eq. destruct why_decidable_eq. +- -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition. ++ -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition; auto with *. + -- intuition. + ** eapply Hx1eq. destruct why_decidable_eq. +- -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition. ++ -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition; auto with *. + -- intuition. + ++ eapply Hx1eq in H2. + destruct why_decidable_eq. +@@ -177,11 +177,11 @@ destruct ClassicalEpsilon.constructive_i + destruct a1 as (Hdidup, Hdieq). + destruct a0 as (Hx0dup, Hx0eq). + destruct a2 as (Hx1dup, Hx1eq). +- rewrite fold_left_symm; try now intuition. ++ rewrite fold_left_symm; try now intuition; auto with *. + rewrite Z.add_0_l. rewrite <- List.fold_left_app. + eapply fold_left_iff_symm; eauto. +- + intuition. +- + intuition. ++ + intuition; auto with *. ++ + intuition; auto with *. + + intros. rewrite List.in_app_iff. rewrite Hx1eq. rewrite Hx0eq. + rewrite Hdieq. rewrite set.Set.diff'def. unfold set.Set.mem. + split; intros. +@@ -210,11 +210,11 @@ destruct ClassicalEpsilon.constructive_i + destruct a0 as (Hundup, Huneq). + destruct a1 as (Hx0dup, Hx0eq). + destruct a2 as (Hx1dup, Hx1eq). +- rewrite fold_left_symm; try now intuition. ++ rewrite fold_left_symm; try now intuition; auto with *. + rewrite Z.add_0_l. rewrite <- List.fold_left_app. + eapply fold_left_iff_symm; eauto. +- + intuition. +- + intuition. ++ + intuition; auto with *. ++ + intuition; auto with *. + + intros. rewrite List.in_app_iff. rewrite Hx1eq. rewrite Hx0eq. rewrite Huneq. + rewrite set.Set.union'def. clear - e. intuition. + + eapply Cardinal.NoDup_app; eauto. +@@ -312,7 +312,7 @@ assert (Z.of_nat (length (a0 :: x)) = Z. + simpl. rewrite Zpos_P_of_succ_nat. ring. + rewrite H. + rewrite IHx. rewrite @fold_left_symm; eauto. +-intuition. +-intuition. ++intuition; auto with *. ++intuition; auto with *. + Qed. + +--- why3-1.8.2/lib/coq/set/Fset.v.orig 2025-09-16 09:37:32.000000000 -0600 ++++ why3-1.8.2/lib/coq/set/Fset.v 2026-04-11 21:14:24.563998083 -0600 +@@ -103,12 +103,14 @@ Proof. + exists (fun x => false). + apply Cardinal.is_finite_empty. unfold set.Set.is_empty. + unfold set.Set.mem. intuition. ++discriminate H. + Defined. + + (* Why3 goal *) + Lemma is_empty_empty {a:Type} {a_WT:WhyType a} : is_empty (empty : fset a). + Proof. + unfold empty, is_empty, mem, set.Set.mem. intuition. ++discriminate H. + Qed. + + (* Why3 goal *) +@@ -118,6 +120,7 @@ Proof. + intros s h1. + eapply extensionality. intro. unfold empty, is_empty, mem, set.Set.mem in *. + destruct s. intuition. destruct (h1 _ H). ++discriminate H. + Qed. + + (* Why3 goal *) +@@ -163,6 +166,7 @@ Proof. + intros x s y. + unfold mem, remove, set.Set.mem, Map.set. destruct s. + destruct why_decidable_eq; intuition. ++discriminate H. discriminate H. + Qed. + + (* Why3 goal *) +--- why3-1.8.2/lib/coq/set/SetImpInt.v.orig 2025-09-16 09:37:32.000000000 -0600 ++++ why3-1.8.2/lib/coq/set/SetImpInt.v 2026-04-12 13:35:37.131334141 -0600 +@@ -48,6 +48,6 @@ Lemma choose'spec : + Proof. + intros s h1. + destruct h1. unfold to_fset, Fset.is_empty, Fset.mem, set.Set.mem. +-intuition. ++intuition. inversion H. + Qed. + +--- why3-1.8.2/lib/coq/set/SetImp.v.orig 2025-09-16 09:37:32.000000000 -0600 ++++ why3-1.8.2/lib/coq/set/SetImp.v 2026-04-12 13:28:53.584021692 -0600 +@@ -53,6 +53,6 @@ Lemma choose'spec : + Proof. + intros s h1. + destruct h1. unfold to_fset, Fset.is_empty, Fset.mem, set.Set.mem. +-intuition. ++intuition. inversion H. + Qed. + +--- why3-1.8.2/lib/coq/set/Set.v.orig 2025-09-16 09:37:32.000000000 -0600 ++++ why3-1.8.2/lib/coq/set/Set.v 2026-04-11 15:34:29.297022916 -0600 +@@ -139,6 +139,7 @@ Proof. + intros x s y. + unfold mem, Map.set. + destruct (why_decidable_eq x y) as [->|H] ; intuition. ++discriminate H. + Qed. + + (* Why3 goal *) +@@ -332,7 +333,7 @@ intuition. + destruct (s1 x); destruct (s2 x); intuition. + - rewrite <- H. + rewrite Bool.andb_true_iff. +- destruct (s2 x); intuition. ++ destruct (s2 x); auto with *. + Qed. + + (* Why3 goal *) +@@ -345,7 +346,7 @@ unfold disjoint, diff. + unfold mem. + intros x. + rewrite Bool.andb_true_iff. +-destruct (s2 x); intuition. ++destruct (s2 x); auto with *. + Qed. + + (* Why3 goal *) diff --git a/why3.spec b/why3.spec index 2f0fe19..e54851c 100644 --- a/why3.spec +++ b/why3.spec @@ -21,6 +21,8 @@ Source1: fr.lri.%{name}.desktop Source2: fr.lri.%{name}.metainfo.xml # The deprecated Zmod alias was removed in rocq-stdlib 9.1.0 Patch: %{name}-zmod.patch +# Adapt to changes in rocq 9.2.0 +Patch: %{name}-rocq-9.2.patch BuildRequires: coq-core-compat BuildRequires: emacs-nw From f8b7cae4a6e0252db85541e6bc3aae7d4429d9e1 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 9 Jul 2026 20:52:51 -0600 Subject: [PATCH 45/47] OCaml 5.5.0 rebuild --- why3.spec | 20 ++++---------------- 1 file changed, 4 insertions(+), 16 deletions(-) diff --git a/why3.spec b/why3.spec index e54851c..3d69c11 100644 --- a/why3.spec +++ b/why3.spec @@ -1,6 +1,3 @@ -# Coq's plugin architecture requires cmxs files, so: -ExclusiveArch: %{ocaml_native_compiler} - # NOTE: Upstream has said that the Frama-C support is still experimental, and # less functional than the corresponding support in why2. They recommend not # enabling it for now. We abide by their wishes. Revisit this decision each @@ -24,11 +21,13 @@ Patch: %{name}-zmod.patch # Adapt to changes in rocq 9.2.0 Patch: %{name}-rocq-9.2.patch +# Coq's plugin architecture requires cmxs files, so: +ExclusiveArch: %{ocaml_native_compiler} + BuildRequires: coq-core-compat BuildRequires: emacs-nw BuildRequires: emacs-proofgeneral BuildRequires: flocq -BuildRequires: graphviz BuildRequires: java-devel BuildRequires: latexmk BuildRequires: libappstream-glib @@ -41,7 +40,6 @@ BuildRequires: ocaml-lablgtk3-sourceview3-devel BuildRequires: ocaml-menhir BuildRequires: ocaml-mlmpfr-devel BuildRequires: ocaml-num-devel -BuildRequires: ocaml-ocamldoc BuildRequires: ocaml-ocamlgraph-devel BuildRequires: ocaml-ppx-deriving-devel BuildRequires: ocaml-ppx-sexp-conv-devel @@ -52,17 +50,7 @@ BuildRequires: ocaml-zip-devel BuildRequires: %{py3_dist sphinx} BuildRequires: %{py3_dist sphinxcontrib-bibtex} BuildRequires: rocq -BuildRequires: tex(capt-of.sty) -BuildRequires: tex(comment.sty) -BuildRequires: tex(fncychap.sty) -BuildRequires: tex(framed.sty) -BuildRequires: tex(latex) -BuildRequires: tex(needspace.sty) -BuildRequires: tex(tabulary.sty) -BuildRequires: tex(tgtermes.sty) -BuildRequires: tex(upquote.sty) -BuildRequires: tex(wrapfig.sty) -BuildRequires: tex-urlbst +BuildRequires: texlive-latex BuildRequires: vim-filesystem Requires: gtksourceview3%{?_isa} From 679e804de11e5f6845d679cc01841201c48b38ad Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 17 Jul 2026 08:48:20 +0000 Subject: [PATCH 46/47] Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild From cb0c5c7d69a0df1697f6f6ca2369f3b6feeca61b Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 29 Jul 2026 12:32:20 -0600 Subject: [PATCH 47/47] Rebuild for ocaml-ppx-deriving 6.1.3 --- why3.spec | 2 -- 1 file changed, 2 deletions(-) diff --git a/why3.spec b/why3.spec index 3d69c11..3fc4249 100644 --- a/why3.spec +++ b/why3.spec @@ -47,8 +47,6 @@ BuildRequires: ocaml-re-devel BuildRequires: ocaml-sexplib-devel BuildRequires: ocaml-zarith-devel BuildRequires: ocaml-zip-devel -BuildRequires: %{py3_dist sphinx} -BuildRequires: %{py3_dist sphinxcontrib-bibtex} BuildRequires: rocq BuildRequires: texlive-latex BuildRequires: vim-filesystem