From 98f35406b7984e483338b4845ae9b79e0834e0b9 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 2 Jan 2024 19:28:19 -0700 Subject: [PATCH 1/3] Version 1.7.0. Drop upstreamed coq patch. --- sources | 2 +- why3-coq-8.17.patch | 82 --------------------------------------------- why3.spec | 26 ++++---------- 3 files changed, 8 insertions(+), 102 deletions(-) delete mode 100644 why3-coq-8.17.patch diff --git a/sources b/sources index 026cfc6..2c57c42 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (why3-1.6.0.tar.gz) = 60d61b8337ab9f2fd2e6c7174eb0bab063f122417738cd75990c5c53120dd535bcedccb670567f5753853d6bc9f8efebb563d079e4d368372a7687193f1346b1 +SHA512 (why3-1.7.0.tar.gz) = 1fb458e58b75662e3cc4f3cdb42b0e2229d5c73e44a182370ce8beca3a2e18ac8b6c9a403ba94f9391d46cb9bd47cd37cfc9592c77cc2164a7f92124f6f557b6 diff --git a/why3-coq-8.17.patch b/why3-coq-8.17.patch deleted file mode 100644 index 2503ce7..0000000 --- a/why3-coq-8.17.patch +++ /dev/null @@ -1,82 +0,0 @@ ---- why3-1.6.0/configure.in.orig 2023-03-07 02:15:31.000000000 -0700 -+++ why3-1.6.0/configure.in 2023-06-26 14:21:56.361457115 -0600 -@@ -993,6 +993,10 @@ if test "$enable_coq_support" = yes; the - 8.16*) - coq_compat_version="COQ816" - ;; -+ 8.17*) -+ coq_compat_version="COQ817" -+ COQFLAGS="-w deprecated-instance-without-locality,deprecated-hint-without-locality" -+ ;; - *) - enable_coq_support=no - AC_MSG_WARN([You need Coq 8.7 or later; Coq discarded.]) -@@ -1242,6 +1246,7 @@ AC_SUBST(COQC) - AC_SUBST(COQDEP) - AC_SUBST(COQLIB) - AC_SUBST(COQVERSION) -+AC_SUBST(COQFLAGS) - - AC_SUBST(enable_pvs_libs) - AC_SUBST(PVS) ---- why3-1.6.0/configure.orig 2023-03-07 02:15:31.000000000 -0700 -+++ why3-1.6.0/configure 2023-06-26 14:35:07.856280739 -0600 -@@ -696,6 +696,7 @@ PVSVERSION - enable_pvs_libs - COQVERSION - COQLIB -+COQFLAGS - coq_compat_version - enable_coq_fp_libs - enable_coq_libs -@@ -5926,6 +5927,10 @@ printf "%s\n" "$COQVERSION" >&6; } - 8.16*) - coq_compat_version="COQ816" - ;; -+ 8.17*) -+ coq_compat_version="COQ817" -+ COQFLAGS="-w deprecated-instance-without-locality,deprecated-hint-without-locality" -+ ;; - *) - enable_coq_support=no - { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: You need Coq 8.7 or later; Coq discarded." >&5 ---- why3-1.6.0/Makefile.in.orig 2023-03-07 02:15:31.000000000 -0700 -+++ why3-1.6.0/Makefile.in 2023-06-26 14:21:12.426061732 -0600 -@@ -62,6 +62,7 @@ OCAMLBEST = @OCAMLBEST@ - OCAMLVERSION = @OCAMLVERSION@ - COQC = @COQC@ - COQDEP = @COQDEP@ -+COQFLAGS = @COQFLAGS@ - FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@ - MENHIR = @MENHIR@ - -@@ -1068,7 +1069,7 @@ COQLIBS_FILES = lib/coq/BuiltIn lib/coq/ - - %.vo: %.v - $(SHOW) 'Coqc $<' -- $(HIDE)$(COQC) -R lib/coq Why3 $< -+ $(HIDE)$(COQC) $(COQFLAGS) -R lib/coq Why3 $< - - %.vd: %.v - $(SHOW) 'Coqdep $<' ---- why3-1.6.0/share/provers-detection-data.conf.orig 2023-03-07 02:15:31.000000000 -0700 -+++ why3-1.6.0/share/provers-detection-data.conf 2023-06-26 14:22:52.768680868 -0600 -@@ -838,16 +838,8 @@ support_library = "%l/coq/version" - exec = "coqtop" - version_switch = "-v" - version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)" --version_ok = "^8\.16\.[0-9]+$" --version_ok = "^8\.15\.[0-9]+$" --version_ok = "^8\.14\.[0-9]+$" --version_ok = "^8\.13\.[0-9]+$" --version_ok = "^8\.12\.[0-9]+$" --version_ok = "^8\.11\.[0-9]+$" --version_ok = "^8\.10\.[0-9]+$" --version_ok = "^8\.9\.[0-9]+$" --version_ok = "^8\.8\.[0-9]+$" --version_ok = "^8\.7\.[0-9]+$" -+version_ok = "^8\.1[0-7]\.[0-9]+$" -+version_ok = "^8\.[7-9]\.[0-9]+$" - version_old = "8.6.1" - version_old = "8.6" - version_old = "^8\.5pl[1-3]$" diff --git a/why3.spec b/why3.spec index d9c2622..76f7b7b 100644 --- a/why3.spec +++ b/why3.spec @@ -17,8 +17,8 @@ ExclusiveArch: %{ocaml_native_compiler} %endif Name: why3 -Version: 1.6.0 -Release: 6%{?dist} +Version: 1.7.0 +Release: 1%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception @@ -29,10 +29,6 @@ Source1: fr.lri.%{name}.desktop # AppData file written by Jerry James Source2: fr.lri.%{name}.metainfo.xml -# Support coq 8.17. See -# https://gitlab.inria.fr/why3/why3/-/commit/64facc03bdc2bc4ce0586ff2f458bcd87f646ba8 -Patch0: %{name}-coq-8.17.patch - BuildRequires: coq BuildRequires: emacs-nox BuildRequires: emacs-proofgeneral @@ -84,14 +80,6 @@ Provides: bundled(js-jquery) # The corresponding Provides is not generated, so filter this out %global __requires_exclude ocaml\\\((Driver_ast|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} - # This can be removed when F39 reaches EOL Obsoletes: %{name}-xemacs < 1.4.0-4 @@ -125,10 +113,6 @@ Summary: Complete Why3 software verification platform suite Requires: %{name}%{?_isa} = %{version}-%{release} Requires: alt-ergo coq cvc5 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. @@ -270,7 +254,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %{_datadir}/icons/hicolor/scalable/%{name}.svg %{_datadir}/vim/vimfiles/ftdetect/%{name}.vim %{_datadir}/vim/vimfiles/syntax/%{name}.vim -%{_datadir}/zsh/ +%{_datadir}/zsh/site-functions/_why3 %{_texmf}/tex/latex/why3/ %{_libdir}/%{name}/ %{_metainfodir}/fr.lri.%{name}.metainfo.xml @@ -308,6 +292,10 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Tue Jan 2 2024 Jerry James - 1.7.0-1 +- Version 1.7.0 +- Drop upstreamed coq patch + * Sat Sep 9 2023 Jerry James - 1.6.0-6 - Rebuild for ocaml-ocamlgraph 2.1.0 From b04eb93322a82251b8fa3ca083964ebd8e3c49aa Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 2 Feb 2024 16:41:48 -0700 Subject: [PATCH 2/3] Version 1.7.1 --- sources | 2 +- why3.spec | 11 ++++------- 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/sources b/sources index 2c57c42..8b5ff60 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (why3-1.7.0.tar.gz) = 1fb458e58b75662e3cc4f3cdb42b0e2229d5c73e44a182370ce8beca3a2e18ac8b6c9a403ba94f9391d46cb9bd47cd37cfc9592c77cc2164a7f92124f6f557b6 +SHA512 (why3-1.7.1.tar.gz) = 3b1636e9459aced943a6b895aa7a6db3552adcf9878c2fa2b67913d6b555b67b00f6f1c9b28ffa80cbdf3fa01007aa7f8c9c4fa6c8c56dee579955cf5d57980b diff --git a/why3.spec b/why3.spec index 76f7b7b..5eb7f9a 100644 --- a/why3.spec +++ b/why3.spec @@ -1,12 +1,6 @@ # Coq's plugin architecture requires cmxs files, so: ExclusiveArch: %{ocaml_native_compiler} -# ANTLR is unavailable on i686, so coq is also unavailable. We could build -# without coq support, but choose to forgo i686 support entirely. -# See https://fedoraproject.org/wiki/Changes/Drop_i686_JDKs -# See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval -#ExclusiveArch: %%{java_arches} - # NOTE: Upstream has said that the Frama-C support is still experimental, and # less functional than the corresponding support in why2. They recommend not # enabling it for now. We abide by their wishes. Revisit this decision each @@ -17,7 +11,7 @@ ExclusiveArch: %{ocaml_native_compiler} %endif Name: why3 -Version: 1.7.0 +Version: 1.7.1 Release: 1%{?dist} Summary: Software verification platform @@ -292,6 +286,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Fri Feb 2 2024 Jerry James - 1.7.1-1 +- Version 1.7.1 + * Tue Jan 2 2024 Jerry James - 1.7.0-1 - Version 1.7.0 - Drop upstreamed coq patch From 0e4b6bbc827f7a260d64a4417162c790195c5910 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 18 Apr 2024 12:18:03 -0600 Subject: [PATCH 3/3] Version 1.7.2 --- sources | 2 +- why3.spec | 22 +++++++++++----------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/sources b/sources index 8b5ff60..a941d8e 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (why3-1.7.1.tar.gz) = 3b1636e9459aced943a6b895aa7a6db3552adcf9878c2fa2b67913d6b555b67b00f6f1c9b28ffa80cbdf3fa01007aa7f8c9c4fa6c8c56dee579955cf5d57980b +SHA512 (why3-1.7.2.tar.gz) = 7e80671480ce0dc3c69514bea2836f5899c686b43a4e8607c27d28e63f78150150dc45fcac5760dbee9721d363e456b1dcaeb1501fc9f63f360722a1021f675f diff --git a/why3.spec b/why3.spec index 5eb7f9a..2d47fb0 100644 --- a/why3.spec +++ b/why3.spec @@ -6,17 +6,14 @@ ExclusiveArch: %{ocaml_native_compiler} # 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.7.1 +Version: 1.7.2 Release: 1%{?dist} Summary: Software verification platform License: LGPL-2.1-only WITH OCaml-LGPL-linking-exception URL: https://why3.lri.fr/ +VCS: https://gitlab.inria.fr/why3/why3 Source0: https://why3.gitlabpages.inria.fr/releases/%{name}-%{version}.tar.gz # Desktop file written by Jerry James Source1: fr.lri.%{name}.desktop @@ -182,12 +179,12 @@ cd - %endif # Install the bash completion file -mkdir -p %{buildroot}%{_datadir}/bash-completion/completions -cp -p share/bash/%{name} %{buildroot}%{_datadir}/bash-completion/completions +mkdir -p %{buildroot}%{bash_completions_dir} +cp -p share/bash/%{name} %{buildroot}%{bash_completions_dir} # Install the zsh completion file -mkdir -p %{buildroot}%{_datadir}/zsh/site-functions -cp -p share/zsh/_why3 %{buildroot}%{_datadir}/zsh/site-functions +mkdir -p %{buildroot}%{zsh_completions_dir} +cp -p share/zsh/_why3 %{buildroot}%{zsh_completions_dir} # Install the LaTeX style mkdir -p %{buildroot}%{_texmf}/tex/latex/why3 @@ -239,16 +236,16 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %license LICENSE %{_bindir}/%{name} %{_bindir}/isabelle_client +%{bash_completions_dir}/why3 +%{zsh_completions_dir}/_why3 %{_datadir}/%{name}/ %{_datadir}/applications/fr.lri.%{name}.desktop -%{_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/%{name}.svg %{_datadir}/vim/vimfiles/ftdetect/%{name}.vim %{_datadir}/vim/vimfiles/syntax/%{name}.vim -%{_datadir}/zsh/site-functions/_why3 %{_texmf}/tex/latex/why3/ %{_libdir}/%{name}/ %{_metainfodir}/fr.lri.%{name}.metainfo.xml @@ -286,6 +283,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %files all %changelog +* Thu Apr 18 2024 Jerry James - 1.7.2-1 +- Version 1.7.2 + * Fri Feb 2 2024 Jerry James - 1.7.1-1 - Version 1.7.1