Merge pull request #159997 from jvanbruegge/isabelle-linter

pkgs/applications/science/logic/isabelle/components/default.nix

@@ -0,0 +1,5 @@
+{ callPackage }:
+
+{
+  isabelle-linter = callPackage ./isabelle-linter.nix {};
+}

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;
+  };
+}

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
+''

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;
+    };
 }

pkgs/top-level/all-packages.nix

@@ -32733,6 +32733,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 { };