From 6db348ad34005efce96567082717ccc0756f2675 Mon Sep 17 00:00:00 2001 From: sempiternal-aurora <78790545+sempiternal-aurora@users.noreply.github.com> Date: Mon, 19 Jan 2026 23:40:24 +0800 Subject: [PATCH 1/6] isabelle: fixup and make vscode work Replace the electron binary and remove unused libs, and fixes the platforms. --- pkgs/by-name/is/isabelle/package.nix | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/pkgs/by-name/is/isabelle/package.nix b/pkgs/by-name/is/isabelle/package.nix index c0c9d040127a..1a4fef548cc9 100644 --- a/pkgs/by-name/is/isabelle/package.nix +++ b/pkgs/by-name/is/isabelle/package.nix @@ -19,6 +19,7 @@ isabelle-components, symlinkJoin, fetchhg, + electron, }: let @@ -192,10 +193,15 @@ stdenv.mkDerivation (finalAttrs: { arch=${ if stdenv.hostPlatform.system == "aarch64-linux" then "arm64-linux" else stdenv.hostPlatform.system } - for f in contrib/*/$arch/{z3,nunchaku,spass,zipperposition}; do + for f in contrib/*/$arch/{z3,nunchaku,SPASS,zipperposition}; do patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f"${lib.optionalString stdenv.hostPlatform.isAarch64 " || true"} done patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) contrib/bash_process-*/$arch/bash_process + + ln -sf ${electron}/bin/electron contrib/vscodium-*/*/electron + rm contrib/vscodium-*/*/*.so{,.*} + rm contrib/vscodium-*/*/chrome* + for d in contrib/kodkodi-*/jni/$arch; do patchelf --set-rpath "${ lib.concatStringsSep ":" [ @@ -279,7 +285,12 @@ stdenv.mkDerivation (finalAttrs: { maintainers = [ lib.maintainers.jvanbruegge ]; - platforms = lib.platforms.unix; + platforms = [ + "x86_64-linux" + "aarch64-linux" + "x86_64-darwin" + "aarch64-darwin" + ]; }; passthru.withComponents = From 48d6c3310aabaee019107634b6460d2c5501a931 Mon Sep 17 00:00:00 2001 From: sempiternal-aurora <78790545+sempiternal-aurora@users.noreply.github.com> Date: Tue, 20 Jan 2026 00:20:09 +0800 Subject: [PATCH 2/6] isabelle: fix permission of copied files some files are copied from the nix store and may not be writeable, so set them writeable on copy --- pkgs/by-name/is/isabelle/fix-copied-permissions.patch | 10 ++++++++++ pkgs/by-name/is/isabelle/package.nix | 6 ++++++ 2 files changed, 16 insertions(+) create mode 100644 pkgs/by-name/is/isabelle/fix-copied-permissions.patch diff --git a/pkgs/by-name/is/isabelle/fix-copied-permissions.patch b/pkgs/by-name/is/isabelle/fix-copied-permissions.patch new file mode 100644 index 000000000000..5bfbd583ac34 --- /dev/null +++ b/pkgs/by-name/is/isabelle/fix-copied-permissions.patch @@ -0,0 +1,10 @@ +--- a/src/Pure/System/isabelle_system.scala ++++ b/src/Pure/System/isabelle_system.scala +@@ -214,6 +214,7 @@ object Isabelle_System { + Files.copy(src.toPath, target.toPath, + StandardCopyOption.COPY_ATTRIBUTES, + StandardCopyOption.REPLACE_EXISTING) ++ target.setWritable(true) + } + catch { + case ERROR(msg) => diff --git a/pkgs/by-name/is/isabelle/package.nix b/pkgs/by-name/is/isabelle/package.nix index 1a4fef548cc9..2348d50d9bdf 100644 --- a/pkgs/by-name/is/isabelle/package.nix +++ b/pkgs/by-name/is/isabelle/package.nix @@ -119,6 +119,12 @@ stdenv.mkDerivation (finalAttrs: { net-tools ]; + patches = [ + # Make "isabelle build" work when generating documents + # See: https://github.com/NixOS/nixpkgs/issues/289529 + ./fix-copied-permissions.patch + ]; + propagatedBuildInputs = lib.optionals stdenv.hostPlatform.isDarwin [ procps ]; sourceRoot = "${finalAttrs.dirname}${lib.optionalString stdenv.hostPlatform.isDarwin ".app"}"; From 78dbd6c9b40cc0c471fa8f93850cebb48d37fb01 Mon Sep 17 00:00:00 2001 From: sempiternal-aurora <78790545+sempiternal-aurora@users.noreply.github.com> Date: Tue, 20 Jan 2026 00:22:06 +0800 Subject: [PATCH 3/6] isabelle-linter: change stdenv --- pkgs/by-name/is/isabelle/components/isabelle-linter.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pkgs/by-name/is/isabelle/components/isabelle-linter.nix b/pkgs/by-name/is/isabelle/components/isabelle-linter.nix index 879cf0520bb0..f87f2603f36a 100644 --- a/pkgs/by-name/is/isabelle/components/isabelle-linter.nix +++ b/pkgs/by-name/is/isabelle/components/isabelle-linter.nix @@ -1,11 +1,11 @@ { - stdenv, + stdenvNoCC, lib, fetchFromGitHub, isabelle, }: -stdenv.mkDerivation rec { +stdenvNoCC.mkDerivation rec { pname = "isabelle-linter"; version = "2025-1-1.0.0"; From 2016a39d8d6bf6201b5108ecfc45d37008d85e40 Mon Sep 17 00:00:00 2001 From: sempiternal-aurora <78790545+sempiternal-aurora@users.noreply.github.com> Date: Tue, 20 Jan 2026 00:39:22 +0800 Subject: [PATCH 4/6] isabelle: add sempiternal-aurora as maintainer --- pkgs/by-name/is/isabelle/package.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/pkgs/by-name/is/isabelle/package.nix b/pkgs/by-name/is/isabelle/package.nix index 2348d50d9bdf..b98d7b615d4d 100644 --- a/pkgs/by-name/is/isabelle/package.nix +++ b/pkgs/by-name/is/isabelle/package.nix @@ -290,6 +290,7 @@ stdenv.mkDerivation (finalAttrs: { license = lib.licenses.bsd3; maintainers = [ lib.maintainers.jvanbruegge + lib.maintainers.sempiternal-aurora ]; platforms = [ "x86_64-linux" From 3ca9b73b03a7b7d30569479484178dc515c28e63 Mon Sep 17 00:00:00 2001 From: sempiternal-aurora <78790545+sempiternal-aurora@users.noreply.github.com> Date: Tue, 20 Jan 2026 21:33:42 +0800 Subject: [PATCH 5/6] isaebelle: 2025.1 -> 2025.2 --- pkgs/by-name/is/isabelle/package.nix | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/pkgs/by-name/is/isabelle/package.nix b/pkgs/by-name/is/isabelle/package.nix index b98d7b615d4d..971053bbfe6f 100644 --- a/pkgs/by-name/is/isabelle/package.nix +++ b/pkgs/by-name/is/isabelle/package.nix @@ -88,7 +88,7 @@ let in stdenv.mkDerivation (finalAttrs: { pname = "isabelle"; - version = "2025-1"; + version = "2025-2"; dirname = "Isabelle${finalAttrs.version}"; @@ -96,17 +96,17 @@ stdenv.mkDerivation (finalAttrs: { if stdenv.hostPlatform.isDarwin then fetchurl { url = "https://isabelle.in.tum.de/website-${finalAttrs.dirname}/dist/${finalAttrs.dirname}_macos.tar.gz"; - hash = "sha256-WKlrsXP6oZHy6NTaaQYpddtgE2QGhBZ4uKai61dtQ14="; + hash = "sha256-jxh0luKV8WmVLpRHRa+eSuAMnBzS7UytvPfYmOREkT4="; } else if stdenv.hostPlatform.isx86 then fetchurl { url = "https://isabelle.in.tum.de/website-${finalAttrs.dirname}/dist/${finalAttrs.dirname}_linux.tar.gz"; - hash = "sha256-0SA28X3fIKMV3wZtlJvBxq9MZkI6GevVuSNzgqJ4xQU="; + hash = "sha256-ogpQe8fBJw2L6WqfP77AY0U4d4nS3CxNPfYmDUe/szw="; } else fetchurl { url = "https://isabelle.in.tum.de/website-${finalAttrs.dirname}/dist/${finalAttrs.dirname}_linux_arm.tar.gz"; - hash = "sha256-BUhdK8qhdV2Den+4bbdd9T6MD/BtGpxp+1Axj21NxrI="; + hash = "sha256-ZQqWabSgh2da+zQpTYLe0vBwTUfVgN2e1FzdyfF2S90="; }; nativeBuildInputs = [ java ]; From ea3ab172b725876cd90886799afcb062ef2d1210 Mon Sep 17 00:00:00 2001 From: sempiternal-aurora <78790545+sempiternal-aurora@users.noreply.github.com> Date: Tue, 20 Jan 2026 21:34:18 +0800 Subject: [PATCH 6/6] isabelle: Use nix built csdp and cvc5 Replace the bundled binaries of csdp and cvc5 with ones built by nix, matching the versions expected by isabelle. Also export the isabelle specific packages through passthru for testing --- pkgs/by-name/is/isabelle/package.nix | 84 +++++++++++++++++++--------- 1 file changed, 58 insertions(+), 26 deletions(-) diff --git a/pkgs/by-name/is/isabelle/package.nix b/pkgs/by-name/is/isabelle/package.nix index 971053bbfe6f..c44851d0e337 100644 --- a/pkgs/by-name/is/isabelle/package.nix +++ b/pkgs/by-name/is/isabelle/package.nix @@ -12,6 +12,8 @@ verit, vampire, eprover-ho, + cvc5, + csdp, rlwrap, perl, procps, @@ -85,6 +87,16 @@ let ''; }; + cvc5' = cvc5.overrideAttrs { + version = "1.2.0"; + src = fetchFromGitHub { + owner = "cvc5"; + repo = "cvc5"; + tag = "cvc5-1.2.0"; + hash = "sha256-Um1x+XgQ5yWSoqtx1ZWbVAnNET2C4GVasIbn0eNfico="; + }; + }; + in stdenv.mkDerivation (finalAttrs: { pname = "isabelle"; @@ -117,6 +129,8 @@ stdenv.mkDerivation (finalAttrs: { vampire' eprover-ho net-tools + cvc5' + csdp ]; patches = [ @@ -158,6 +172,17 @@ stdenv.mkDerivation (finalAttrs: { VAMPIRE_EXTRA_OPTIONS="--mode casc" EOF + cat >contrib/cvc5-*/etc/settings <contrib/csdp-*/etc/settings <contrib/polyml-*/etc/settings <>etc/settings - for comp in contrib/jdk* contrib/polyml-* contrib/verit-* contrib/vampire-* contrib/e-*; do + for comp in contrib/jdk* contrib/polyml-* contrib/verit-* contrib/vampire-* \ + contrib/e-* contrib/cvc5-* contrib/csdp-*; do rm -rf $comp/${if stdenv.hostPlatform.isx86 then "x86" else "arm"}* done rm -rf contrib/*/src @@ -300,32 +326,38 @@ stdenv.mkDerivation (finalAttrs: { ]; }; - 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 ] ++ (map (c: c.override { inherit isabelle; }) components); + passthru = { + vampire = vampire'; + polyml = polyml'; + cvc5 = cvc5'; + sha1 = sha1; + withComponents = + f: + let + isabelle = finalAttrs.finalPackage; + base = "$out/${isabelle.dirname}"; + components = f isabelle-components; + in + symlinkJoin { + name = "isabelle-with-components-${isabelle.version}"; + paths = [ isabelle ] ++ (map (c: c.override { inherit isabelle; }) components); - postBuild = '' - rm $out/bin/* + 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 + 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; - }; + 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; + }; + }; })