Version 1.7.2

sources

@@ -1 +1 @@
-SHA512 (why3-1.6.0.tar.gz) = 60d61b8337ab9f2fd2e6c7174eb0bab063f122417738cd75990c5c53120dd535bcedccb670567f5753853d6bc9f8efebb563d079e4d368372a7687193f1346b1
+SHA512 (why3-1.7.2.tar.gz) = 7e80671480ce0dc3c69514bea2836f5899c686b43a4e8607c27d28e63f78150150dc45fcac5760dbee9721d363e456b1dcaeb1501fc9f63f360722a1021f675f

why3-coq-8.17.patch

@@ -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]$"

why3.spec

@@ -1,38 +1,25 @@
 # 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
 # release.
 
-%ifnarch %{ocaml_native_compiler}
-%global debug_package %{nil}
-%endif
-
 Name:           why3
-Version:        1.6.0
-Release:        6%{?dist}
+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
 # 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 +71,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 +104,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.
@@ -204,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
@@ -261,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/
 %{_texmf}/tex/latex/why3/
 %{_libdir}/%{name}/
 %{_metainfodir}/fr.lri.%{name}.metainfo.xml
@@ -308,6 +283,16 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %files all
 
 %changelog
+* Thu Apr 18 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-1
+- Version 1.7.2
+
+* Fri Feb  2 2024 Jerry James <loganjerry@gmail.com> - 1.7.1-1
+- Version 1.7.1
+
+* Tue Jan  2 2024 Jerry James <loganjerry@gmail.com> - 1.7.0-1
+- Version 1.7.0
+- Drop upstreamed coq patch
+
 * Sat Sep  9 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-6
 - Rebuild for ocaml-ocamlgraph 2.1.0