add(nix): why3 (with provers)

nix/custom/default.nix

@@ -2,6 +2,7 @@
   callPackage,
   unstable,
   opam-nix,
+  alt-ergo,
 }: let
   mkNerdFont = callPackage ./mkNerdFont.nix {inherit (unstable) nerd-font-patcher;};
 
@@ -20,6 +21,8 @@
     font = hiosevka;
     extraArgs = ["--name {/.}-NFP" "--variable-width-glyphs"];
   };
+
+  why3 = callPackage ./why3.nix {inherit alt-ergo;};
 in {
   myPkgs = {
     inherit
@@ -28,6 +31,7 @@ in {
       hiosevka
       hiosevka-nerd-font-mono
       hiosevka-nerd-font-propo
+      why3
       ;
   };
 

nix/custom/why3.nix

@@ -0,0 +1,27 @@
+{
+  symlinkJoin,
+  makeWrapper,
+  why3,
+  alt-ergo,
+  cvc4,
+  z3_4_12,
+}: let
+  provers = [
+    alt-ergo
+    cvc4
+    z3_4_12
+  ];
+in
+  symlinkJoin {
+    name = "why3";
+    # Generate configuration in the store, and wrap why3 with the corresponding option
+    paths = [
+      (why3.override {version = "1.6.0";})
+    ];
+    buildInputs = provers;
+    nativeBuildInputs = [makeWrapper];
+    postBuild = ''
+      $out/bin/why3 config detect --config=$out/why3.conf
+      wrapProgram $out/bin/why3 --add-flags "--config=$out/why3.conf"
+    '';
+  }