From 9aa4c5dbfc806b2f71ad351fc79d5d0312e0caa4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= <supermanitu@gmail.com>
Date: Wed, 20 Apr 2022 11:21:26 +0200
Subject: [PATCH] isabelle: Make closer to upstream

This makes isabelle use the versions of polyml and z3 that are also used
upstream. Additionally it packages the sha1 library that isabelle uses.

Co-authored-by: 1000teslas <47207223+1000teslas@users.noreply.github.com>
---
 .../science/logic/isabelle/default.nix        | 33 +++++++++++++++++--
 pkgs/top-level/all-packages.nix               | 20 +++++++++--
 2 files changed, 49 insertions(+), 4 deletions(-)

diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix
index 6696527cece..9e5d40be2c6 100644
--- a/pkgs/applications/science/logic/isabelle/default.nix
+++ b/pkgs/applications/science/logic/isabelle/default.nix
@@ -1,7 +1,33 @@
-{ lib, stdenv, fetchurl, coreutils, nettools, java, scala, polyml, z3, veriT, vampire, eprover-ho, naproche, rlwrap, perl, makeDesktopItem, isabelle-components, isabelle, symlinkJoin }:
+{ lib, stdenv, fetchurl, coreutils, nettools, java, scala, polyml, z3, veriT, vampire, eprover-ho, naproche, rlwrap, perl, makeDesktopItem, isabelle-components, isabelle, symlinkJoin, fetchhg }:
 # nettools needed for hostname
 
-stdenv.mkDerivation rec {
+let
+  sha1 = stdenv.mkDerivation {
+    pname = "isabelle-sha1";
+    version = "2021-1";
+
+    src = fetchhg {
+      url = "https://isabelle.sketis.net/repos/sha1";
+      rev = "e0239faa6f42";
+      sha256 = "sha256-4sxHzU/ixMAkSo67FiE6/ZqWJq9Nb9OMNhMoXH2bEy4=";
+    };
+
+    buildPhase = (if stdenv.isDarwin then ''
+      LDFLAGS="-dynamic -undefined dynamic_lookup -lSystem"
+    '' else ''
+      LDFLAGS="-fPIC -shared"
+    '') + ''
+      CFLAGS="-fPIC -I."
+      $CC $CFLAGS -c sha1.c -o sha1.o
+      $LD $LDFLAGS sha1.o -o libsha1.so
+    '';
+
+    installPhase = ''
+      mkdir -p $out/lib
+      cp libsha1.so $out/lib/
+    '';
+  };
+in stdenv.mkDerivation rec {
   pname = "isabelle";
   version = "2021-1";
 
@@ -82,6 +108,9 @@ stdenv.mkDerivation rec {
       --replace 'cmd.add("/usr/bin/env");' "" \
       --replace 'cmd.add("bash");' "cmd.add(\"$SHELL\");"
 
+    substituteInPlace src/Pure/General/sha1.ML \
+      --replace '"$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so")' '"${sha1}/lib/libsha1.so"'
+
     rm -r heaps
   '' + (if ! stdenv.isLinux then "" else ''
     arch=${if stdenv.hostPlatform.system == "x86_64-linux" then "x86_64-linux" else "x86-linux"}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 789360728df..44367c50337 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -32975,12 +32975,28 @@ with pkgs;
   ifstat-legacy = callPackage ../tools/networking/ifstat-legacy { };
 
   isabelle = callPackage ../applications/science/logic/isabelle {
-    polyml = lib.overrideDerivation polyml (_: {
+    polyml = polyml.overrideAttrs (_: {
+      pname = "polyml-for-isabelle";
+      version = "2021-1";
       configureFlags = [ "--enable-intinf-as-int" "--with-gmp" "--disable-shared" ];
+      buildFlags = [ "compiler" ];
+      src = fetchFromGitHub {
+        owner = "polyml";
+        repo = "polyml";
+        rev = "39d96a2def903ed019c6855e3b688df5070d633a";
+        sha256 = "sha256-S7d2Vr/nB+rCX9d4qQj4f7edVZKocKIjc5rrx9A/B4Q=";
+      };
     });
 
     java = openjdk17;
-    z3 = z3_4_4_0;
+    z3 = z3_4_4_0.overrideAttrs (_: {
+      src = fetchFromGitHub {
+        owner = "Z3Prover";
+        repo = "z3";
+        rev = "0482e7fe727c75e259ac55a932b28cf1842c530e";
+        sha256 = "1m53avlljxqd2p8w266ksmjywjycsd23h224yn786qsnf36dr63x";
+      };
+    });
   };
   isabelle-components = recurseIntoAttrs (callPackage ../applications/science/logic/isabelle/components { });