Rebuild for ocaml-ppx-deriving 6.1.3

- Add patch to avoid Zmod, removed in rocq 9.1

README.md

@@ -0,0 +1,16 @@
+# why3
+
+Why3 is a platform for deductive program verification.  It provides a rich
+language for specification and programming, called WhyML, and relies on
+external theorem provers, both automated and interactive, to discharge
+verification conditions.  (See the
+[list of supported provers](http://why3.lri.fr/#provers).)  Why3 comes with a
+standard library of logical theories (integer and real arithmetic, Boolean
+operations, sets and maps, etc.) and basic programming data structures
+(arrays, queues, hash tables, etc.).  A user can write WhyML programs directly
+and get correct-by-construction OCaml programs through an automated extraction
+mechanism.  WhyML is also used as an intermediate language for the
+verification of C, Java, or Ada programs.  (See the list of
+[Projects using Why3](http://why3.lri.fr/#users).)  Why3 can be extended
+easily with support for new theorem provers.  Why3 can be used as a software
+library, through an OCaml API.

changelog

@@ -0,0 +1,534 @@
+* Mon Oct 14 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-10
+- Fix the location of the icon
+
+* Sun Oct  6 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-9
+- Rebuild for ocaml-re 1.13.3
+
+* Mon Aug  5 2024 Jerry James <loganjerry@gmail.com> - 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 <releng@fedoraproject.org> - 1.7.2-7
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild
+
+* Tue Jul 16 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-6
+- Rebuild for ocaml-zarith 1.14
+
+* Wed Jul  3 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-5
+- Rebuild for ocaml-ppx-sexp-conv 0.17.0
+
+* Wed Jun 19 2024 Richard W.M. Jones <rjones@redhat.com> - 1.7.2-4
+- OCaml 5.2.0 ppc64le fix
+
+* Thu Jun 13 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-3
+- Rebuild for apron 0.9.15
+- New upstream URL
+
+* Thu May 30 2024 Richard W.M. Jones <rjones@redhat.com> - 1.7.2-2
+- OCaml 5.2.0 for Fedora 41
+
+* Thu Apr 18 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-1
+- Version 1.7.2
+
+* Mon Mar 25 2024 Richard W.M. Jones <rjones@redhat.com> - 1.7.1-3
+- Use %%{bash_completions_dir} macro
+
+* Fri Feb  2 2024 Jerry James <loganjerry@gmail.com> - 1.7.1-2
+- Build again because koji ran out of disk space
+
+* Fri Feb  2 2024 Jerry James <loganjerry@gmail.com> - 1.7.1-1
+- Version 1.7.1
+
+* Sat Jan 27 2024 Fedora Release Engineering <releng@fedoraproject.org> - 1.7.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
+
+* Tue Jan  2 2024 Jerry James <loganjerry@gmail.com> - 1.7.0-1
+- Version 1.7.0
+- Drop upstreamed coq patch
+
+* Mon Dec 18 2023 Richard W.M. Jones <rjones@redhat.com> - 1.6.0-9
+- OCaml 5.1.1 + s390x code gen fix for Fedora 40
+
+* Tue Dec 12 2023 Richard W.M. Jones <rjones@redhat.com> - 1.6.0-8
+- OCaml 5.1.1 rebuild for Fedora 40
+
+* Thu Oct 05 2023 Richard W.M. Jones <rjones@redhat.com> - 1.6.0-7
+- OCaml 5.1 rebuild for Fedora 40
+
+* Sat Sep  9 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-6
+- Rebuild for ocaml-ocamlgraph 2.1.0
+
+* Sat Jul 29 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-5
+- Require cvc5 instead of cvc4
+
+* Thu Jul 27 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-4
+- Rebuild for ocaml-zarith 1.13
+
+* Sat Jul 22 2023 Fedora Release Engineering <releng@fedoraproject.org> - 1.6.0-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
+
+* Tue Jul 18 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-2
+- Validate metadata with appstream-util
+
+* Thu Jul 13 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-2
+- Rebuild for mpfr 4.2.0
+
+* Mon Jul 10 2023 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 1.5.1-7
+- Rebuild for coq 8.17.0
+
+* Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 1.5.1-6
+- Rebuild OCaml packages for F38
+
+* Sat Jan 21 2023 Fedora Release Engineering <releng@fedoraproject.org> - 1.5.1-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
+
+* Fri Jan  6 2023 Jerry James <loganjerry@gmail.com> - 1.5.1-4
+- BR tex(tgtermes.sty) to fix FTBFS with TeXLive 2022
+
+* Sat Nov 26 2022 Jerry James <loganjerry@gmail.com> - 1.5.1-3
+- Rebuild for coq 8.16.1
+
+* Tue Nov  1 2022 Jerry James <loganjerry@gmail.com> - 1.5.1-2
+- Rebuild for ocaml-ppxlib 0.28.0
+
+* Fri Sep 16 2022 Jerry James <loganjerry@gmail.com> - 1.5.1-1
+- Version 1.5.1
+
+* Thu Aug 18 2022 Jerry James <loganjerry@gmail.com> - 1.5.0-3
+- Rebuild to fix coq dependency
+- Convert License tag to SPDX
+
+* Sat Jul 23 2022 Fedora Release Engineering <releng@fedoraproject.org> - 1.5.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
+
+* Tue Jul 19 2022 Jerry James <loganjerry@gmail.com> - 1.5.0-1
+- Remove i686 support
+
+* Thu Jul  7 2022 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 1.4.1-3
+- OCaml 4.14.0 rebuild
+
+* Fri Mar 25 2022 Jerry James <loganjerry@gmail.com> - 1.4.1-2
+- Rebuild for coq 8.15.1
+
+* Mon Feb 28 2022 Jerry James <loganjerry@gmail.com> - 1.4.1-1
+- Version 1.4.1
+
+* Fri Feb 04 2022 Richard W.M. Jones <rjones@redhat.com> - 1.4.0-11
+- OCaml 4.13.1 rebuild to remove package notes
+
+* Sat Jan 22 2022 Fedora Release Engineering <releng@fedoraproject.org> - 1.4.0-10
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
+
+* Mon Jan 17 2022 Jerry James <loganjerry@gmail.com> - 1.4.0-9
+- Rebuild for menhir 20211230
+
+* Mon Dec 27 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-8
+- Rebuild for alt-ergo 2.3.0 and ocaml-zip 1.11
+
+* Tue Nov 30 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-7
+- Rebuild for coq 8.14.1, sexplib0 0.15.0 and menhir 20211128
+
+* Thu Oct 21 2021 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 1.4.0-5
+- OCaml 4.13.1 build
+
+* Mon Oct 04 2021 Richard W.M. Jones <rjones@redhat.com> - 1.4.0-4
+- Try to build on s390x with OCaml 4.13
+
+* Fri Jul 30 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-3
+- Rebuild for rebuilt coq
+
+* Fri Jul 23 2021 Fedora Release Engineering <releng@fedoraproject.org> - 1.4.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
+
+* Wed Jul 14 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-1
+- Version 1.4.0
+- Drop all patches
+- Validate with appstreamcli instead of appstream-util
+
+* Tue Jun  8 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-9
+- Rebuild for ocaml-menhir 20210419
+
+* Wed Mar  3 2021 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 1.3.3-7
+- OCaml 4.12.0 build
+
+* Sat Feb 20 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-6
+- Rebuild for coq 8.13.0
+- Update metainfo and install in metainfodir
+
+* Wed Jan 27 2021 Fedora Release Engineering <releng@fedoraproject.org> - 1.3.3-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
+
+* Sat Jan  2 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-4
+- Rebuild for flocq 3.4.0
+
+* Wed Dec 23 2020 Jerry James <loganjerry@gmail.com> - 1.3.3-3
+- Rebuild for coq 8.12.2
+
+* Wed Dec  2 2020 Jerry James <loganjerry@gmail.com> - 1.3.3-2
+- Rebuild for coq 8.12.1 and menhir 20201201
+
+* Fri Sep 25 2020 Jerry James <loganjerry@gmail.com> - 1.3.3-1
+- Version 1.3.3
+
+* Wed Sep 02 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-14
+- OCaml 4.11.1 rebuild
+
+* Tue Sep  1 2020  Jerry James <loganjerry@gmail.com> - 1.3.1-13
+- Rebuild for coq 8.12.0
+
+* Mon Aug 24 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-13
+- OCaml 4.11.0 rebuild
+
+* Thu Aug  6 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-12
+- Rebuild for ocaml-lablgtk3 3.1.1 and ocaml-menhir 20200624
+
+* Wed Jul 29 2020 Fedora Release Engineering <releng@fedoraproject.org> - 1.3.1-11
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
+
+* Mon Jun 15 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-10
+- Rebuild for coq 8.11.2
+
+* Sat Jun 13 2020 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 1.3.1-8
+- Rebuild for coq 8.11.1
+
+* Tue May 05 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-7
+- OCaml 4.11.0+dev2-2020-04-22 rebuild
+
+* Sun Apr 12 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-6
+- Make the dependencies on ocaml-num and ocaml-zip explicit (bz 1795083)
+
+* Wed Apr  8 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-5
+- Rebuild for flocq 3.2.1
+
+* Sun Apr 05 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-4
+- Update all OCaml dependencies for RPM 4.16.
+
+* Wed Apr  1 2020 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 1.3.1-2
+- Remove useless BRs and Rs (bz 1817878)
+
+* Wed Mar 25 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-1
+- Version 1.3.1
+
+* Fri Jan 31 2020 Fedora Release Engineering <releng@fedoraproject.org> - 1.2.1-4
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
+
+* Wed Jan 22 2020 Jerry James <loganjerry@gmail.com> - 1.2.1-3
+- OCaml 4.10.0+beta1 rebuild.
+
+* Fri Dec 06 2019 Richard W.M. Jones <rjones@redhat.com> - 1.2.1-2
+- OCaml 4.09.0 (final) rebuild.
+
+* Tue Oct 29 2019 Jerry James <loganjerry@gmail.com> - 1.2.1-1
+- New upstream release
+- Add -proofgeneral subpackage
+- Add desktop and AppData files
+
+* Fri Oct 11 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-6
+- Rebuild for ocaml-menhir 20190924
+
+* Fri Sep  6 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-5
+- Rebuild for ocaml-zarith 1.9
+
+* Thu Aug  1 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-4
+- Also install the library, for consumption by frama-c
+
+* Thu Aug  1 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-3
+- Rebuild for flocq 3.2.0
+
+* Sat Jul 27 2019 Fedora Release Engineering <releng@fedoraproject.org> - 1.2.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
+
+* Wed Jun  5 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-1
+- New upstream release
+
+* Sun Feb 03 2019 Fedora Release Engineering <releng@fedoraproject.org> - 1.1.1-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
+
+* Sat Jan 26 2019 Jerry James <loganjerry@gmail.com> - 1.1.1-1
+- New upstream release
+
+* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 0.88.3-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
+
+* Thu Jul 12 2018 Richard W.M. Jones <rjones@redhat.com> - 0.88.3-4
+- OCaml 4.07.0 (final) rebuild.
+
+* Wed Jun 20 2018 Richard W.M. Jones <rjones@redhat.com> - 0.88.3-3
+- Bump release and rebuild.
+
+* Wed Jun 20 2018 Richard W.M. Jones <rjones@redhat.com> - 0.88.3-2
+- OCaml 4.07.0-rc1 rebuild.
+
+* Mon Feb 12 2018 Jerry James <loganjerry@gmail.com> - 0.88.3-1
+- New upstream release
+
+* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 0.88.2-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
+
+* Sat Dec  9 2017 Jerry James <loganjerry@gmail.com> - 0.88.2-1
+- New upstream release
+
+* Fri Nov 17 2017 Richard W.M. Jones <rjones@redhat.com> - 0.88.1-1
+- New upstream version 0.88.1.
+- OCaml 4.06.0 rebuild.
+
+* Sat Oct  7 2017 Jerry James <loganjerry@gmail.com> - 0.88.0-1
+- New usptream release
+
+* Thu Oct  5 2017 Jerry James <loganjerry@gmail.com> - 0.87.3-12
+- Rebuild for flocq 2.6.0
+
+* Wed Sep 06 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-11
+- OCaml 4.05.0 rebuild.
+
+* Thu Aug 03 2017 Fedora Release Engineering <releng@fedoraproject.org> - 0.87.3-10
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild
+
+* Thu Jul 27 2017 Fedora Release Engineering <releng@fedoraproject.org> - 0.87.3-9
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
+
+* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-8
+- Bump release and rebuild.
+
+* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-7
+- Bump release and rebuild.
+
+* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-6
+- Bump release and rebuild.
+
+* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-5
+- OCaml 4.04.2 rebuild.
+
+* Fri May 12 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-4
+- OCaml 4.04.1 rebuild.
+
+* Fri Mar 24 2017 Jerry James <loganjerry@gmail.com> - 0.87.3-3
+- Rebuild to fix coq consistency issue
+
+* Sat Feb 11 2017 Fedora Release Engineering <releng@fedoraproject.org> - 0.87.3-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
+
+* Thu Jan 12 2017 Jerry James <loganjerry@gmail.com> - 0.87.3-1
+- New upstream release
+
+* Mon Nov 07 2016 Richard W.M. Jones <rjones@redhat.com> - 0.87.2-4
+- Rebuild for OCaml 4.04.0.
+
+* Fri Oct 28 2016 Jerry James <loganjerry@gmail.com> - 0.87.2-3
+- Rebuild for coq 8.5pl3
+- Remove obsolete scriptlets
+- Fix install location of why3lang.sty
+
+* Thu Sep 29 2016 Jerry James <loganjerry@gmail.com> - 0.87.2-2
+- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1
+
+* Fri Sep  2 2016 Jerry James <loganjerry@gmail.com> - 0.87.2-1
+- New upstream release
+
+* Wed Jul 13 2016 Jerry James <loganjerry@gmail.com> - 0.87.1-2
+- Rebuild for coq 8.5pl2
+
+* Wed Jun  1 2016 Jerry James <loganjerry@gmail.com> - 0.87.1-1
+- New upstream release
+
+* Fri Apr 22 2016 Jerry James <loganjerry@gmail.com> - 0.87.0-3
+- Rebuild for coq 8.5pl1
+
+* Sat Apr 16 2016 Jerry James <loganjerry@gmail.com> - 0.87.0-2
+- Rebuild for ocaml-ocamlgraph 1.8.7
+
+* Fri Mar 18 2016 Jerry James <loganjerry@gmail.com> - 0.87.0-1
+- New upstream release
+- Drop boomy icon removal; upstream no longer ships them
+
+* Fri Feb 12 2016 Jerry James <loganjerry@gmail.com> - 0.86.3-1
+- New upstream release
+- Use camlp4 in preference to camlp5
+
+* Fri Feb 05 2016 Fedora Release Engineering <releng@fedoraproject.org> - 0.86.2-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
+
+* Wed Nov 25 2015 Jerry James <loganjerry@gmail.com> - 0.86.2-2
+- Rebuild for ocaml-zarith 1.4.1 and ocaml-menhir 20151112
+
+* Wed Oct 14 2015 Jerry James <loganjerry@gmail.com> - 0.86.2-1
+- New upstream release
+- Do not ship the nonfree boomy icons
+
+* Wed Jun 24 2015 Richard W.M. Jones <rjones@redhat.com> - 0.86.1-2
+- ocaml-4.02.2 final rebuild.
+
+* Mon Jun 22 2015 Jerry James <loganjerry@gmail.com> - 0.86.1-1
+- New upstream release
+
+* Wed Jun 17 2015 Richard W.M. Jones <rjones@redhat.com> - 0.86-2
+- ocaml-4.02.2 rebuild.
+
+* Sat May 16 2015 Jerry James <loganjerry@gmail.com> - 0.86-1
+- New upstream release
+
+* Sat Apr 11 2015 Jerry James <loganjerry@gmail.com> - 0.85-9
+- Rebuild for coq 8.4pl6
+
+* Wed Mar 18 2015 Jerry James <loganjerry@gmail.com> - 0.85-8
+- Rebuild for ocaml-ocamlgraph 1.8.6
+
+* Sat Feb 21 2015 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 0.85-6
+- ocaml-4.02.1 rebuild.
+
+* Thu Nov  6 2014 Jerry James <loganjerry@gmail.com> - 0.85-5
+- Rebuild for ocaml-camlp5 6.12
+
+* Thu Oct 30 2014 Jerry James <loganjerry@gmail.com> - 0.85-4
+- Rebuild for coq 8.4pl5
+
+* Tue Oct 14 2014 Jerry James <loganjerry@gmail.com> - 0.85-3
+- Rebuild for ocaml-zarith 1.3
+
+* Thu Sep 18 2014 Jerry James <loganjerry@gmail.com> - 0.85-2
+- Bump and rebuild
+
+* Wed Sep 17 2014 Jerry James <loganjerry@gmail.com> - 0.85-1
+- New upstream release
+- New source URL
+
+* Tue Sep  2 2014 Jerry James <loganjerry@gmail.com> - 0.84-1
+- New upstream release
+- Fix license handling
+
+* Mon Aug 25 2014 Jerry James <loganjerry@gmail.com> - 0.83-14
+- Rebuild for new gappalib-coq build
+
+* Sun Aug 24 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-13
+- ocaml-4.02.0+rc1 rebuild.
+
+* Mon Aug 18 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.83-12
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
+
+* Mon Aug  4 2014 Jerry James <loganjerry@gmail.com> - 0.83-11
+- Rebuild for new gappalib-coq build
+
+* Sat Aug 02 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-10
+- ocaml-4.02.0-0.8.git10e45753.fc22 rebuild.
+
+* Fri Aug 01 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-9
+- OCaml 4.02.0 beta rebuild.
+
+* Thu Jun 26 2014 Jerry James <loganjerry@gmail.com> - 0.83-8
+- Linking with -z relro -z now breaks plugins; omit "-z now"
+
+* Sun Jun 08 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.83-7
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
+
+* Tue May 13 2014 Jerry James <loganjerry@gmail.com> - 0.83-6
+- Rebuild for coq 8.4pl4
+
+* Mon Apr 21 2014 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 0.83-4
+- Remove ocaml_arches macro (RHBZ#1087794).
+
+* Mon Mar 24 2014 Jerry James <loganjerry@gmail.com> - 0.83-3
+- Apply upstream fix for building with ocaml-zarith
+- Fix file encodings
+- Fix permission bits
+
+* Tue Mar 18 2014 Jerry James <loganjerry@gmail.com> - 0.83-2
+- Back out the post-release fix to the Coq printer, which breaks Frama-C
+
+* Fri Mar 14 2014 Jerry James <loganjerry@gmail.com> - 0.83-1
+- New upstream release
+- Use cvc4 instead of cvc3
+
+* Wed Feb 26 2014 Jerry James <loganjerry@gmail.com> - 0.82-2
+- Rebuild for ocamlgraph 1.8.4
+- BR ocaml-findlib instead of ocaml-findlib-devel
+
+* Fri Dec 13 2013 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 0.81-6
+- Apply upstream fix for change in the alt-ergo timelimit option
+
+* Tue Sep 17 2013 Jerry James <loganjerry@gmail.com> - 0.81-5
+- Rebuild for OCaml 4.01.0
+- Enable debuginfo for the ocaml sources
+
+* Sun Aug 04 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.81-4
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild
+
+* Fri Jun 21 2013 Jerry James <loganjerry@gmail.com> - 0.81-3
+- Rebuild for frama-c Fluorine 20130601
+
+* Thu May 23 2013 Jerry James <loganjerry@gmail.com> - 0.81-2
+- Rebuild for frama-c Fluorine 20130501
+
+* Fri May 10 2013 Jerry James <loganjerry@gmail.com> - 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 <rel-eng@lists.fedoraproject.org> - 0.73-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild
+
+* Mon Jan  7 2013 Jerry James <loganjerry@gmail.com> - 0.73-4
+- Rebuild for coq 8.4pl1
+
+* Fri Dec 14 2012 Richard W.M. Jones <rjones@redhat.com> - 0.73-3
+- Rebuild for OCaml 4.00.1.
+
+* Thu Aug 23 2012 Jerry James <loganjerry@gmail.com> - 0.73-2
+- Rebuild for coq 8.4
+
+* Thu Aug  2 2012 Jerry James <loganjerry@gmail.com> - 0.73-1
+- New upstream release
+
+* Sun Jul 22 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.71-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
+
+* Thu Apr 19 2012 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 0.71-1
+- Initial RPM

fr.lri.why3.metainfo.xml

@@ -0,0 +1,48 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<component type="desktop-application">
+  <id>fr.lri.why3.desktop</id>
+  <metadata_license>0BSD</metadata_license>
+  <project_license>LGPL-2.1-only WITH OCaml-LGPL-linking-exception</project_license>
+  <name>Why3</name>
+  <summary>Software verification platform</summary>
+  <description>
+    <p>
+      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.
+    </p>
+  </description>
+  <launchable type="desktop-id">fr.lri.why3.desktop</launchable>
+  <screenshots>
+    <screenshot type="default">
+      <image>http://why3.lri.fr/doc/_images/gui-1.png</image>
+      <caption>Initial Why3 GUI window</caption>
+    </screenshot>
+    <screenshot>
+      <image>http://why3.lri.fr/doc/_images/gui-2.png</image>
+      <caption>The Why3 GUI with goal G1 selected</caption>
+    </screenshot>
+    <screenshot>
+      <image>http://why3.lri.fr/doc/_images/gui-3.png</image>
+      <caption>The Why3 GUI after running Alt-Ergo on each goal</caption>
+    </screenshot>
+    <screenshot>
+      <image>http://why3.lri.fr/doc/_images/gui-4.png</image>
+      <caption>The Why3 GUI after splitting goal G2</caption>
+    </screenshot>
+    <screenshot>
+      <image>http://why3.lri.fr/doc/_images/gui-5.png</image>
+      <caption>File reloaded after modifying goal G2</caption>
+    </screenshot>
+  </screenshots>
+  <update_contact>why3-maintainers@fedoraproject.org</update_contact>
+  <url type="homepage">http://why3.lri.fr/</url>
+  <url type="bugtracker">https://gitlab.inria.fr/why3/why3/issues</url>
+  <content_rating type="oars-1.1"></content_rating>
+  <provides>
+    <binary>why3</binary>
+  </provides>
+</component>

sources

@@ -1,2 +1 @@
-SHA512 (why3-man.tar.xz) = 8355776ac8a67a56ae7354f8fd40dc5d2057022d1035090a3e38e139fbfe3c258fe3ccbed6e333cb005e66c7b4cdbbf6580e3420170fd08384cc9b36ce5ec2a1
-SHA512 (why3-1.2.1.tar.gz) = 7a5d4403bda5a9c88490d83803a6c3d30b80b9949398de6d35b92df80a90980235c014d59afb46dd1bdd3028f20252ae1f59756a3d6978228e5c8fd9aefa1b3d
+SHA512 (why3-1.8.2.tar.gz) = a35e88fafe1aa29c36d2248c1a644eae85afa1bb7b3009193f4a5c28ba684d0882717d63733d8581a7c2cd5ec493e2d15c82baabef615b4d00323fa9309875f8

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 *)

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.

why3.appdata.xml

@@ -1,43 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<component type="desktop">
- <id>why3.desktop</id>
- <metadata_license>0BSD</metadata_license>
- <project_license>LGPL-2.1-only WITH OCaml-LGPL-linking-exception</project_license>
- <name>Why3</name>
- <summary>Software verification platform</summary>
- <description>
-  <p>
-   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.
-  </p>
- </description>
- <screenshots>
-  <screenshot type="default">
-   <image>http://why3.lri.fr/doc/gui-1.png</image>
-   <caption>Initial Why3 GUI window</caption>
-  </screenshot>
-  <screenshot>
-   <image>http://why3.lri.fr/doc/gui-2.png</image>
-   <image>The Why3 GUI with goal G1 selected</image>
-  </screenshot>
-  <screenshot>
-   <image>http://why3.lri.fr/doc/gui-3.png</image>
-   <image>The Why3 GUI after running Alt-Ergo on each goal</image>
-  </screenshot>
-  <screenshot>
-   <image>http://why3.lri.fr/doc/gui-4.png</image>
-   <image>The Why3 GUI after splitting goal G2</image>
-  </screenshot>
-  <screenshot>
-   <image>http://why3.lri.fr/doc/gui-5.png</image>
-   <image>File reloaded after modifying	 goal G2</image>
-  </screenshot>
- </screenshots>
- <updatecontact>loganjerry@gmail.com</updatecontact>
- <url type="homepage">http://why3.lri.fr/</url>
- <url type="bugtracker">https://gitlab.inria.fr/why3/why3/issues</url>
-</component>

why3.rpmlintrc

@@ -1,28 +0,0 @@
-# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON
-# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors
-
-# The dictionary lacks some technical words
-addFilter(r'W: spelling-error .* provers')
-
-# Caused by ocaml; this package cannot fix it
-addFilter(r'why3\.[^:]+: E: missing-call-to-chdir-with-chroot')
-
-# Indeed there is no documentation
-addFilter(r'ocaml-why3(|-devel).[^:]+: W: no-documentation')
-addFilter(r'why3-(all|emacs|xemacs).[^:]+: W: no-documentation')
-
-# This file is not a text file
-addFilter(r'W: file-not-utf8 .*\.mlw')
-
-# The TeX input carries its own character encoding declaration
-addFilter(r'why3-examples\.noarch: W: file-not-utf8 .*digit_sum\.tex')
-
-# The .notempty files are markers
-addFilter(r'why3-examples\.noarch: W: hidden-file-or-dir .*/\.notempty')
-addFilter(r'why3-examples\.noarch: E: zero-length .*/\.notempty')
-
-# We use the version of jquery provided by ocamldoc
-addFilter(r'W: unversioned-explicit-provides bundled\(jquery\)')
-
-# The man pages were created by the Fedora packager; there is no URL
-addFilter(r'why3\.spec: W: invalid-url Source1: why3-man\.tar\.xz')

why3.spec

@@ -3,67 +3,74 @@
 # 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.2.1
-Release:        1%{?dist}
+Version:        1.8.2
+Release:        %autorelease
 Summary:        Software verification platform
 
-# See LICENSE for the terms of the exception
-License:        LGPLv2 with exceptions
-URL:            http://why3.lri.fr/
-Source0:        https://gforge.inria.fr/frs/download.php/file/38185/%{name}-%{version}.tar.gz
-# Man pages written by Jerry James using text found in the sources.  Hence,
-# the copyright and license are the same as for the upstream sources.
-Source1:        %{name}-man.tar.xz
+License:        LGPL-2.1-only WITH OCaml-LGPL-linking-exception
+URL:            https://www.why3.org/
+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
-Source2:        %{name}.desktop
+Source1:        fr.lri.%{name}.desktop
 # AppData file written by Jerry James
-Source3:        %{name}.appdata.xml
+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
+# Coq's plugin architecture requires cmxs files, so:
+ExclusiveArch:  %{ocaml_native_compiler}
+
+BuildRequires:  coq-core-compat
+BuildRequires:  emacs-nw
 BuildRequires:  emacs-proofgeneral
-BuildRequires:  evince
 BuildRequires:  flocq
-BuildRequires:  hevea
+BuildRequires:  java-devel
+BuildRequires:  latexmk
 BuildRequires:  libappstream-glib
+BuildRequires:  make
 BuildRequires:  ocaml
-BuildRequires:  ocaml-camlp5-devel
+BuildRequires:  ocaml-apron-devel
+BuildRequires:  ocaml-camlidl-devel
 BuildRequires:  ocaml-findlib
-BuildRequires:  ocaml-lablgtk-devel
-BuildRequires:  ocaml-ocamldoc
-BuildRequires:  ocaml-ocamlgraph-devel
-BuildRequires:  ocaml-menhir-devel
+BuildRequires:  ocaml-lablgtk3-sourceview3-devel
+BuildRequires:  ocaml-menhir
+BuildRequires:  ocaml-mlmpfr-devel
 BuildRequires:  ocaml-num-devel
-BuildRequires:  ocaml-sqlite-devel
+BuildRequires:  ocaml-ocamlgraph-devel
+BuildRequires:  ocaml-ppx-deriving-devel
+BuildRequires:  ocaml-ppx-sexp-conv-devel
+BuildRequires:  ocaml-re-devel
+BuildRequires:  ocaml-sexplib-devel
 BuildRequires:  ocaml-zarith-devel
 BuildRequires:  ocaml-zip-devel
-BuildRequires:  pkgconfig(gtksourceview-2.0)
-BuildRequires:  rubber
-BuildRequires:  tex(comment.sty)
-BuildRequires:  tex(upquote.sty)
-BuildRequires:  tex-urlbst
-BuildRequires:  emacs xemacs xemacs-packages-extra
+BuildRequires:  rocq
+BuildRequires:  texlive-latex
+BuildRequires:  vim-filesystem
 
-Requires:       gtksourceview2
+Requires:       gtksourceview3%{?_isa}
 Requires:       hicolor-icon-theme
-Requires:       texlive-base
+Requires:       texlive-base%{?_isa}
 Requires:       vim-filesystem
-Provides:       bundled(jquery)
+
+Recommends:     bash-completion
+Recommends:     flocq
+
+Provides:       bundled(js-jquery)
 
 # The corresponding Provides is not generated, so filter this out
-%global __requires_exclude ocaml\\\(Why3\\\)
+%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
@@ -82,41 +89,35 @@ BuildArch:      noarch
 %description emacs
 This package contains an Emacs support file for working with %{name} files.
 
-%package xemacs
-Summary:        XEmacs support file for %{name} files
-Requires:       %{name} = %{version}-%{release}
-Requires:       xemacs(bin)
-BuildArch:      noarch
-
-%description xemacs
-This package contains an XEmacs support file for working with %{name} files.
-
 %package all
 Summary:        Complete Why3 software verification platform suite
 Requires:       %{name}%{?_isa} = %{version}-%{release}
-Requires:       alt-ergo coq cvc4 E gappalib-coq yices z3 zenon
+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
 Requires:       ocaml-%{name}%{?_isa} = %{version}-%{release}
-Requires:       ocaml-menhir-devel%{?_isa}
+Requires:       ocaml-menhir%{?_isa}
 Requires:       ocaml-num-devel%{?_isa}
+Requires:       ocaml-re-devel%{?_isa}
+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
@@ -128,105 +129,91 @@ BuildArch:      noarch
 This package provides a why3 plugin for ProofGeneral.
 
 %prep
-%setup -q
-%setup -q -T -D -a 1
+%autosetup -p1
 
+%conf
 fixtimestamp() {
   touch -r $1.orig $1
   rm $1.orig
 }
 
 # Use the correct compiler flags, keep timestamps, and harden the build due to
-# network use
-# Link the binaries with runtime compiled with -fPIC.
+# network use.  Link the binaries with runtime compiled with -fPIC.
 # This avoids many link-time errors.
-sed -e "s|-Wall|$RPM_OPT_FLAGS|;s/ -O -g//" \
-    -e "s/cp /cp -p /" \
-    -e "s|^OLINKFLAGS =.*|& -runtime-variant _pic -ccopt \"$RPM_LD_FLAGS\"|" \
+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
 
-# Remove spurious executable bits
-find -O3 examples -type f -perm /0111 -exec chmod a-x {} \+
-chmod a+x examples/*.sh
-
-# Remove spurious shebangs
-sed -i.orig '/#!.*/d' examples/use_api/runstrat/{echo,run}_wait.ml
-fixtimestamp examples/use_api/runstrat/echo_wait.ml
-fixtimestamp examples/use_api/runstrat/run_wait.ml
-
-# Fix end of line encodings
-sed -i.orig 's/\r//' examples/bts/20881.why
-fixtimestamp examples/bts/20881.why
-
 # Update the ProofGeneral integration instructions
 sed -i.orig 's,(MY_PATH_TO_WHY3)/share/whyitp,%{_emacs_sitelispdir},' share/whyitp/README
 fixtimestamp share/whyitp/README
 
 %build
-%configure --enable-verbose-make
-make #%%{?_smp_mflags}
-make doc/manual.pdf
+%configure --enable-verbose-make --enable-bddinfer
+
+# FIXME: Parallel make sometimes fails
+make
+# The documentation build is broken in the 1.8.0 release
+# make doc
+rm -f doc/html/.buildinfo examples/use_api/.merlin.in
 
 %install
-make install DESTDIR=%{buildroot}
-make install-lib DESTDIR=%{buildroot}
+%make_install
+make install-lib DESTDIR=%{?buildroot} INSTALL="%{__install} -p"
 
-# Install the man pages
-mkdir -p %{buildroot}%{_mandir}/man1
-cd man
-for f in *.1; do
-  sed "s/@version@/%{version}/" $f > %{buildroot}%{_mandir}/man1/$f
-  touch -r $f %{buildroot}%{_mandir}/man1/$f
+%ifarch %{ocaml_native_compiler}
+# Install the native coq files
+cd lib/coq
+for dir in $(find . -name .coq-native); do
+  cp -a $dir %{buildroot}%{_libdir}/%{name}/coq/$dir
 done
-cd ..
+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
-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
-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-2.0
+mkdir -p %{buildroot}%{_datadir}/gtksourceview-3.0
 mv %{buildroot}%{_datadir}/%{name}/lang \
-   %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs
+   %{buildroot}%{_datadir}/gtksourceview-3.0/language-specs
 
 # Install the desktop file
 mkdir -p %{buildroot}%{_datadir}/applications
-desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE2}
+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}
-cp -p %{SOURCE3} %{buildroot}%{_metainfodir}
-appstream-util validate-relax --nonet %{buildroot}%{_metainfodir}/%{name}.appdata.xml
+cp -p %{SOURCE2} %{buildroot}%{_metainfodir}
+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 (X)Emacs support files
-mkdir -p %{buildroot}%{_xemacs_sitelispdir}
-cp -p %{buildroot}%{_emacs_sitelispdir}/%{name}.el \
-   %{buildroot}%{_xemacs_sitelispdir}
+# Byte compile the Emacs support files
 cp -p share/whyitp/whyitp.el %{buildroot}%{_emacs_sitelispdir}
-pushd %{buildroot}%{_xemacs_sitelispdir}
-%{_xemacs_bytecompile} %{name}.el
 cd %{buildroot}%{_emacs_sitelispdir}
 %{_emacs_bytecompile} %{name}.el whyitp.el
-popd
+cd -
 
 # Remove misplaced documentation
 rm -fr %{buildroot}%{_datadir}/doc
@@ -235,41 +222,45 @@ rm -fr %{buildroot}%{_datadir}/doc
 chmod 0755 %{buildroot}%{_bindir}/* \
            %{buildroot}%{_libdir}/%{name}/commands/* \
            %{buildroot}%{_libdir}/%{name}/plugins/*.cmxs \
-           %{buildroot}%{_libdir}/ocaml/%{name}/*.cmxs
+           %{buildroot}%{ocamldir}/%{name}/*.cmxs
 
 %files
-%doc AUTHORS CHANGES.md README.md doc/manual.pdf
+%doc AUTHORS CHANGES.md README.md
 %license LICENSE
 %{_bindir}/%{name}
+%{_bindir}/isabelle_client
+%{bash_completions_dir}/why3
+%{zsh_completions_dir}/_why3
 %{_datadir}/%{name}/
-%{_datadir}/applications/%{name}.desktop
-%{_datadir}/bash-completion/
-%{_datadir}/gtksourceview-2.0/language-specs/%{name}.lang
-%{_datadir}/icons/hicolor/scalable/%{name}.svg
-%{_datadir}/vim/vimfiles/ftdetect/%{name}.vim
-%{_datadir}/vim/vimfiles/syntax/%{name}.vim
-%{_datadir}/zsh/
-%{_texmf}/tex/latex/why3/
+%{_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
+%{_datadir}/icons/hicolor/scalable/apps/%{name}.svg
+%{vimfiles_root}/ftdetect/%{name}.vim
+%{vimfiles_root}/syntax/%{name}.vim
+%{_texmf_main}/tex/latex/why3/
 %{_libdir}/%{name}/
-%{_mandir}/man1/%{name}*
-%{_metainfodir}/%{name}.appdata.xml
+%{_metainfodir}/fr.lri.%{name}.metainfo.xml
 
 %files -n ocaml-%{name}
-%dir %{_libdir}/ocaml/%{name}/
-%{_libdir}/ocaml/%{name}/META
-%{_libdir}/ocaml/%{name}/*.cmi
+%dir %{ocamldir}/%{name}/
+%{ocamldir}/%{name}/META
+%{ocamldir}/%{name}/*.cmi
 %ifarch %{ocaml_native_compiler}
-%{_libdir}/ocaml/%{name}/*.cmxs
+%{ocamldir}/%{name}/*.cmxs
 %endif
 
 %files -n ocaml-%{name}-devel
 %ifarch %{ocaml_native_compiler}
-%{_libdir}/ocaml/%{name}/*.a
-%{_libdir}/ocaml/%{name}/*.cmx
-%{_libdir}/ocaml/%{name}/*.cmxa
+%{ocamldir}/%{name}/*.a
+%{ocamldir}/%{name}/*.cmx
+%{ocamldir}/%{name}/*.cmxa
 %else
-%{_libdir}/ocaml/%{name}/*.cma
+%{ocamldir}/%{name}/*.cma
 %endif
+%{ocamldir}/%{name}/*.cmt
 
 %files examples
 %doc examples
@@ -277,9 +268,6 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %files emacs
 %{_emacs_sitelispdir}/%{name}.el*
 
-%files xemacs
-%{_xemacs_sitelispdir}/%{name}.el*
-
 %files proofgeneral
 %doc share/whyitp/README
 %{_emacs_sitelispdir}/whyitp.el*
@@ -289,290 +277,4 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %files all
 
 %changelog
-* Tue Oct 29 2019 Jerry James <loganjerry@gmail.com> - 1.2.1-1
-- New upstream release
-- Add -proofgeneral subpackage
-- Add desktop and AppData files
-
-* Fri Oct 11 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-6
-- Rebuild for ocaml-menhir 20190924
-
-* Fri Sep  6 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-5
-- Rebuild for ocaml-zarith 1.9
-
-* Thu Aug  1 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-4
-- Also install the library, for consumption by frama-c
-
-* Thu Aug  1 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-3
-- Rebuild for flocq 3.2.0
-
-* Sat Jul 27 2019 Fedora Release Engineering <releng@fedoraproject.org> - 1.2.0-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
-
-* Wed Jun  5 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-1
-- New upstream release
-
-* Sun Feb 03 2019 Fedora Release Engineering <releng@fedoraproject.org> - 1.1.1-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
-
-* Sat Jan 26 2019 Jerry James <loganjerry@gmail.com> - 1.1.1-1
-- New upstream release
-
-* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 0.88.3-5
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
-
-* Thu Jul 12 2018 Richard W.M. Jones <rjones@redhat.com> - 0.88.3-4
-- OCaml 4.07.0 (final) rebuild.
-
-* Wed Jun 20 2018 Richard W.M. Jones <rjones@redhat.com> - 0.88.3-3
-- Bump release and rebuild.
-
-* Wed Jun 20 2018 Richard W.M. Jones <rjones@redhat.com> - 0.88.3-2
-- OCaml 4.07.0-rc1 rebuild.
-
-* Mon Feb 12 2018 Jerry James <loganjerry@gmail.com> - 0.88.3-1
-- New upstream release
-
-* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 0.88.2-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
-
-* Sat Dec  9 2017 Jerry James <loganjerry@gmail.com> - 0.88.2-1
-- New upstream release
-
-* Fri Nov 17 2017 Richard W.M. Jones <rjones@redhat.com> - 0.88.1-1
-- New upstream version 0.88.1.
-- OCaml 4.06.0 rebuild.
-
-* Sat Oct  7 2017 Jerry James <loganjerry@gmail.com> - 0.88.0-1
-- New usptream release
-
-* Thu Oct  5 2017 Jerry James <loganjerry@gmail.com> - 0.87.3-12
-- Rebuild for flocq 2.6.0
-
-* Wed Sep 06 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-11
-- OCaml 4.05.0 rebuild.
-
-* Thu Aug 03 2017 Fedora Release Engineering <releng@fedoraproject.org> - 0.87.3-10
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild
-
-* Thu Jul 27 2017 Fedora Release Engineering <releng@fedoraproject.org> - 0.87.3-9
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
-
-* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-8
-- Bump release and rebuild.
-
-* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-7
-- Bump release and rebuild.
-
-* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-6
-- Bump release and rebuild.
-
-* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-5
-- OCaml 4.04.2 rebuild.
-
-* Fri May 12 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-4
-- OCaml 4.04.1 rebuild.
-
-* Fri Mar 24 2017 Jerry James <loganjerry@gmail.com> - 0.87.3-3
-- Rebuild to fix coq consistency issue
-
-* Sat Feb 11 2017 Fedora Release Engineering <releng@fedoraproject.org> - 0.87.3-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
-
-* Thu Jan 12 2017 Jerry James <loganjerry@gmail.com> - 0.87.3-1
-- New upstream release
-
-* Mon Nov 07 2016 Richard W.M. Jones <rjones@redhat.com> - 0.87.2-4
-- Rebuild for OCaml 4.04.0.
-
-* Fri Oct 28 2016 Jerry James <loganjerry@gmail.com> - 0.87.2-3
-- Rebuild for coq 8.5pl3
-- Remove obsolete scriptlets
-- Fix install location of why3lang.sty
-
-* Thu Sep 29 2016 Jerry James <loganjerry@gmail.com> - 0.87.2-2
-- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1
-
-* Fri Sep  2 2016 Jerry James <loganjerry@gmail.com> - 0.87.2-1
-- New upstream release
-
-* Wed Jul 13 2016 Jerry James <loganjerry@gmail.com> - 0.87.1-2
-- Rebuild for coq 8.5pl2
-
-* Wed Jun  1 2016 Jerry James <loganjerry@gmail.com> - 0.87.1-1
-- New upstream release
-
-* Fri Apr 22 2016 Jerry James <loganjerry@gmail.com> - 0.87.0-3
-- Rebuild for coq 8.5pl1
-
-* Sat Apr 16 2016 Jerry James <loganjerry@gmail.com> - 0.87.0-2
-- Rebuild for ocaml-ocamlgraph 1.8.7
-
-* Fri Mar 18 2016 Jerry James <loganjerry@gmail.com> - 0.87.0-1
-- New upstream release
-- Drop boomy icon removal; upstream no longer ships them
-
-* Fri Feb 12 2016 Jerry James <loganjerry@gmail.com> - 0.86.3-1
-- New upstream release
-- Use camlp4 in preference to camlp5
-
-* Fri Feb 05 2016 Fedora Release Engineering <releng@fedoraproject.org> - 0.86.2-3
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
-
-* Wed Nov 25 2015 Jerry James <loganjerry@gmail.com> - 0.86.2-2
-- Rebuild for ocaml-zarith 1.4.1 and ocaml-menhir 20151112
-
-* Wed Oct 14 2015 Jerry James <loganjerry@gmail.com> - 0.86.2-1
-- New upstream release
-- Do not ship the nonfree boomy icons
-
-* Wed Jun 24 2015 Richard W.M. Jones <rjones@redhat.com> - 0.86.1-2
-- ocaml-4.02.2 final rebuild.
-
-* Mon Jun 22 2015 Jerry James <loganjerry@gmail.com> - 0.86.1-1
-- New upstream release
-
-* Wed Jun 17 2015 Richard W.M. Jones <rjones@redhat.com> - 0.86-2
-- ocaml-4.02.2 rebuild.
-
-* Sat May 16 2015 Jerry James <loganjerry@gmail.com> - 0.86-1
-- New upstream release
-
-* Sat Apr 11 2015 Jerry James <loganjerry@gmail.com> - 0.85-9
-- Rebuild for coq 8.4pl6
-
-* Wed Mar 18 2015 Jerry James <loganjerry@gmail.com> - 0.85-8
-- Rebuild for ocaml-ocamlgraph 1.8.6
-
-* Sat Feb 21 2015 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 0.85-6
-- ocaml-4.02.1 rebuild.
-
-* Thu Nov  6 2014 Jerry James <loganjerry@gmail.com> - 0.85-5
-- Rebuild for ocaml-camlp5 6.12
-
-* Thu Oct 30 2014 Jerry James <loganjerry@gmail.com> - 0.85-4
-- Rebuild for coq 8.4pl5
-
-* Tue Oct 14 2014 Jerry James <loganjerry@gmail.com> - 0.85-3
-- Rebuild for ocaml-zarith 1.3
-
-* Thu Sep 18 2014 Jerry James <loganjerry@gmail.com> - 0.85-2
-- Bump and rebuild
-
-* Wed Sep 17 2014 Jerry James <loganjerry@gmail.com> - 0.85-1
-- New upstream release
-- New source URL
-
-* Tue Sep  2 2014 Jerry James <loganjerry@gmail.com> - 0.84-1
-- New upstream release
-- Fix license handling
-
-* Mon Aug 25 2014 Jerry James <loganjerry@gmail.com> - 0.83-14
-- Rebuild for new gappalib-coq build
-
-* Sun Aug 24 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-13
-- ocaml-4.02.0+rc1 rebuild.
-
-* Mon Aug 18 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.83-12
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
-
-* Mon Aug  4 2014 Jerry James <loganjerry@gmail.com> - 0.83-11
-- Rebuild for new gappalib-coq build
-
-* Sat Aug 02 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-10
-- ocaml-4.02.0-0.8.git10e45753.fc22 rebuild.
-
-* Fri Aug 01 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-9
-- OCaml 4.02.0 beta rebuild.
-
-* Thu Jun 26 2014 Jerry James <loganjerry@gmail.com> - 0.83-8
-- Linking with -z relro -z now breaks plugins; omit "-z now"
-
-* Sun Jun 08 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.83-7
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
-
-* Tue May 13 2014 Jerry James <loganjerry@gmail.com> - 0.83-6
-- Rebuild for coq 8.4pl4
-
-* Mon Apr 21 2014 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 0.83-4
-- Remove ocaml_arches macro (RHBZ#1087794).
-
-* Mon Mar 24 2014 Jerry James <loganjerry@gmail.com> - 0.83-3
-- Apply upstream fix for building with ocaml-zarith
-- Fix file encodings
-- Fix permission bits
-
-* Tue Mar 18 2014 Jerry James <loganjerry@gmail.com> - 0.83-2
-- Back out the post-release fix to the Coq printer, which breaks Frama-C
-
-* Fri Mar 14 2014 Jerry James <loganjerry@gmail.com> - 0.83-1
-- New upstream release
-- Use cvc4 instead of cvc3
-
-* Wed Feb 26 2014 Jerry James <loganjerry@gmail.com> - 0.82-2
-- Rebuild for ocamlgraph 1.8.4
-- BR ocaml-findlib instead of ocaml-findlib-devel
-
-* Fri Dec 13 2013 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 0.81-6
-- Apply upstream fix for change in the alt-ergo timelimit option
-
-* Tue Sep 17 2013 Jerry James <loganjerry@gmail.com> - 0.81-5
-- Rebuild for OCaml 4.01.0
-- Enable debuginfo for the ocaml sources
-
-* Sun Aug 04 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.81-4
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild
-
-* Fri Jun 21 2013 Jerry James <loganjerry@gmail.com> - 0.81-3
-- Rebuild for frama-c Fluorine 20130601
-
-* Thu May 23 2013 Jerry James <loganjerry@gmail.com> - 0.81-2
-- Rebuild for frama-c Fluorine 20130501
-
-* Fri May 10 2013 Jerry James <loganjerry@gmail.com> - 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 <rel-eng@lists.fedoraproject.org> - 0.73-5
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild
-
-* Mon Jan  7 2013 Jerry James <loganjerry@gmail.com> - 0.73-4
-- Rebuild for coq 8.4pl1
-
-* Fri Dec 14 2012 Richard W.M. Jones <rjones@redhat.com> - 0.73-3
-- Rebuild for OCaml 4.00.1.
-
-* Thu Aug 23 2012 Jerry James <loganjerry@gmail.com> - 0.73-2
-- Rebuild for coq 8.4
-
-* Thu Aug  2 2012 Jerry James <loganjerry@gmail.com> - 0.73-1
-- New upstream release
-
-* Sun Jul 22 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.71-3
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
-
-* Thu Apr 19 2012 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 0.71-1
-- Initial RPM
+%autochangelog