Version 1.8.2

- All patches have been upstreamed

sources

@@ -1 +1 @@
-SHA512 (why3-1.8.0.tar.gz) = 8d30ac4a1280a7d7741ef862365e06aa3218a78fd01ca7f969f0d6515245c7259fcc81897bfe08c581c6b37639d1465ab4a96657f3baf4c747988df8201d4549
+SHA512 (why3-1.8.2.tar.gz) = a35e88fafe1aa29c36d2248c1a644eae85afa1bb7b3009193f4a5c28ba684d0882717d63733d8581a7c2cd5ec493e2d15c82baabef615b4d00323fa9309875f8

why3-c23.patch

@@ -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);

why3-link-order.patch

@@ -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))

why3.spec

@@ -7,7 +7,7 @@ ExclusiveArch: %{ocaml_native_compiler}
 # release.
 
 Name:           why3
-Version:        1.8.0
+Version:        1.8.2
 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
@@ -62,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
@@ -161,13 +158,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
@@ -220,10 +213,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}
@@ -254,8 +247,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