From e57fd9accfaf81866432af7e5630c0664d4e9273 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 9 Jun 2025 15:05:43 -0600 Subject: [PATCH 1/4] Version 1.8.1 - All patches have been upstreamed --- sources | 2 +- why3-c23.patch | 25 ------------------------- why3-link-order.patch | 20 -------------------- why3.spec | 12 ++---------- 4 files changed, 3 insertions(+), 56 deletions(-) delete mode 100644 why3-c23.patch delete mode 100644 why3-link-order.patch diff --git a/sources b/sources index 99a1865..5946fe5 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (why3-1.8.0.tar.gz) = 8d30ac4a1280a7d7741ef862365e06aa3218a78fd01ca7f969f0d6515245c7259fcc81897bfe08c581c6b37639d1465ab4a96657f3baf4c747988df8201d4549 +SHA512 (why3-1.8.1.tar.gz) = b188b64cc8f116c2174e78d1ccb65dede0984265b8ed2fdf8160bf67e74bf9fb24cbb1d5b3c130f924424222b9241f89525cade66f5de7ef66d714eb2e6448b4 diff --git a/why3-c23.patch b/why3-c23.patch deleted file mode 100644 index 736756b..0000000 --- a/why3-c23.patch +++ /dev/null @@ -1,25 +0,0 @@ -Fixes this error: - -src/server/cpulimit-unix.c: In function ‘main’: -src/server/cpulimit-unix.c:95:23: error: assignment to ‘__sighandler_t’ {aka ‘void (*)(int)’} from incompatible pointer type ‘void (*)(void)’ [-Wincompatible-pointer-types] - 95 | sa.sa_handler = &wallclock_timelimit_reached; - | ^ -src/server/cpulimit-unix.c:45:6: note: ‘wallclock_timelimit_reached’ declared here - 45 | void wallclock_timelimit_reached() { - | ^~~~~~~~~~~~~~~~~~~~~~~~~~~ -In file included from src/server/cpulimit-unix.c:22: -/usr/include/signal.h:72:16: note: ‘__sighandler_t’ declared here - 72 | typedef void (*__sighandler_t) (int); - | ^~~~~~~~~~~~~~ - ---- why3-1.8.0/src/server/cpulimit-unix.c.orig 2024-12-11 06:21:37.000000000 -0700 -+++ why3-1.8.0/src/server/cpulimit-unix.c 2025-01-22 14:48:28.808369208 -0700 -@@ -42,7 +42,7 @@ void show_time() { - } - } - --void wallclock_timelimit_reached() { -+void wallclock_timelimit_reached([[maybe_unused]] int sig) { - fprintf(stderr, - "Why3cpulimit: wallclock timelimit %d reached, killing command\n", - wallclock_timelimit); diff --git a/why3-link-order.patch b/why3-link-order.patch deleted file mode 100644 index 25cfeec..0000000 --- a/why3-link-order.patch +++ /dev/null @@ -1,20 +0,0 @@ -Fixes this error: - -File "_none_", line 1: -Error: Forward reference to "Ptree_helpers" in file "src/bddinfer/why3infer.cmo" - ---- why3-1.8.0/Makefile.in.orig 2024-12-11 06:21:37.000000000 -0700 -+++ why3-1.8.0/Makefile.in 2024-12-16 10:27:14.100846332 -0700 -@@ -318,10 +318,10 @@ LIBMODULES = $(addprefix src/util/, $(L - $(addprefix src/core/, $(LIB_CORE)) \ - $(addprefix src/driver/, $(LIB_DRIVER)) \ - $(addprefix src/mlw/, $(LIB_MLW)) \ -- $(addprefix src/infer/, $(LIB_INFER)) \ -- $(addprefix src/bddinfer/, $(LIB_BDDINFER)) \ - $(addprefix src/extract/, $(LIB_EXTRACT)) \ - $(addprefix src/parser/, $(LIB_PARSER)) \ -+ $(addprefix src/infer/, $(LIB_INFER)) \ -+ $(addprefix src/bddinfer/, $(LIB_BDDINFER)) \ - $(addprefix src/transform/, $(LIB_TRANSFORM)) \ - $(addprefix src/printer/, $(LIB_PRINTER)) \ - $(addprefix src/session/, $(LIB_SESSION)) diff --git a/why3.spec b/why3.spec index 12b1211..b08043f 100644 --- a/why3.spec +++ b/why3.spec @@ -7,7 +7,7 @@ ExclusiveArch: %{ocaml_native_compiler} # release. Name: why3 -Version: 1.8.0 +Version: 1.8.1 Release: %autorelease Summary: Software verification platform @@ -19,10 +19,6 @@ Source0: https://why3.gitlabpages.inria.fr/releases/%{name}-%{version}.ta Source1: fr.lri.%{name}.desktop # AppData file written by Jerry James Source2: fr.lri.%{name}.metainfo.xml -# Fix a link order issue -Patch: %{name}-link-order.patch -# Fix an incompatible pointer issue with C23 -Patch: %{name}-c23.patch BuildRequires: coq BuildRequires: emacs-nw @@ -161,13 +157,9 @@ sed -e 's|-Wall|%{build_cflags} %{build_ldflags}|;s/ -O -g//' \ sed -i.orig 's,(MY_PATH_TO_WHY3)/share/whyitp,%{_emacs_sitelispdir},' share/whyitp/README fixtimestamp share/whyitp/README -# Fix a configure script typo -sed -i 's/\$(OCAMLC/$(ocamlc/' configure - %build %configure --enable-verbose-make --enable-bddinfer -# Work around a Makefile bug in version 1.8.0 -ln -s why3.opt bin/why3 + # FIXME: Parallel make sometimes fails make # The documentation build is broken in the 1.8.0 release From 655ea3197d32e2ec9f668e6fe9a12e0092bdc35d Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 10 Aug 2025 11:23:17 -0600 Subject: [PATCH 2/4] Use %{vimfiles_root} --- why3.spec | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/why3.spec b/why3.spec index b08043f..331b1cc 100644 --- a/why3.spec +++ b/why3.spec @@ -212,10 +212,10 @@ appstream-util validate-relax --nonet \ %{buildroot}%{_metainfodir}/fr.lri.%{name}.metainfo.xml # Move the vim file to the right place -mkdir -p %{buildroot}%{_datadir}/vim/vimfiles +mkdir -p %{buildroot}%{vimfiles_root} mv %{buildroot}%{_datadir}/%{name}/vim/ftdetect \ %{buildroot}%{_datadir}/%{name}/vim/syntax \ - %{buildroot}%{_datadir}/vim/vimfiles + %{buildroot}%{vimfiles_root} # Byte compile the Emacs support files cp -p share/whyitp/whyitp.el %{buildroot}%{_emacs_sitelispdir} @@ -246,8 +246,8 @@ chmod 0755 %{buildroot}%{_bindir}/* \ %{_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 -%{_datadir}/vim/vimfiles/ftdetect/%{name}.vim -%{_datadir}/vim/vimfiles/syntax/%{name}.vim +%{vimfiles_root}/ftdetect/%{name}.vim +%{vimfiles_root}/syntax/%{name}.vim %{_texmf}/tex/latex/why3/ %{_libdir}/%{name}/ %{_metainfodir}/fr.lri.%{name}.metainfo.xml From 78e4daa8311db633c3733c5ff2658684695e0496 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 10 Aug 2025 11:47:45 -0600 Subject: [PATCH 3/4] BR vim-filesystem for %{vimfiles_root} --- why3.spec | 1 + 1 file changed, 1 insertion(+) diff --git a/why3.spec b/why3.spec index 331b1cc..75df845 100644 --- a/why3.spec +++ b/why3.spec @@ -58,6 +58,7 @@ BuildRequires: tex(tgtermes.sty) BuildRequires: tex(upquote.sty) BuildRequires: tex(wrapfig.sty) BuildRequires: tex-urlbst +BuildRequires: vim-filesystem Requires: gtksourceview3%{?_isa} Requires: hicolor-icon-theme From d8e269ccc793c8eff76849bb49994dcb8359cb92 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 16 Sep 2025 15:25:39 -0600 Subject: [PATCH 4/4] Version 1.8.2 --- sources | 2 +- why3.spec | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/sources b/sources index 5946fe5..f503a9e 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (why3-1.8.1.tar.gz) = b188b64cc8f116c2174e78d1ccb65dede0984265b8ed2fdf8160bf67e74bf9fb24cbb1d5b3c130f924424222b9241f89525cade66f5de7ef66d714eb2e6448b4 +SHA512 (why3-1.8.2.tar.gz) = a35e88fafe1aa29c36d2248c1a644eae85afa1bb7b3009193f4a5c28ba684d0882717d63733d8581a7c2cd5ec493e2d15c82baabef615b4d00323fa9309875f8 diff --git a/why3.spec b/why3.spec index 75df845..6b24ceb 100644 --- a/why3.spec +++ b/why3.spec @@ -7,7 +7,7 @@ ExclusiveArch: %{ocaml_native_compiler} # release. Name: why3 -Version: 1.8.1 +Version: 1.8.2 Release: %autorelease Summary: Software verification platform