Compare commits
1 commit
| Author | SHA1 | Date | |
|---|---|---|---|
|
532167df2c |
8 changed files with 554 additions and 969 deletions
16
README.md
16
README.md
|
|
@ -1,16 +0,0 @@
|
|||
# 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.
|
||||
534
changelog
534
changelog
|
|
@ -1,534 +0,0 @@
|
|||
* 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
|
||||
|
|
@ -38,10 +38,10 @@
|
|||
<caption>File reloaded after modifying goal G2</caption>
|
||||
</screenshot>
|
||||
</screenshots>
|
||||
<update_contact>why3-maintainers@fedoraproject.org</update_contact>
|
||||
<update_contact>loganjerry@gmail.com</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>
|
||||
<content_rating type="oars-1.0"></content_rating>
|
||||
<provides>
|
||||
<binary>why3</binary>
|
||||
</provides>
|
||||
|
|
|
|||
3
sources
3
sources
|
|
@ -1 +1,2 @@
|
|||
SHA512 (why3-1.8.2.tar.gz) = a35e88fafe1aa29c36d2248c1a644eae85afa1bb7b3009193f4a5c28ba684d0882717d63733d8581a7c2cd5ec493e2d15c82baabef615b4d00323fa9309875f8
|
||||
SHA512 (why3-man.tar.xz) = 8355776ac8a67a56ae7354f8fd40dc5d2057022d1035090a3e38e139fbfe3c258fe3ccbed6e333cb005e66c7b4cdbbf6580e3420170fd08384cc9b36ce5ec2a1
|
||||
SHA512 (why3-1.4.0.tar.gz) = b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a
|
||||
|
|
|
|||
|
|
@ -1,292 +0,0 @@
|
|||
--- 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 *)
|
||||
|
|
@ -1,33 +0,0 @@
|
|||
--- 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.
|
||||
28
why3.rpmlintrc
Normal file
28
why3.rpmlintrc
Normal file
|
|
@ -0,0 +1,28 @@
|
|||
# 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')
|
||||
613
why3.spec
613
why3.spec
|
|
@ -3,53 +3,61 @@
|
|||
# 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.8.2
|
||||
Release: %autorelease
|
||||
Version: 1.4.0
|
||||
Release: 4%{?dist}
|
||||
Summary: Software verification platform
|
||||
|
||||
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
|
||||
# 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/38425/%{name}-%{version}.tar.gz
|
||||
# Man pages written by Jerry James using text found in the sources. Hence,
|
||||
# the copyright and license are the same as for the upstream sources.
|
||||
Source1: %{name}-man.tar.xz
|
||||
# Desktop file written by Jerry James
|
||||
Source1: fr.lri.%{name}.desktop
|
||||
Source2: 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
|
||||
# Adapt to changes in rocq 9.2.0
|
||||
Patch: %{name}-rocq-9.2.patch
|
||||
Source3: fr.lri.%{name}.metainfo.xml
|
||||
|
||||
# Coq's plugin architecture requires cmxs files, so:
|
||||
ExclusiveArch: %{ocaml_native_compiler}
|
||||
# https://bugzilla.redhat.com/show_bug.cgi?id=1874879
|
||||
ExcludeArch: s390x
|
||||
|
||||
BuildRequires: coq-core-compat
|
||||
BuildRequires: emacs-nw
|
||||
BuildRequires: appstream
|
||||
BuildRequires: coq
|
||||
BuildRequires: emacs-proofgeneral
|
||||
BuildRequires: flocq
|
||||
BuildRequires: java-devel
|
||||
BuildRequires: latexmk
|
||||
BuildRequires: libappstream-glib
|
||||
BuildRequires: make
|
||||
BuildRequires: ocaml
|
||||
BuildRequires: ocaml-apron-devel
|
||||
BuildRequires: ocaml-camlidl-devel
|
||||
BuildRequires: ocaml-camlp5-devel
|
||||
BuildRequires: ocaml-findlib
|
||||
BuildRequires: ocaml-lablgtk3-sourceview3-devel
|
||||
BuildRequires: ocaml-menhir
|
||||
BuildRequires: ocaml-mlmpfr-devel
|
||||
BuildRequires: ocaml-num-devel
|
||||
BuildRequires: ocaml-ocamlgraph-devel
|
||||
BuildRequires: ocaml-ppx-deriving-devel
|
||||
BuildRequires: ocaml-ppx-sexp-conv-devel
|
||||
BuildRequires: ocaml-ocamldoc
|
||||
BuildRequires: ocaml-re-devel
|
||||
BuildRequires: ocaml-sexplib-devel
|
||||
BuildRequires: ocaml-seq-devel
|
||||
BuildRequires: ocaml-zarith-devel
|
||||
BuildRequires: ocaml-zip-devel
|
||||
BuildRequires: rocq
|
||||
BuildRequires: texlive-latex
|
||||
BuildRequires: vim-filesystem
|
||||
BuildRequires: %{py3_dist sphinx}
|
||||
BuildRequires: %{py3_dist sphinxcontrib-bibtex}
|
||||
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(upquote.sty)
|
||||
BuildRequires: tex(wrapfig.sty)
|
||||
BuildRequires: tex-urlbst
|
||||
BuildRequires: emacs xemacs xemacs-packages-extra
|
||||
BuildRequires: graphviz
|
||||
|
||||
Requires: gtksourceview3%{?_isa}
|
||||
Requires: hicolor-icon-theme
|
||||
|
|
@ -59,18 +67,26 @@ Requires: vim-filesystem
|
|||
Recommends: bash-completion
|
||||
Recommends: flocq
|
||||
|
||||
Provides: bundled(js-jquery)
|
||||
Provides: bundled(jquery)
|
||||
|
||||
# The corresponding Provides is not generated, so filter this out
|
||||
%global __requires_exclude ocaml\\\(Driver_ast\\\)
|
||||
%global __requires_exclude ocaml\\\(Why3\\\)
|
||||
|
||||
# This can be removed when F36 reaches EOL
|
||||
Obsoletes: why < 2.41-12
|
||||
Provides: why = 2.41-12%{?dist}
|
||||
Obsoletes: why-jessie < 2.41-12
|
||||
Provides: why-jessie = 2.41-12%{?dist}
|
||||
Obsoletes: why-pvs-support < 2.41-12
|
||||
Provides: why-pvs-support = 2.41-12%{?dist}
|
||||
|
||||
%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
|
||||
|
|
@ -89,22 +105,36 @@ 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 cvc5 E gappa yices-tools z3 zenon
|
||||
Requires: alt-ergo coq cvc4 E gappa yices-tools z3 zenon
|
||||
|
||||
# This can be removed when F36 reaches EOL
|
||||
Obsoletes: why-all < 2.41-12
|
||||
Provides: why-all = 2.41-12%{?dist}
|
||||
|
||||
%description all
|
||||
This package provides a complete software verification platform suite based on
|
||||
Why3, including various automated and interactive provers.
|
||||
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-num%{?_isa}
|
||||
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
|
||||
|
|
@ -112,12 +142,11 @@ Requires: ocaml-%{name}%{?_isa} = %{version}-%{release}
|
|||
Requires: ocaml-menhir%{?_isa}
|
||||
Requires: ocaml-num-devel%{?_isa}
|
||||
Requires: ocaml-re-devel%{?_isa}
|
||||
Requires: ocaml-sexplib-devel%{?_isa}
|
||||
Requires: ocaml-zip-devel%{?_isa}
|
||||
Requires: ocaml-seq-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
|
||||
|
|
@ -129,9 +158,9 @@ BuildArch: noarch
|
|||
This package provides a why3 plugin for ProofGeneral.
|
||||
|
||||
%prep
|
||||
%autosetup -p1
|
||||
%autosetup -p0
|
||||
%setup -q -T -D -a 1
|
||||
|
||||
%conf
|
||||
fixtimestamp() {
|
||||
touch -r $1.orig $1
|
||||
rm $1.orig
|
||||
|
|
@ -140,22 +169,23 @@ fixtimestamp() {
|
|||
# Use the correct compiler flags, keep timestamps, and harden the build due to
|
||||
# network use. Link the binaries with runtime compiled with -fPIC.
|
||||
# This avoids many link-time errors.
|
||||
sed -e 's|-Wall|%{build_cflags} %{build_ldflags}|;s/ -O -g//' \
|
||||
-e 's/cp /cp -p /' \
|
||||
-e 's|^OLINKFLAGS =.*|& -runtime-variant _pic -ccopt "%{build_ldflags}"|' \
|
||||
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\"|" \
|
||||
-i Makefile.in
|
||||
|
||||
# Remove spurious executable bits
|
||||
find -O3 examples -type f -perm /0111 -exec chmod a-x {} \+
|
||||
chmod a+x examples/*.sh
|
||||
|
||||
# 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 --enable-bddinfer
|
||||
|
||||
# FIXME: Parallel make sometimes fails
|
||||
make
|
||||
# The documentation build is broken in the 1.8.0 release
|
||||
# make doc
|
||||
%configure --enable-verbose-make
|
||||
make #%%{?_smp_mflags}
|
||||
make doc
|
||||
rm -f doc/html/.buildinfo examples/use_api/.merlin.in
|
||||
|
||||
%install
|
||||
|
|
@ -171,17 +201,26 @@ done
|
|||
cd -
|
||||
%endif
|
||||
|
||||
# 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
|
||||
done
|
||||
cd ..
|
||||
|
||||
# Install the bash completion file
|
||||
mkdir -p %{buildroot}%{bash_completions_dir}
|
||||
cp -p share/bash/%{name} %{buildroot}%{bash_completions_dir}
|
||||
mkdir -p %{buildroot}%{_datadir}/bash-completion/completions
|
||||
cp -p share/bash/%{name} %{buildroot}%{_datadir}/bash-completion/completions
|
||||
|
||||
# Install the zsh completion file
|
||||
mkdir -p %{buildroot}%{zsh_completions_dir}
|
||||
cp -p share/zsh/_why3 %{buildroot}%{zsh_completions_dir}
|
||||
mkdir -p %{buildroot}%{_datadir}/zsh/site-functions
|
||||
cp -p share/zsh/_why3 %{buildroot}%{_datadir}/zsh/site-functions
|
||||
|
||||
# Install the LaTeX style
|
||||
mkdir -p %{buildroot}%{_texmf_main}/tex/latex/why3
|
||||
cp -p share/latex/why3lang.sty %{buildroot}%{_texmf_main}/tex/latex/why3
|
||||
mkdir -p %{buildroot}%{_texmf}/tex/latex/why3
|
||||
cp -p share/latex/why3lang.sty %{buildroot}%{_texmf}/tex/latex/why3
|
||||
|
||||
# Move the gtksourceview language file to the right place
|
||||
mkdir -p %{buildroot}%{_datadir}/gtksourceview-3.0
|
||||
|
|
@ -190,30 +229,35 @@ mv %{buildroot}%{_datadir}/%{name}/lang \
|
|||
|
||||
# Install the desktop file
|
||||
mkdir -p %{buildroot}%{_datadir}/applications
|
||||
desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE1}
|
||||
desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE2}
|
||||
|
||||
# Install the icon
|
||||
mkdir -p %{buildroot}%{_datadir}/icons/hicolor/scalable/apps
|
||||
mkdir -p %{buildroot}%{_datadir}/icons/hicolor/scalable
|
||||
cp -p share/images/src/logo-kim.svg \
|
||||
%{buildroot}%{_datadir}/icons/hicolor/scalable/apps/%{name}.svg
|
||||
%{buildroot}%{_datadir}/icons/hicolor/scalable/%{name}.svg
|
||||
|
||||
# Install the AppStream metadata
|
||||
mkdir -p %{buildroot}%{_metainfodir}
|
||||
cp -p %{SOURCE2} %{buildroot}%{_metainfodir}
|
||||
appstream-util validate-relax --nonet \
|
||||
cp -p %{SOURCE3} %{buildroot}%{_metainfodir}
|
||||
appstreamcli validate --no-net \
|
||||
%{buildroot}%{_metainfodir}/fr.lri.%{name}.metainfo.xml
|
||||
|
||||
# Move the vim file to the right place
|
||||
mkdir -p %{buildroot}%{vimfiles_root}
|
||||
mkdir -p %{buildroot}%{_datadir}/vim/vimfiles
|
||||
mv %{buildroot}%{_datadir}/%{name}/vim/ftdetect \
|
||||
%{buildroot}%{_datadir}/%{name}/vim/syntax \
|
||||
%{buildroot}%{vimfiles_root}
|
||||
%{buildroot}%{_datadir}/vim/vimfiles
|
||||
|
||||
# Byte compile the Emacs support files
|
||||
# Byte compile the (X)Emacs support files
|
||||
mkdir -p %{buildroot}%{_xemacs_sitelispdir}
|
||||
cp -p %{buildroot}%{_emacs_sitelispdir}/%{name}.el \
|
||||
%{buildroot}%{_xemacs_sitelispdir}
|
||||
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
|
||||
cd -
|
||||
popd
|
||||
|
||||
# Remove misplaced documentation
|
||||
rm -fr %{buildroot}%{_datadir}/doc
|
||||
|
|
@ -222,45 +266,44 @@ rm -fr %{buildroot}%{_datadir}/doc
|
|||
chmod 0755 %{buildroot}%{_bindir}/* \
|
||||
%{buildroot}%{_libdir}/%{name}/commands/* \
|
||||
%{buildroot}%{_libdir}/%{name}/plugins/*.cmxs \
|
||||
%{buildroot}%{ocamldir}/%{name}/*.cmxs
|
||||
%{buildroot}%{_libdir}/ocaml/%{name}/*.cmxs
|
||||
|
||||
%files
|
||||
%doc AUTHORS CHANGES.md README.md
|
||||
%doc AUTHORS CHANGES.md README.md doc/html doc/latex/manual.pdf
|
||||
%license LICENSE
|
||||
%{_bindir}/%{name}
|
||||
%{_bindir}/isabelle_client
|
||||
%{bash_completions_dir}/why3
|
||||
%{zsh_completions_dir}/_why3
|
||||
%{_datadir}/%{name}/
|
||||
%{_datadir}/applications/fr.lri.%{name}.desktop
|
||||
%{_datadir}/gtksourceview-3.0/language-specs/coma.lang
|
||||
%{_datadir}/bash-completion/completions/why3
|
||||
%{_datadir}/gtksourceview-3.0/language-specs/%{name}.lang
|
||||
%{_datadir}/gtksourceview-3.0/language-specs/%{name}c.lang
|
||||
%{_datadir}/gtksourceview-3.0/language-specs/%{name}py.lang
|
||||
%{_datadir}/icons/hicolor/scalable/apps/%{name}.svg
|
||||
%{vimfiles_root}/ftdetect/%{name}.vim
|
||||
%{vimfiles_root}/syntax/%{name}.vim
|
||||
%{_texmf_main}/tex/latex/why3/
|
||||
%{_datadir}/icons/hicolor/scalable/%{name}.svg
|
||||
%{_datadir}/vim/vimfiles/ftdetect/%{name}.vim
|
||||
%{_datadir}/vim/vimfiles/syntax/%{name}.vim
|
||||
%{_datadir}/zsh/
|
||||
%{_texmf}/tex/latex/why3/
|
||||
%{_libdir}/%{name}/
|
||||
%{_mandir}/man1/%{name}*
|
||||
%{_metainfodir}/fr.lri.%{name}.metainfo.xml
|
||||
|
||||
%files -n ocaml-%{name}
|
||||
%dir %{ocamldir}/%{name}/
|
||||
%{ocamldir}/%{name}/META
|
||||
%{ocamldir}/%{name}/*.cmi
|
||||
%dir %{_libdir}/ocaml/%{name}/
|
||||
%{_libdir}/ocaml/%{name}/META
|
||||
%{_libdir}/ocaml/%{name}/*.cmi
|
||||
%ifarch %{ocaml_native_compiler}
|
||||
%{ocamldir}/%{name}/*.cmxs
|
||||
%{_libdir}/ocaml/%{name}/*.cmxs
|
||||
%endif
|
||||
|
||||
%files -n ocaml-%{name}-devel
|
||||
%ifarch %{ocaml_native_compiler}
|
||||
%{ocamldir}/%{name}/*.a
|
||||
%{ocamldir}/%{name}/*.cmx
|
||||
%{ocamldir}/%{name}/*.cmxa
|
||||
%{_libdir}/ocaml/%{name}/*.a
|
||||
%{_libdir}/ocaml/%{name}/*.cmx
|
||||
%{_libdir}/ocaml/%{name}/*.cmxa
|
||||
%else
|
||||
%{ocamldir}/%{name}/*.cma
|
||||
%{_libdir}/ocaml/%{name}/*.cma
|
||||
%endif
|
||||
%{ocamldir}/%{name}/*.cmt
|
||||
%{_libdir}/ocaml/%{name}/*.cmt
|
||||
|
||||
%files examples
|
||||
%doc examples
|
||||
|
|
@ -268,6 +311,9 @@ 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*
|
||||
|
|
@ -277,4 +323,389 @@ chmod 0755 %{buildroot}%{_bindir}/* \
|
|||
%files all
|
||||
|
||||
%changelog
|
||||
%autochangelog
|
||||
* Mon Oct 17 2022 Jerry James <loganjerry@gmail.com> - 1.4.0-4
|
||||
- Rebuild for coq 8.13.2-4
|
||||
|
||||
* 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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue