From 6e3a86f2f73a466656a401302d3ece26fba401d9 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Sat, 30 Apr 2022 15:37:40 +0200
Subject: [PATCH 1/2] why3.withProvers: fix #168644

---
 pkgs/applications/science/logic/why3/with-provers.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pkgs/applications/science/logic/why3/with-provers.nix b/pkgs/applications/science/logic/why3/with-provers.nix
index ae0acb1e525..739064bb616 100644
--- a/pkgs/applications/science/logic/why3/with-provers.nix
+++ b/pkgs/applications/science/logic/why3/with-provers.nix
@@ -27,6 +27,6 @@ stdenv.mkDerivation {
 
   installPhase = ''
     mkdir -p $out/bin
-    makeWrapper ${why3}/bin/why3 $out/bin/why3 --add-flags "--extra-config $out/share/why3/why3.conf"
+    makeWrapper ${why3}/bin/why3 $out/bin/why3 --add-flags "--config $out/share/why3/why3.conf"
   '';
 }

From 4a87fcbc86fd458a790b09c849ad451812dcdc33 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Sat, 30 Apr 2022 15:53:28 +0200
Subject: [PATCH 2/2] =?UTF-8?q?why3:=201.4.1=20=E2=86=92=201.5.0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

easycrypt: fix build with why3-1.5.0
frama-c: build with why3 1.4.1
---
 pkgs/applications/science/logic/easycrypt/default.nix | 8 +++++++-
 pkgs/applications/science/logic/why3/default.nix      | 4 ++--
 pkgs/development/tools/analysis/frama-c/default.nix   | 9 +++++++++
 3 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/pkgs/applications/science/logic/easycrypt/default.nix b/pkgs/applications/science/logic/easycrypt/default.nix
index 5f28ca73c4e..da4ff212e29 100644
--- a/pkgs/applications/science/logic/easycrypt/default.nix
+++ b/pkgs/applications/science/logic/easycrypt/default.nix
@@ -1,4 +1,4 @@
-{ lib, stdenv, fetchFromGitHub, ocamlPackages, why3 }:
+{ lib, stdenv, fetchFromGitHub, fetchpatch, ocamlPackages, why3 }:
 
 stdenv.mkDerivation rec {
   pname = "easycrypt";
@@ -11,6 +11,12 @@ stdenv.mkDerivation rec {
     sha256 = "sha256:09rdwcj70lkamkhd895p284rfpz4bcnsf55mcimhiqncd2a21ml7";
   };
 
+  # Fix build with Why3 1.5
+  patches = fetchpatch {
+    url = "https://github.com/EasyCrypt/easycrypt/commit/d226387432deb7f22738e1d5579346a2cbc9be7a.patch";
+    sha256 = "sha256:1zvxij35fnr3h9b5wdl8ml17aqfx3a39rd4mgwmdvkapbg3pa4lm";
+  };
+
   nativeBuildInputs = with ocamlPackages; [
     dune_3
     findlib
diff --git a/pkgs/applications/science/logic/why3/default.nix b/pkgs/applications/science/logic/why3/default.nix
index 0f3dab8038e..8917135b2c8 100644
--- a/pkgs/applications/science/logic/why3/default.nix
+++ b/pkgs/applications/science/logic/why3/default.nix
@@ -3,11 +3,11 @@
 
 stdenv.mkDerivation rec {
   pname = "why3";
-  version = "1.4.1";
+  version = "1.5.0";
 
   src = fetchurl {
     url = "https://why3.gitlabpages.inria.fr/releases/${pname}-${version}.tar.gz";
-    sha256 = "sha256:1rqyypzlvagrn43ykl0c5wxyvnry5fl1ykn3xcvlzgghk96yq3jq";
+    sha256 = "sha256:0qjh49pyqmg3xi09fn4lyzz23i6h18y9sgc8ayscvx3bwr3vcqhr";
   };
 
   buildInputs = with ocamlPackages; [
diff --git a/pkgs/development/tools/analysis/frama-c/default.nix b/pkgs/development/tools/analysis/frama-c/default.nix
index b5ae5055d02..0b962a97ef1 100644
--- a/pkgs/development/tools/analysis/frama-c/default.nix
+++ b/pkgs/development/tools/analysis/frama-c/default.nix
@@ -4,6 +4,15 @@
 , gdk-pixbuf, wrapGAppsHook
 }:
 
+let why3_1_5 = why3; in
+let why3 = why3_1_5.overrideAttrs (o: rec {
+  version = "1.4.1";
+  src = fetchurl {
+    url = "https://why3.gitlabpages.inria.fr/releases/${o.pname}-${version}.tar.gz";
+    sha256 = "sha256:1rqyypzlvagrn43ykl0c5wxyvnry5fl1ykn3xcvlzgghk96yq3jq";
+  };
+}); in
+
 let
   mkocamlpath = p: "${p}/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib";
   runtimeDeps = with ocamlPackages; [