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 01/12] 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 02/12] 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 03/12] 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 04/12] 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 05/12] 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 06/12] 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 07/12] 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 08/12] 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 09/12] 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 10/12] 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 11/12] 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 12/12] 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