From 6c70d9252ab4bf05843656d5d42477a1e9ac045f Mon Sep 17 00:00:00 2001
From: Weijia Wang <9713184+wegank@users.noreply.github.com>
Date: Mon, 9 Jan 2023 20:10:30 +0100
Subject: [PATCH] satallax: add darwin support

---
 .../science/logic/satallax/default.nix        | 28 +++++++++++++++----
 pkgs/top-level/all-packages.nix               |  4 +--
 2 files changed, 23 insertions(+), 9 deletions(-)

diff --git a/pkgs/applications/science/logic/satallax/default.nix b/pkgs/applications/science/logic/satallax/default.nix
index 7a523bbf24e..648ebee6550 100644
--- a/pkgs/applications/science/logic/satallax/default.nix
+++ b/pkgs/applications/science/logic/satallax/default.nix
@@ -1,10 +1,10 @@
-{lib, stdenv, fetchurl, ocaml, zlib, which, eprover, makeWrapper, coq}:
+{ lib, stdenv, fetchurl, ocaml, zlib, which, eprover, makeWrapper, coq }:
 stdenv.mkDerivation rec {
   pname = "satallax";
   version = "2.7";
 
   nativeBuildInputs = [ makeWrapper ];
-  buildInputs = [ocaml zlib which eprover coq];
+  buildInputs = [ ocaml zlib which eprover coq ];
   src = fetchurl {
     url = "https://www.ps.uni-saarland.de/~cebrown/satallax/downloads/${pname}-${version}.tar.gz";
     sha256 = "1kvxn8mc35igk4vigi5cp7w3wpxk2z3bgwllfm4n3h2jfs0vkpib";
@@ -15,6 +15,10 @@ stdenv.mkDerivation rec {
     ./fix-declaration-gcc9.patch
   ];
 
+  prePatch = ''
+    patch -p1 -i ${../avy/minisat-fenv.patch} -d minisat
+  '';
+
   preConfigure = ''
     mkdir fake-tools
     echo "echo 'Nix-build-host.localdomain'" > fake-tools/hostname
@@ -41,7 +45,8 @@ stdenv.mkDerivation rec {
     )
   '';
 
-  postBuild = "echo testing; ! (bash ./test | grep ERROR)";
+  # error: invalid suffix on literal; C++11 requires a space between literal and identifier
+  NIX_CFLAGS_COMPILE = lib.optionalString stdenv.isDarwin "-Wno-reserved-user-defined-literal";
 
   installPhase = ''
     mkdir -p "$out/share/doc/satallax" "$out/bin" "$out/lib" "$out/lib/satallax"
@@ -59,11 +64,22 @@ stdenv.mkDerivation rec {
     cp -r coq* "$out/lib/satallax/"
   '';
 
+  doCheck = stdenv.isLinux;
+
+  checkPhase = ''
+    runHook preCheck
+    if bash ./test | grep ERROR; then
+      echo "Tests failed"
+      exit 1
+    fi
+    runHook postCheck
+  '';
+
   meta = {
     description = "Automated theorem prover for higher-order logic";
-    license = lib.licenses.mit ;
-    maintainers = [lib.maintainers.raskin];
-    platforms = lib.platforms.linux;
+    license = lib.licenses.mit;
+    maintainers = [ lib.maintainers.raskin ];
+    platforms = lib.platforms.unix;
     downloadPage = "http://www.ps.uni-saarland.de/~cebrown/satallax/downloads.php";
     homepage = "http://www.ps.uni-saarland.de/~cebrown/satallax/index.php";
   };
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 7424cf7bff1..baee5eb6014 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -36264,9 +36264,7 @@ with pkgs;
 
   proverif = callPackage ../applications/science/logic/proverif { };
 
-  satallax = callPackage ../applications/science/logic/satallax {
-    ocaml = ocaml-ng.ocamlPackages_4_01_0.ocaml;
-  };
+  satallax = callPackage ../applications/science/logic/satallax { };
 
   saw-tools = callPackage ../applications/science/logic/saw-tools {};