From d5299641bb35b3ead5db880a02a27d1665587f5e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Sat, 3 Dec 2022 16:37:09 +0000 Subject: [PATCH 1/3] isabelle: make withComponents function use finalAttrs Before this change ``` (isabelle.overrideAttrs ( /* whatever */ )).withComponents (/* whatever */) ``` would ignore the `overrideAttrs` and use the normal `isabelle` derivation instead. This commit fixes this --- pkgs/applications/science/logic/isabelle/default.nix | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix index 1bb7ede6da7b..7a796cefe441 100644 --- a/pkgs/applications/science/logic/isabelle/default.nix +++ b/pkgs/applications/science/logic/isabelle/default.nix @@ -15,7 +15,6 @@ , perl , makeDesktopItem , isabelle-components -, isabelle , symlinkJoin , fetchhg }: @@ -46,7 +45,7 @@ let cp libsha1.so $out/lib/ ''; }; -in stdenv.mkDerivation rec { +in stdenv.mkDerivation (finalAttrs: rec { pname = "isabelle"; version = "2022"; @@ -219,14 +218,15 @@ in stdenv.mkDerivation rec { maintainers = [ maintainers.jwiegley maintainers.jvanbruegge ]; platforms = platforms.unix; }; -} // { - withComponents = f: + + passthru.withComponents = f: let + isabelle = finalAttrs.finalPackage; base = "$out/${isabelle.dirname}"; components = f isabelle-components; in symlinkJoin { name = "isabelle-with-components-${isabelle.version}"; - paths = [ isabelle ] ++ components; + paths = [ isabelle ] ++ (builtins.map (c: c.override { inherit isabelle; }) components); postBuild = '' rm $out/bin/* @@ -244,4 +244,4 @@ in stdenv.mkDerivation rec { echo contrib/${c.pname}-${c.version} >> ${base}/etc/components '') components; }; -} +}) From 26c369214e6f76216ac3ef6ed7dddfaad486ab3e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Sat, 3 Dec 2022 17:03:20 +0000 Subject: [PATCH 2/3] isabelle: use prebuilt z3 Isabelle requires this specific version of z3 which is being removed from nixpkgs due to requiring python2 for its build. We can work around this by patching the distributed binary --- .../science/logic/isabelle/default.nix | 22 +++++++------------ pkgs/top-level/all-packages.nix | 8 ------- 2 files changed, 8 insertions(+), 22 deletions(-) diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix index 7a796cefe441..dce369572396 100644 --- a/pkgs/applications/science/logic/isabelle/default.nix +++ b/pkgs/applications/science/logic/isabelle/default.nix @@ -6,7 +6,6 @@ , java , scala_3 , polyml -, z3 , veriT , vampire , eprover-ho @@ -67,11 +66,14 @@ in stdenv.mkDerivation (finalAttrs: rec { nativeBuildInputs = [ java ]; - buildInputs = [ polyml z3 veriT vampire eprover-ho nettools ] + buildInputs = [ polyml veriT vampire eprover-ho nettools ] ++ lib.optionals (!stdenv.isDarwin) [ java ]; sourceRoot = dirname; + doCheck = true; + checkPhase = "bin/isabelle build -v HOL-SMT_Examples"; + postUnpack = lib.optionalString stdenv.isDarwin '' mv $sourceRoot.app $sourceRoot ''; @@ -79,13 +81,6 @@ in stdenv.mkDerivation (finalAttrs: rec { postPatch = '' patchShebangs lib/Tools/ bin/ - cat >contrib/z3*/etc/settings <contrib/verit-*/etc/settings <>etc/settings - for comp in contrib/jdk* contrib/polyml-* contrib/z3-* contrib/verit-* contrib/vampire-* contrib/e-*; do + for comp in contrib/jdk* contrib/polyml-* contrib/verit-* contrib/vampire-* contrib/e-*; do rm -rf $comp/x86* done @@ -142,15 +137,14 @@ in stdenv.mkDerivation (finalAttrs: rec { --replace 'ISABELLE_APPLE_PLATFORM64=arm64-darwin' "" '' + lib.optionalString stdenv.isLinux '' arch=${if stdenv.hostPlatform.system == "x86_64-linux" then "x86_64-linux" else "x86-linux"} - for f in contrib/*/$arch/{bash_process,epclextract,nunchaku,SPASS,zipperposition}; do - patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f" - done - for f in contrib/*/platform_$arch/{bash_process,epclextract,nunchaku,SPASS,zipperposition}; do + for f in contrib/*/$arch/{z3,epclextract,nunchaku,SPASS,zipperposition}; do patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f" done + patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) contrib/bash_process-*/platform_$arch/bash_process for d in contrib/kodkodi-*/jni/$arch; do patchelf --set-rpath "${lib.concatStringsSep ":" [ "${java}/lib/openjdk/lib/server" "${stdenv.cc.cc.lib}/lib" ]}" $d/*.so done + patchelf --set-rpath "${stdenv.cc.cc.lib}/lib" contrib/z3-*/$arch/z3 ''; buildPhase = '' diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 5686aeb6db2e..fa2722a8436c 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -35911,14 +35911,6 @@ with pkgs; }); java = openjdk17; - 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 { }); From 698c7342b7c3a9f33025de6a43a37851c1feeb12 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Tue, 6 Dec 2022 15:55:35 +0000 Subject: [PATCH 3/3] isabelle: fix build on MacOS --- pkgs/applications/science/logic/isabelle/default.nix | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix index dce369572396..d2326d2d4d0e 100644 --- a/pkgs/applications/science/logic/isabelle/default.nix +++ b/pkgs/applications/science/logic/isabelle/default.nix @@ -69,13 +69,14 @@ in stdenv.mkDerivation (finalAttrs: rec { buildInputs = [ polyml veriT vampire eprover-ho nettools ] ++ lib.optionals (!stdenv.isDarwin) [ java ]; - sourceRoot = dirname; + sourceRoot = "${dirname}${lib.optionalString stdenv.isDarwin ".app"}"; doCheck = true; checkPhase = "bin/isabelle build -v HOL-SMT_Examples"; postUnpack = lib.optionalString stdenv.isDarwin '' - mv $sourceRoot.app $sourceRoot + mv $sourceRoot ${dirname} + sourceRoot=${dirname} ''; postPatch = ''