From 0391279c2479fa7dcf744238ac071b6cad0673b6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= <supermanitu@gmail.com>
Date: Mon, 14 Feb 2022 12:40:49 +0100
Subject: [PATCH] isabelle: Add isabelle-linter as optional component

---
 .../logic/isabelle/components/default.nix     |  5 +++
 .../isabelle/components/isabelle-linter.nix   | 22 ++++++++++++
 .../logic/isabelle/components/mkBuild.nix     | 36 +++++++++++++++++++
 .../science/logic/isabelle/default.nix        | 27 +++++++++++++-
 pkgs/top-level/all-packages.nix               |  1 +
 5 files changed, 90 insertions(+), 1 deletion(-)
 create mode 100644 pkgs/applications/science/logic/isabelle/components/default.nix
 create mode 100644 pkgs/applications/science/logic/isabelle/components/isabelle-linter.nix
 create mode 100644 pkgs/applications/science/logic/isabelle/components/mkBuild.nix

diff --git a/pkgs/applications/science/logic/isabelle/components/default.nix b/pkgs/applications/science/logic/isabelle/components/default.nix
new file mode 100644
index 000000000000..dd7b605f56af
--- /dev/null
+++ b/pkgs/applications/science/logic/isabelle/components/default.nix
@@ -0,0 +1,5 @@
+{ callPackage }:
+
+{
+  isabelle-linter = callPackage ./isabelle-linter.nix {};
+}
diff --git a/pkgs/applications/science/logic/isabelle/components/isabelle-linter.nix b/pkgs/applications/science/logic/isabelle/components/isabelle-linter.nix
new file mode 100644
index 000000000000..7fca547f67c8
--- /dev/null
+++ b/pkgs/applications/science/logic/isabelle/components/isabelle-linter.nix
@@ -0,0 +1,22 @@
+{ stdenv, lib, fetchFromGitHub, isabelle }:
+
+stdenv.mkDerivation rec {
+  pname = "isabelle-linter";
+  version = "Isabelle2021-1-v1.0.0";
+
+  src = fetchFromGitHub {
+    owner = "isabelle-prover";
+    repo = "isabelle-linter";
+    rev = version;
+    sha256 = "0v6scc2rhj6bjv530gzz6i57czzcgpkw7a9iqnfdnm5gvs5qjk7a";
+  };
+
+  installPhase = import ./mkBuild.nix { inherit isabelle; path = "${pname}-${version}"; };
+
+  meta = with lib; {
+    description = "Linter component for Isabelle.";
+    homepage = "https://github.com/isabelle-prover/isabelle-linter";
+    maintainers = with maintainers; [ jvanbruegge ];
+    license = licenses.mit;
+  };
+}
diff --git a/pkgs/applications/science/logic/isabelle/components/mkBuild.nix b/pkgs/applications/science/logic/isabelle/components/mkBuild.nix
new file mode 100644
index 000000000000..a05b5196b007
--- /dev/null
+++ b/pkgs/applications/science/logic/isabelle/components/mkBuild.nix
@@ -0,0 +1,36 @@
+{ isabelle, path }:
+
+let
+  dir = "$out/isabelle/${isabelle.dirname}";
+  iDir = "${isabelle}/${isabelle.dirname}";
+in ''
+  shopt -s extglob
+  mkdir -p ${dir}/lib/classes
+
+  cDir=$out/${isabelle.dirname}/contrib/${path}
+  mkdir -p $cDir
+  cp -r !(isabelle) $cDir
+
+  cd ${dir}
+  ln -s ${iDir}/!(lib|bin) ./
+  ln -s ${iDir}/lib/!(classes) lib/
+  ln -s ${iDir}/lib/classes/* lib/classes/
+
+  mkdir bin/
+  cp ${iDir}/bin/* bin/
+
+  export HOME=$TMP
+  bin/isabelle components -u $cDir
+  bin/isabelle scala_build
+
+  cd lib/classes
+  for f in ${iDir}/lib/classes/*; do
+    rm $(basename $f)
+  done
+
+  lDir=$out/${isabelle.dirname}/lib/classes/
+  mkdir -p $lDir
+  cp -r * $lDir
+  cd $out
+  rm -rf isabelle
+''
diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix
index 1c613419cc86..6696527cece2 100644
--- a/pkgs/applications/science/logic/isabelle/default.nix
+++ b/pkgs/applications/science/logic/isabelle/default.nix
@@ -1,4 +1,4 @@
-{ lib, stdenv, fetchurl, coreutils, nettools, java, scala, polyml, z3, veriT, vampire, eprover-ho, naproche, rlwrap, perl, makeDesktopItem }:
+{ lib, stdenv, fetchurl, coreutils, nettools, java, scala, polyml, z3, veriT, vampire, eprover-ho, naproche, rlwrap, perl, makeDesktopItem, isabelle-components, isabelle, symlinkJoin }:
 # nettools needed for hostname
 
 stdenv.mkDerivation rec {
@@ -153,4 +153,29 @@ stdenv.mkDerivation rec {
     maintainers = [ maintainers.jwiegley maintainers.jvanbruegge ];
     platforms = platforms.linux;
   };
+} // {
+  withComponents = f:
+    let
+      base = "$out/${isabelle.dirname}";
+      components = f isabelle-components;
+    in symlinkJoin {
+      name = "isabelle-with-components-${isabelle.version}";
+      paths = [ isabelle ] ++ components;
+
+      postBuild = ''
+        rm $out/bin/*
+
+        cd ${base}
+        rm bin/*
+        cp ${isabelle}/${isabelle.dirname}/bin/* bin/
+        rm etc/components
+        cat ${isabelle}/${isabelle.dirname}/etc/components > etc/components
+
+        export HOME=$TMP
+        bin/isabelle install $out/bin
+        patchShebangs $out/bin
+      '' + lib.concatMapStringsSep "\n" (c: ''
+        echo contrib/${c.pname}-${c.version} >> ${base}/etc/components
+      '') components;
+    };
 }
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index ca05863803df..80c56cad1627 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -32646,6 +32646,7 @@ with pkgs;
     java = openjdk17;
     z3 = z3_4_4_0;
   };
+  isabelle-components = recurseIntoAttrs (callPackage ../applications/science/logic/isabelle/components { });
 
   iprover = callPackage ../applications/science/logic/iprover { };