From 525daf1052eea1914832f816692ff94ccd980c7b Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Tue, 15 Apr 2025 14:09:32 -0600
Subject: [PATCH 01/27] Rebuild for ocaml-ocamlgraph 2.2.0


From 9ec4d214c637445e124d5f5197dac87d39989de8 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Sat, 7 Jun 2025 10:34:13 -0600
Subject: [PATCH 02/27] Rebuild for bumped ocaml-mlgmpidl


From 92927d0b7d8189b623450fbb86fdb93ae7e7b8f1 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Mon, 9 Jun 2025 15:05:43 -0600
Subject: [PATCH 03/27] 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 e57fd9accfaf81866432af7e5630c0664d4e9273 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Mon, 9 Jun 2025 15:05:43 -0600
Subject: [PATCH 04/27] 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 <loganjerry@gmail.com>
Date: Sat, 12 Jul 2025 16:48:04 -0600
Subject: [PATCH 05/27] Rebuild to fix OCaml dependencies


From ddf170d66aea5be37ff01884592f5c6f7ff84da6 Mon Sep 17 00:00:00 2001
From: Fedora Release Engineering <releng@fedoraproject.org>
Date: Fri, 25 Jul 2025 20:24:57 +0000
Subject: [PATCH 06/27] Rebuilt for
 https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild


From 25a38102cfc023541d69de0ba02609e6893a1f13 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Sun, 10 Aug 2025 11:02:02 -0600
Subject: [PATCH 07/27] Bump and rebuild


From 32bd519ce70092560444c001b8e8fc1becfcef12 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Sun, 10 Aug 2025 11:23:17 -0600
Subject: [PATCH 08/27] 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 <loganjerry@gmail.com>
Date: Sun, 10 Aug 2025 11:47:45 -0600
Subject: [PATCH 09/27] 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 <loganjerry@gmail.com>
Date: Fri, 22 Aug 2025 10:25:54 -0600
Subject: [PATCH 10/27] 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 <loganjerry@gmail.com>
Date: Fri, 5 Sep 2025 11:14:24 -0600
Subject: [PATCH 11/27] Rebuild for ocaml-menhir 20250903


From 10869d3c2e3e17871ea018f5e159a79b3cef5600 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Tue, 16 Sep 2025 15:25:39 -0600
Subject: [PATCH 12/27] 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 655ea3197d32e2ec9f668e6fe9a12e0092bdc35d Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Sun, 10 Aug 2025 11:23:17 -0600
Subject: [PATCH 13/27] 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 78e4daa8311db633c3733c5ff2658684695e0496 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Sun, 10 Aug 2025 11:47:45 -0600
Subject: [PATCH 14/27] 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 d8e269ccc793c8eff76849bb49994dcb8359cb92 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Tue, 16 Sep 2025 15:25:39 -0600
Subject: [PATCH 15/27] 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 75df845..6b24ceb 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" <rjones@redhat.com>
Date: Tue, 14 Oct 2025 20:54:37 +0100
Subject: [PATCH 16/27] OCaml 5.4.0 rebuild


From e51d1ba9fcf860fc0689885e3385774d47702fa9 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Wed, 14 Jan 2026 08:53:03 -0700
Subject: [PATCH 17/27] 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 <releng@fedoraproject.org>
Date: Sat, 17 Jan 2026 20:13:59 +0000
Subject: [PATCH 18/27] Rebuilt for
 https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild


From a4c3815695573390e5bec5846405432fcfe62bd3 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Mon, 2 Feb 2026 16:26:22 -0700
Subject: [PATCH 19/27] Rebuild for ocaml-menhir 20260122


From e7d64b7f0f0b63d1490549dbc80b5c47a28a9195 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Fri, 6 Feb 2026 17:00:40 -0700
Subject: [PATCH 20/27] Rebuild for ocaml-menhir 20260203


From 5a8173d697f7319ab0238dc45c4de2b942791eb5 Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Wed, 11 Feb 2026 20:03:06 -0700
Subject: [PATCH 21/27] Rebuild for ocaml-menhir-20260209


From 1889b3d497d0878b590075490921b32dc72abd8a Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Sat, 21 Feb 2026 00:12:57 +0000
Subject: [PATCH 22/27] OCaml 5.4.1 rebuild


From f6d80e1a295c47c3582fab0e6bf2f1d5d943a8eb Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Thu, 19 Mar 2026 21:38:47 -0600
Subject: [PATCH 23/27] 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 <loganjerry@gmail.com>
Date: Thu, 16 Apr 2026 12:23:41 -0600
Subject: [PATCH 24/27] 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 <loganjerry@gmail.com>
Date: Thu, 9 Jul 2026 20:52:51 -0600
Subject: [PATCH 25/27] 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 <releng@fedoraproject.org>
Date: Fri, 17 Jul 2026 08:48:20 +0000
Subject: [PATCH 26/27] Rebuilt for
 https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild


From cb0c5c7d69a0df1697f6f6ca2369f3b6feeca61b Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Wed, 29 Jul 2026 12:32:20 -0600
Subject: [PATCH 27/27] 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