diff --git a/README.md b/README.md deleted file mode 100644 index bad69ce..0000000 --- a/README.md +++ /dev/null @@ -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. diff --git a/changelog b/changelog deleted file mode 100644 index 0856a59..0000000 --- a/changelog +++ /dev/null @@ -1,534 +0,0 @@ -* Mon Oct 14 2024 Jerry James - 1.7.2-10 -- Fix the location of the icon - -* Sun Oct 6 2024 Jerry James - 1.7.2-9 -- Rebuild for ocaml-re 1.13.3 - -* Mon Aug 5 2024 Jerry James - 1.7.2-8 -- Rebuild for ocaml-menhir 20240715, ocaml-ppxlib 0.33.0, and ocaml-zip 1.1.2 - -* Sat Jul 20 2024 Fedora Release Engineering - 1.7.2-7 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild - -* Tue Jul 16 2024 Jerry James - 1.7.2-6 -- Rebuild for ocaml-zarith 1.14 - -* Wed Jul 3 2024 Jerry James - 1.7.2-5 -- Rebuild for ocaml-ppx-sexp-conv 0.17.0 - -* Wed Jun 19 2024 Richard W.M. Jones - 1.7.2-4 -- OCaml 5.2.0 ppc64le fix - -* Thu Jun 13 2024 Jerry James - 1.7.2-3 -- Rebuild for apron 0.9.15 -- New upstream URL - -* Thu May 30 2024 Richard W.M. Jones - 1.7.2-2 -- OCaml 5.2.0 for Fedora 41 - -* Thu Apr 18 2024 Jerry James - 1.7.2-1 -- Version 1.7.2 - -* Mon Mar 25 2024 Richard W.M. Jones - 1.7.1-3 -- Use %%{bash_completions_dir} macro - -* Fri Feb 2 2024 Jerry James - 1.7.1-2 -- Build again because koji ran out of disk space - -* Fri Feb 2 2024 Jerry James - 1.7.1-1 -- Version 1.7.1 - -* Sat Jan 27 2024 Fedora Release Engineering - 1.7.0-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild - -* Tue Jan 2 2024 Jerry James - 1.7.0-1 -- Version 1.7.0 -- Drop upstreamed coq patch - -* Mon Dec 18 2023 Richard W.M. Jones - 1.6.0-9 -- OCaml 5.1.1 + s390x code gen fix for Fedora 40 - -* Tue Dec 12 2023 Richard W.M. Jones - 1.6.0-8 -- OCaml 5.1.1 rebuild for Fedora 40 - -* Thu Oct 05 2023 Richard W.M. Jones - 1.6.0-7 -- OCaml 5.1 rebuild for Fedora 40 - -* Sat Sep 9 2023 Jerry James - 1.6.0-6 -- Rebuild for ocaml-ocamlgraph 2.1.0 - -* Sat Jul 29 2023 Jerry James - 1.6.0-5 -- Require cvc5 instead of cvc4 - -* Thu Jul 27 2023 Jerry James - 1.6.0-4 -- Rebuild for ocaml-zarith 1.13 - -* Sat Jul 22 2023 Fedora Release Engineering - 1.6.0-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild - -* Tue Jul 18 2023 Jerry James - 1.6.0-2 -- Validate metadata with appstream-util - -* Thu Jul 13 2023 Jerry James - 1.6.0-2 -- Rebuild for mpfr 4.2.0 - -* Mon Jul 10 2023 Jerry James - 1.6.0-1 -- Version 1.6.0 -- Enable inference with BDDs -- Add patch for coq 8.17 support - -* Sat Apr 1 2023 Jerry James - 1.5.1-7 -- Rebuild for coq 8.17.0 - -* Tue Jan 24 2023 Richard W.M. Jones - 1.5.1-6 -- Rebuild OCaml packages for F38 - -* Sat Jan 21 2023 Fedora Release Engineering - 1.5.1-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild - -* Fri Jan 6 2023 Jerry James - 1.5.1-4 -- BR tex(tgtermes.sty) to fix FTBFS with TeXLive 2022 - -* Sat Nov 26 2022 Jerry James - 1.5.1-3 -- Rebuild for coq 8.16.1 - -* Tue Nov 1 2022 Jerry James - 1.5.1-2 -- Rebuild for ocaml-ppxlib 0.28.0 - -* Fri Sep 16 2022 Jerry James - 1.5.1-1 -- Version 1.5.1 - -* Thu Aug 18 2022 Jerry James - 1.5.0-3 -- Rebuild to fix coq dependency -- Convert License tag to SPDX - -* Sat Jul 23 2022 Fedora Release Engineering - 1.5.0-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild - -* Tue Jul 19 2022 Jerry James - 1.5.0-1 -- Remove i686 support - -* Thu Jul 7 2022 Jerry James - 1.5.0-1 -- Version 1.5.0 -- Add ocaml-mlmpfr support -- Drop unmaintained man pages -- Use new OCaml macros - -* Sun Jun 19 2022 Richard W.M. Jones - 1.4.1-3 -- OCaml 4.14.0 rebuild - -* Fri Mar 25 2022 Jerry James - 1.4.1-2 -- Rebuild for coq 8.15.1 - -* Mon Feb 28 2022 Jerry James - 1.4.1-1 -- Version 1.4.1 - -* Fri Feb 04 2022 Richard W.M. Jones - 1.4.0-11 -- OCaml 4.13.1 rebuild to remove package notes - -* Sat Jan 22 2022 Fedora Release Engineering - 1.4.0-10 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild - -* Mon Jan 17 2022 Jerry James - 1.4.0-9 -- Rebuild for menhir 20211230 - -* Mon Dec 27 2021 Jerry James - 1.4.0-8 -- Rebuild for alt-ergo 2.3.0 and ocaml-zip 1.11 - -* Tue Nov 30 2021 Jerry James - 1.4.0-7 -- Rebuild for coq 8.14.1, sexplib0 0.15.0 and menhir 20211128 - -* Thu Oct 21 2021 Jerry James - 1.4.0-6 -- Rebuild for coq 8.14.0 and menhir 20211012 -- Add -coq8.14 patch -- Drop XEmacs support - -* Tue Oct 05 2021 Richard W.M. Jones - 1.4.0-5 -- OCaml 4.13.1 build - -* Mon Oct 04 2021 Richard W.M. Jones - 1.4.0-4 -- Try to build on s390x with OCaml 4.13 - -* Fri Jul 30 2021 Jerry James - 1.4.0-3 -- Rebuild for rebuilt coq - -* Fri Jul 23 2021 Fedora Release Engineering - 1.4.0-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild - -* Wed Jul 14 2021 Jerry James - 1.4.0-1 -- Version 1.4.0 -- Drop all patches -- Validate with appstreamcli instead of appstream-util - -* Tue Jun 8 2021 Jerry James - 1.3.3-9 -- Rebuild for ocaml-menhir 20210419 - -* Wed Mar 3 2021 Jerry James - 1.3.3-8 -- Rebuild for coq 8.13.1 and ocaml-zarith 1.12 - -* Tue Mar 2 11:18:12 GMT 2021 Richard W.M. Jones - 1.3.3-7 -- OCaml 4.12.0 build - -* Sat Feb 20 2021 Jerry James - 1.3.3-6 -- Rebuild for coq 8.13.0 -- Update metainfo and install in metainfodir - -* Wed Jan 27 2021 Fedora Release Engineering - 1.3.3-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild - -* Sat Jan 2 2021 Jerry James - 1.3.3-4 -- Rebuild for flocq 3.4.0 - -* Wed Dec 23 2020 Jerry James - 1.3.3-3 -- Rebuild for coq 8.12.2 - -* Wed Dec 2 2020 Jerry James - 1.3.3-2 -- Rebuild for coq 8.12.1 and menhir 20201201 - -* Fri Sep 25 2020 Jerry James - 1.3.3-1 -- Version 1.3.3 - -* Wed Sep 02 2020 Richard W.M. Jones - 1.3.1-14 -- OCaml 4.11.1 rebuild - -* Tue Sep 1 2020 Jerry James - 1.3.1-13 -- Rebuild for coq 8.12.0 - -* Mon Aug 24 2020 Richard W.M. Jones - 1.3.1-13 -- OCaml 4.11.0 rebuild - -* Thu Aug 6 2020 Jerry James - 1.3.1-12 -- Rebuild for ocaml-lablgtk3 3.1.1 and ocaml-menhir 20200624 - -* Wed Jul 29 2020 Fedora Release Engineering - 1.3.1-11 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild - -* Mon Jun 15 2020 Jerry James - 1.3.1-10 -- Rebuild for coq 8.11.2 - -* Sat Jun 13 2020 Jerry James - 1.3.1-9 -- Rebuild for flocq 3.3.1 -- Build the coq files with the native compiler when possible - -* Wed May 20 2020 Jerry James - 1.3.1-8 -- Rebuild for coq 8.11.1 - -* Tue May 05 2020 Richard W.M. Jones - 1.3.1-7 -- OCaml 4.11.0+dev2-2020-04-22 rebuild - -* Sun Apr 12 2020 Jerry James - 1.3.1-6 -- Make the dependencies on ocaml-num and ocaml-zip explicit (bz 1795083) - -* Wed Apr 8 2020 Jerry James - 1.3.1-5 -- Rebuild for flocq 3.2.1 - -* Sun Apr 05 2020 Richard W.M. Jones - 1.3.1-4 -- Update all OCaml dependencies for RPM 4.16. - -* Wed Apr 1 2020 Jerry James - 1.3.1-3 -- Do not build with mlmpfr; symbols clash with mlgmpidl, causing frama-c to - fail to start -- Obsolete the why2 packages - -* Sat Mar 28 2020 Jerry James - 1.3.1-2 -- Remove useless BRs and Rs (bz 1817878) - -* Wed Mar 25 2020 Jerry James - 1.3.1-1 -- Version 1.3.1 - -* Fri Jan 31 2020 Fedora Release Engineering - 1.2.1-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild - -* Wed Jan 22 2020 Jerry James - 1.2.1-3 -- OCaml 4.10.0+beta1 rebuild. - -* Fri Dec 06 2019 Richard W.M. Jones - 1.2.1-2 -- OCaml 4.09.0 (final) rebuild. - -* Tue Oct 29 2019 Jerry James - 1.2.1-1 -- New upstream release -- Add -proofgeneral subpackage -- Add desktop and AppData files - -* Fri Oct 11 2019 Jerry James - 1.2.0-6 -- Rebuild for ocaml-menhir 20190924 - -* Fri Sep 6 2019 Jerry James - 1.2.0-5 -- Rebuild for ocaml-zarith 1.9 - -* Thu Aug 1 2019 Jerry James - 1.2.0-4 -- Also install the library, for consumption by frama-c - -* Thu Aug 1 2019 Jerry James - 1.2.0-3 -- Rebuild for flocq 3.2.0 - -* Sat Jul 27 2019 Fedora Release Engineering - 1.2.0-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild - -* Wed Jun 5 2019 Jerry James - 1.2.0-1 -- New upstream release - -* Sun Feb 03 2019 Fedora Release Engineering - 1.1.1-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild - -* Sat Jan 26 2019 Jerry James - 1.1.1-1 -- New upstream release - -* Sat Jul 14 2018 Fedora Release Engineering - 0.88.3-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild - -* Thu Jul 12 2018 Richard W.M. Jones - 0.88.3-4 -- OCaml 4.07.0 (final) rebuild. - -* Wed Jun 20 2018 Richard W.M. Jones - 0.88.3-3 -- Bump release and rebuild. - -* Wed Jun 20 2018 Richard W.M. Jones - 0.88.3-2 -- OCaml 4.07.0-rc1 rebuild. - -* Mon Feb 12 2018 Jerry James - 0.88.3-1 -- New upstream release - -* Fri Feb 09 2018 Fedora Release Engineering - 0.88.2-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild - -* Sat Dec 9 2017 Jerry James - 0.88.2-1 -- New upstream release - -* Fri Nov 17 2017 Richard W.M. Jones - 0.88.1-1 -- New upstream version 0.88.1. -- OCaml 4.06.0 rebuild. - -* Sat Oct 7 2017 Jerry James - 0.88.0-1 -- New usptream release - -* Thu Oct 5 2017 Jerry James - 0.87.3-12 -- Rebuild for flocq 2.6.0 - -* Wed Sep 06 2017 Richard W.M. Jones - 0.87.3-11 -- OCaml 4.05.0 rebuild. - -* Thu Aug 03 2017 Fedora Release Engineering - 0.87.3-10 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild - -* Thu Jul 27 2017 Fedora Release Engineering - 0.87.3-9 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild - -* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-8 -- Bump release and rebuild. - -* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-7 -- Bump release and rebuild. - -* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-6 -- Bump release and rebuild. - -* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-5 -- OCaml 4.04.2 rebuild. - -* Fri May 12 2017 Richard W.M. Jones - 0.87.3-4 -- OCaml 4.04.1 rebuild. - -* Fri Mar 24 2017 Jerry James - 0.87.3-3 -- Rebuild to fix coq consistency issue - -* Sat Feb 11 2017 Fedora Release Engineering - 0.87.3-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild - -* Thu Jan 12 2017 Jerry James - 0.87.3-1 -- New upstream release - -* Mon Nov 07 2016 Richard W.M. Jones - 0.87.2-4 -- Rebuild for OCaml 4.04.0. - -* Fri Oct 28 2016 Jerry James - 0.87.2-3 -- Rebuild for coq 8.5pl3 -- Remove obsolete scriptlets -- Fix install location of why3lang.sty - -* Thu Sep 29 2016 Jerry James - 0.87.2-2 -- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1 - -* Fri Sep 2 2016 Jerry James - 0.87.2-1 -- New upstream release - -* Wed Jul 13 2016 Jerry James - 0.87.1-2 -- Rebuild for coq 8.5pl2 - -* Wed Jun 1 2016 Jerry James - 0.87.1-1 -- New upstream release - -* Fri Apr 22 2016 Jerry James - 0.87.0-3 -- Rebuild for coq 8.5pl1 - -* Sat Apr 16 2016 Jerry James - 0.87.0-2 -- Rebuild for ocaml-ocamlgraph 1.8.7 - -* Fri Mar 18 2016 Jerry James - 0.87.0-1 -- New upstream release -- Drop boomy icon removal; upstream no longer ships them - -* Fri Feb 12 2016 Jerry James - 0.86.3-1 -- New upstream release -- Use camlp4 in preference to camlp5 - -* Fri Feb 05 2016 Fedora Release Engineering - 0.86.2-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild - -* Wed Nov 25 2015 Jerry James - 0.86.2-2 -- Rebuild for ocaml-zarith 1.4.1 and ocaml-menhir 20151112 - -* Wed Oct 14 2015 Jerry James - 0.86.2-1 -- New upstream release -- Do not ship the nonfree boomy icons - -* Wed Jun 24 2015 Richard W.M. Jones - 0.86.1-2 -- ocaml-4.02.2 final rebuild. - -* Mon Jun 22 2015 Jerry James - 0.86.1-1 -- New upstream release - -* Wed Jun 17 2015 Richard W.M. Jones - 0.86-2 -- ocaml-4.02.2 rebuild. - -* Sat May 16 2015 Jerry James - 0.86-1 -- New upstream release - -* Sat Apr 11 2015 Jerry James - 0.85-9 -- Rebuild for coq 8.4pl6 - -* Wed Mar 18 2015 Jerry James - 0.85-8 -- Rebuild for ocaml-ocamlgraph 1.8.6 - -* Sat Feb 21 2015 Jerry James - 0.85-7 -- Note bundled jquery -- Fix sed expression separators for new RPM_OPT_FLAGS and RPM_LD_FLAGS - -* Wed Feb 18 2015 Richard W.M. Jones - 0.85-6 -- ocaml-4.02.1 rebuild. - -* Thu Nov 6 2014 Jerry James - 0.85-5 -- Rebuild for ocaml-camlp5 6.12 - -* Thu Oct 30 2014 Jerry James - 0.85-4 -- Rebuild for coq 8.4pl5 - -* Tue Oct 14 2014 Jerry James - 0.85-3 -- Rebuild for ocaml-zarith 1.3 - -* Thu Sep 18 2014 Jerry James - 0.85-2 -- Bump and rebuild - -* Wed Sep 17 2014 Jerry James - 0.85-1 -- New upstream release -- New source URL - -* Tue Sep 2 2014 Jerry James - 0.84-1 -- New upstream release -- Fix license handling - -* Mon Aug 25 2014 Jerry James - 0.83-14 -- Rebuild for new gappalib-coq build - -* Sun Aug 24 2014 Richard W.M. Jones - 0.83-13 -- ocaml-4.02.0+rc1 rebuild. - -* Mon Aug 18 2014 Fedora Release Engineering - 0.83-12 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild - -* Mon Aug 4 2014 Jerry James - 0.83-11 -- Rebuild for new gappalib-coq build - -* Sat Aug 02 2014 Richard W.M. Jones - 0.83-10 -- ocaml-4.02.0-0.8.git10e45753.fc22 rebuild. - -* Fri Aug 01 2014 Richard W.M. Jones - 0.83-9 -- OCaml 4.02.0 beta rebuild. - -* Thu Jun 26 2014 Jerry James - 0.83-8 -- Linking with -z relro -z now breaks plugins; omit "-z now" - -* Sun Jun 08 2014 Fedora Release Engineering - 0.83-7 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild - -* Tue May 13 2014 Jerry James - 0.83-6 -- Rebuild for coq 8.4pl4 - -* Mon Apr 21 2014 Jerry James - 0.83-5 -- Rebuild for flocq 2.3.0 and ocamlgraph 1.8.5 -- Drop unnecessary sqlite-devel BR - -* Tue Apr 15 2014 Richard W.M. Jones - 0.83-4 -- Remove ocaml_arches macro (RHBZ#1087794). - -* Mon Mar 24 2014 Jerry James - 0.83-3 -- Apply upstream fix for building with ocaml-zarith -- Fix file encodings -- Fix permission bits - -* Tue Mar 18 2014 Jerry James - 0.83-2 -- Back out the post-release fix to the Coq printer, which breaks Frama-C - -* Fri Mar 14 2014 Jerry James - 0.83-1 -- New upstream release -- Use cvc4 instead of cvc3 - -* Wed Feb 26 2014 Jerry James - 0.82-2 -- Rebuild for ocamlgraph 1.8.4 -- BR ocaml-findlib instead of ocaml-findlib-devel - -* Fri Dec 13 2013 Jerry James - 0.82-1 -- New upstream release -- Drop upstreamed patches -- Add -examples subpackage -- Install LaTeX style -- Turn off frama-c support at upstream's request - -* Mon Sep 30 2013 Jerry James - 0.81-6 -- Apply upstream fix for change in the alt-ergo timelimit option - -* Tue Sep 17 2013 Jerry James - 0.81-5 -- Rebuild for OCaml 4.01.0 -- Enable debuginfo for the ocaml sources - -* Sun Aug 04 2013 Fedora Release Engineering - 0.81-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild - -* Fri Jun 21 2013 Jerry James - 0.81-3 -- Rebuild for frama-c Fluorine 20130601 - -* Thu May 23 2013 Jerry James - 0.81-2 -- Rebuild for frama-c Fluorine 20130501 - -* Fri May 10 2013 Jerry James - 0.81-1 -- New upstream release -- Disable PVS support for now; it requires the NASA libraries -- Fix the conflict between the why and why3 Emacs packages (bz 913522) -- Disable parallel builds due to intermittent build failures - -* Fri Feb 15 2013 Fedora Release Engineering - 0.73-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild - -* Mon Jan 7 2013 Jerry James - 0.73-4 -- Rebuild for coq 8.4pl1 - -* Fri Dec 14 2012 Richard W.M. Jones - 0.73-3 -- Rebuild for OCaml 4.00.1. - -* Thu Aug 23 2012 Jerry James - 0.73-2 -- Rebuild for coq 8.4 - -* Thu Aug 2 2012 Jerry James - 0.73-1 -- New upstream release - -* Sun Jul 22 2012 Fedora Release Engineering - 0.71-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild - -* Thu Apr 19 2012 Jerry James - 0.71-2 -- Add missing sqlite-devel BR -- Do not move the coq plugin -- Generate debuginfo for the sole C program -- Add man pages - -* Fri Dec 16 2011 Jerry James - 0.71-1 -- Initial RPM diff --git a/fr.lri.why3.metainfo.xml b/fr.lri.why3.metainfo.xml index 5ec6c75..0c44545 100644 --- a/fr.lri.why3.metainfo.xml +++ b/fr.lri.why3.metainfo.xml @@ -38,10 +38,10 @@ File reloaded after modifying goal G2 - why3-maintainers@fedoraproject.org + loganjerry@gmail.com http://why3.lri.fr/ https://gitlab.inria.fr/why3/why3/issues - + why3 diff --git a/sources b/sources index f503a9e..8b12354 100644 --- a/sources +++ b/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 diff --git a/why3-rocq-9.2.patch b/why3-rocq-9.2.patch deleted file mode 100644 index 9b2042c..0000000 --- a/why3-rocq-9.2.patch +++ /dev/null @@ -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 *) diff --git a/why3-zmod.patch b/why3-zmod.patch deleted file mode 100644 index 48f3ae4..0000000 --- a/why3-zmod.patch +++ /dev/null @@ -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. diff --git a/why3.rpmlintrc b/why3.rpmlintrc new file mode 100644 index 0000000..7b0f672 --- /dev/null +++ b/why3.rpmlintrc @@ -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') diff --git a/why3.spec b/why3.spec index 3fc4249..3928724 100644 --- a/why3.spec +++ b/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: 1%{?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,377 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog -%autochangelog +* Wed Jul 14 2021 Jerry James - 1.4.0-1 +- Version 1.4.0 +- Drop all patches +- Validate with appstreamcli instead of appstream-util + +* Tue Jun 8 2021 Jerry James - 1.3.3-8 +- Rebuild for ocaml-menhir 20210419 + +* Wed Mar 3 2021 Jerry James - 1.3.3-7 +- Rebuild for coq 8.13.1 and ocaml-zarith 1.12 + +* Sat Feb 20 2021 Jerry James - 1.3.3-6 +- Rebuild for coq 8.13.0 +- Update metainfo and install in metainfodir + +* Wed Jan 27 2021 Fedora Release Engineering - 1.3.3-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild + +* Sat Jan 2 2021 Jerry James - 1.3.3-4 +- Rebuild for flocq 3.4.0 + +* Wed Dec 23 2020 Jerry James - 1.3.3-3 +- Rebuild for coq 8.12.2 + +* Wed Dec 2 2020 Jerry James - 1.3.3-2 +- Rebuild for coq 8.12.1 and menhir 20201201 + +* Fri Sep 25 2020 Jerry James - 1.3.3-1 +- Version 1.3.3 + +* Wed Sep 02 2020 Richard W.M. Jones - 1.3.1-14 +- OCaml 4.11.1 rebuild + +* Tue Sep 1 2020 Jerry James - 1.3.1-13 +- Rebuild for coq 8.12.0 + +* Mon Aug 24 2020 Richard W.M. Jones - 1.3.1-13 +- OCaml 4.11.0 rebuild + +* Thu Aug 6 2020 Jerry James - 1.3.1-12 +- Rebuild for ocaml-lablgtk3 3.1.1 and ocaml-menhir 20200624 + +* Wed Jul 29 2020 Fedora Release Engineering - 1.3.1-11 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild + +* Mon Jun 15 2020 Jerry James - 1.3.1-10 +- Rebuild for coq 8.11.2 + +* Sat Jun 13 2020 Jerry James - 1.3.1-9 +- Rebuild for flocq 3.3.1 +- Build the coq files with the native compiler when possible + +* Wed May 20 2020 Jerry James - 1.3.1-8 +- Rebuild for coq 8.11.1 + +* Tue May 05 2020 Richard W.M. Jones - 1.3.1-7 +- OCaml 4.11.0+dev2-2020-04-22 rebuild + +* Sun Apr 12 2020 Jerry James - 1.3.1-6 +- Make the dependencies on ocaml-num and ocaml-zip explicit (bz 1795083) + +* Wed Apr 8 2020 Jerry James - 1.3.1-5 +- Rebuild for flocq 3.2.1 + +* Sun Apr 05 2020 Richard W.M. Jones - 1.3.1-4 +- Update all OCaml dependencies for RPM 4.16. + +* Wed Apr 1 2020 Jerry James - 1.3.1-3 +- Do not build with mlmpfr; symbols clash with mlgmpidl, causing frama-c to + fail to start +- Obsolete the why2 packages + +* Sat Mar 28 2020 Jerry James - 1.3.1-2 +- Remove useless BRs and Rs (bz 1817878) + +* Wed Mar 25 2020 Jerry James - 1.3.1-1 +- Version 1.3.1 + +* Fri Jan 31 2020 Fedora Release Engineering - 1.2.1-4 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild + +* Wed Jan 22 2020 Jerry James - 1.2.1-3 +- OCaml 4.10.0+beta1 rebuild. + +* Fri Dec 06 2019 Richard W.M. Jones - 1.2.1-2 +- OCaml 4.09.0 (final) rebuild. + +* Tue Oct 29 2019 Jerry James - 1.2.1-1 +- New upstream release +- Add -proofgeneral subpackage +- Add desktop and AppData files + +* Fri Oct 11 2019 Jerry James - 1.2.0-6 +- Rebuild for ocaml-menhir 20190924 + +* Fri Sep 6 2019 Jerry James - 1.2.0-5 +- Rebuild for ocaml-zarith 1.9 + +* Thu Aug 1 2019 Jerry James - 1.2.0-4 +- Also install the library, for consumption by frama-c + +* Thu Aug 1 2019 Jerry James - 1.2.0-3 +- Rebuild for flocq 3.2.0 + +* Sat Jul 27 2019 Fedora Release Engineering - 1.2.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild + +* Wed Jun 5 2019 Jerry James - 1.2.0-1 +- New upstream release + +* Sun Feb 03 2019 Fedora Release Engineering - 1.1.1-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild + +* Sat Jan 26 2019 Jerry James - 1.1.1-1 +- New upstream release + +* Sat Jul 14 2018 Fedora Release Engineering - 0.88.3-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild + +* Thu Jul 12 2018 Richard W.M. Jones - 0.88.3-4 +- OCaml 4.07.0 (final) rebuild. + +* Wed Jun 20 2018 Richard W.M. Jones - 0.88.3-3 +- Bump release and rebuild. + +* Wed Jun 20 2018 Richard W.M. Jones - 0.88.3-2 +- OCaml 4.07.0-rc1 rebuild. + +* Mon Feb 12 2018 Jerry James - 0.88.3-1 +- New upstream release + +* Fri Feb 09 2018 Fedora Release Engineering - 0.88.2-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild + +* Sat Dec 9 2017 Jerry James - 0.88.2-1 +- New upstream release + +* Fri Nov 17 2017 Richard W.M. Jones - 0.88.1-1 +- New upstream version 0.88.1. +- OCaml 4.06.0 rebuild. + +* Sat Oct 7 2017 Jerry James - 0.88.0-1 +- New usptream release + +* Thu Oct 5 2017 Jerry James - 0.87.3-12 +- Rebuild for flocq 2.6.0 + +* Wed Sep 06 2017 Richard W.M. Jones - 0.87.3-11 +- OCaml 4.05.0 rebuild. + +* Thu Aug 03 2017 Fedora Release Engineering - 0.87.3-10 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild + +* Thu Jul 27 2017 Fedora Release Engineering - 0.87.3-9 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild + +* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-8 +- Bump release and rebuild. + +* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-7 +- Bump release and rebuild. + +* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-6 +- Bump release and rebuild. + +* Tue Jun 27 2017 Richard W.M. Jones - 0.87.3-5 +- OCaml 4.04.2 rebuild. + +* Fri May 12 2017 Richard W.M. Jones - 0.87.3-4 +- OCaml 4.04.1 rebuild. + +* Fri Mar 24 2017 Jerry James - 0.87.3-3 +- Rebuild to fix coq consistency issue + +* Sat Feb 11 2017 Fedora Release Engineering - 0.87.3-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild + +* Thu Jan 12 2017 Jerry James - 0.87.3-1 +- New upstream release + +* Mon Nov 07 2016 Richard W.M. Jones - 0.87.2-4 +- Rebuild for OCaml 4.04.0. + +* Fri Oct 28 2016 Jerry James - 0.87.2-3 +- Rebuild for coq 8.5pl3 +- Remove obsolete scriptlets +- Fix install location of why3lang.sty + +* Thu Sep 29 2016 Jerry James - 0.87.2-2 +- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1 + +* Fri Sep 2 2016 Jerry James - 0.87.2-1 +- New upstream release + +* Wed Jul 13 2016 Jerry James - 0.87.1-2 +- Rebuild for coq 8.5pl2 + +* Wed Jun 1 2016 Jerry James - 0.87.1-1 +- New upstream release + +* Fri Apr 22 2016 Jerry James - 0.87.0-3 +- Rebuild for coq 8.5pl1 + +* Sat Apr 16 2016 Jerry James - 0.87.0-2 +- Rebuild for ocaml-ocamlgraph 1.8.7 + +* Fri Mar 18 2016 Jerry James - 0.87.0-1 +- New upstream release +- Drop boomy icon removal; upstream no longer ships them + +* Fri Feb 12 2016 Jerry James - 0.86.3-1 +- New upstream release +- Use camlp4 in preference to camlp5 + +* Fri Feb 05 2016 Fedora Release Engineering - 0.86.2-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild + +* Wed Nov 25 2015 Jerry James - 0.86.2-2 +- Rebuild for ocaml-zarith 1.4.1 and ocaml-menhir 20151112 + +* Wed Oct 14 2015 Jerry James - 0.86.2-1 +- New upstream release +- Do not ship the nonfree boomy icons + +* Wed Jun 24 2015 Richard W.M. Jones - 0.86.1-2 +- ocaml-4.02.2 final rebuild. + +* Mon Jun 22 2015 Jerry James - 0.86.1-1 +- New upstream release + +* Wed Jun 17 2015 Richard W.M. Jones - 0.86-2 +- ocaml-4.02.2 rebuild. + +* Sat May 16 2015 Jerry James - 0.86-1 +- New upstream release + +* Sat Apr 11 2015 Jerry James - 0.85-9 +- Rebuild for coq 8.4pl6 + +* Wed Mar 18 2015 Jerry James - 0.85-8 +- Rebuild for ocaml-ocamlgraph 1.8.6 + +* Sat Feb 21 2015 Jerry James - 0.85-7 +- Note bundled jquery +- Fix sed expression separators for new RPM_OPT_FLAGS and RPM_LD_FLAGS + +* Wed Feb 18 2015 Richard W.M. Jones - 0.85-6 +- ocaml-4.02.1 rebuild. + +* Thu Nov 6 2014 Jerry James - 0.85-5 +- Rebuild for ocaml-camlp5 6.12 + +* Thu Oct 30 2014 Jerry James - 0.85-4 +- Rebuild for coq 8.4pl5 + +* Tue Oct 14 2014 Jerry James - 0.85-3 +- Rebuild for ocaml-zarith 1.3 + +* Thu Sep 18 2014 Jerry James - 0.85-2 +- Bump and rebuild + +* Wed Sep 17 2014 Jerry James - 0.85-1 +- New upstream release +- New source URL + +* Tue Sep 2 2014 Jerry James - 0.84-1 +- New upstream release +- Fix license handling + +* Mon Aug 25 2014 Jerry James - 0.83-14 +- Rebuild for new gappalib-coq build + +* Sun Aug 24 2014 Richard W.M. Jones - 0.83-13 +- ocaml-4.02.0+rc1 rebuild. + +* Mon Aug 18 2014 Fedora Release Engineering - 0.83-12 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild + +* Mon Aug 4 2014 Jerry James - 0.83-11 +- Rebuild for new gappalib-coq build + +* Sat Aug 02 2014 Richard W.M. Jones - 0.83-10 +- ocaml-4.02.0-0.8.git10e45753.fc22 rebuild. + +* Fri Aug 01 2014 Richard W.M. Jones - 0.83-9 +- OCaml 4.02.0 beta rebuild. + +* Thu Jun 26 2014 Jerry James - 0.83-8 +- Linking with -z relro -z now breaks plugins; omit "-z now" + +* Sun Jun 08 2014 Fedora Release Engineering - 0.83-7 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild + +* Tue May 13 2014 Jerry James - 0.83-6 +- Rebuild for coq 8.4pl4 + +* Mon Apr 21 2014 Jerry James - 0.83-5 +- Rebuild for flocq 2.3.0 and ocamlgraph 1.8.5 +- Drop unnecessary sqlite-devel BR + +* Tue Apr 15 2014 Richard W.M. Jones - 0.83-4 +- Remove ocaml_arches macro (RHBZ#1087794). + +* Mon Mar 24 2014 Jerry James - 0.83-3 +- Apply upstream fix for building with ocaml-zarith +- Fix file encodings +- Fix permission bits + +* Tue Mar 18 2014 Jerry James - 0.83-2 +- Back out the post-release fix to the Coq printer, which breaks Frama-C + +* Fri Mar 14 2014 Jerry James - 0.83-1 +- New upstream release +- Use cvc4 instead of cvc3 + +* Wed Feb 26 2014 Jerry James - 0.82-2 +- Rebuild for ocamlgraph 1.8.4 +- BR ocaml-findlib instead of ocaml-findlib-devel + +* Fri Dec 13 2013 Jerry James - 0.82-1 +- New upstream release +- Drop upstreamed patches +- Add -examples subpackage +- Install LaTeX style +- Turn off frama-c support at upstream's request + +* Mon Sep 30 2013 Jerry James - 0.81-6 +- Apply upstream fix for change in the alt-ergo timelimit option + +* Tue Sep 17 2013 Jerry James - 0.81-5 +- Rebuild for OCaml 4.01.0 +- Enable debuginfo for the ocaml sources + +* Sun Aug 04 2013 Fedora Release Engineering - 0.81-4 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild + +* Fri Jun 21 2013 Jerry James - 0.81-3 +- Rebuild for frama-c Fluorine 20130601 + +* Thu May 23 2013 Jerry James - 0.81-2 +- Rebuild for frama-c Fluorine 20130501 + +* Fri May 10 2013 Jerry James - 0.81-1 +- New upstream release +- Disable PVS support for now; it requires the NASA libraries +- Fix the conflict between the why and why3 Emacs packages (bz 913522) +- Disable parallel builds due to intermittent build failures + +* Fri Feb 15 2013 Fedora Release Engineering - 0.73-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild + +* Mon Jan 7 2013 Jerry James - 0.73-4 +- Rebuild for coq 8.4pl1 + +* Fri Dec 14 2012 Richard W.M. Jones - 0.73-3 +- Rebuild for OCaml 4.00.1. + +* Thu Aug 23 2012 Jerry James - 0.73-2 +- Rebuild for coq 8.4 + +* Thu Aug 2 2012 Jerry James - 0.73-1 +- New upstream release + +* Sun Jul 22 2012 Fedora Release Engineering - 0.71-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild + +* Thu Apr 19 2012 Jerry James - 0.71-2 +- Add missing sqlite-devel BR +- Do not move the coq plugin +- Generate debuginfo for the sole C program +- Add man pages + +* Fri Dec 16 2011 Jerry James - 0.71-1 +- Initial RPM