Merge staging-next into staging

2026-03-24 12:18:19 +00:00
parent b76d124c05 e7a56f178b
commit b5cc7da1e3
79 changed files with 1374 additions and 568 deletions
@@ -13974,13 +13974,6 @@
    githubId = 788813;
    name = "Bryan Gardiner";
  };
-  khushraj = {
-    email = "khushraj.rathod@gmail.com";
-    github = "khrj";
-    githubId = 44947946;
-    name = "Khushraj Rathod";
-    keys = [ { fingerprint = "1988 3FD8 EA2E B4EC 0A93  1E22 B77B 2A40 E770 2F19"; } ];
-  };
  kiara = {
    name = "kiara";
    email = "cinereal@riseup.net";
@@ -18708,6 +18701,12 @@
    githubId = 23151917;
    name = "nadir-ishiguro";
  };
+  nadja-y = {
+    email = "git@njy.dev";
+    github = "nadja-y";
+    githubId = 255079535;
+    name = "Nadja Yang";
+  };
  nadrieril = {
    email = "nadrieril@gmail.com";
    github = "Nadrieril";
@@ -189,7 +189,7 @@

 - [Improved File Manager (IFM)](https://github.com/misterunknown/ifm), a single-file web-based file manager. Available as [services.ifm](options.html#opt-services.ifm.enable).

- [OpenGFW](https://github.com/apernet/OpenGFW), an implementation of the Great Firewall on Linux. Available as [services.opengfw](#opt-services.opengfw.enable).
+- [OpenGFW](https://github.com/apernet/OpenGFW), an implementation of the Great Firewall on Linux. Available as `services.opengfw`.

 - [Rathole](https://github.com/rapiz1/rathole), a lightweight and high-performance reverse proxy for NAT traversal. Available as [services.rathole](#opt-services.rathole.enable).

@@ -93,6 +93,7 @@
   - It may introduce unexpected breakage or degrade performance without clear benefit,
   - It is difficult to manage user expectations, especially since the implications of enabling it are not always obvious,
   - and as multiple contributors have noted, it is often more of a “grab bag” of settings than a cohesive security policy.
+   - See [NixOS Hardening](https://wiki.nixos.org/wiki/NixOS_Hardening) wiki page for hardening options.

 - `services.crabfit` was removed because its upstream packages are unmaintained and insecure.

@@ -223,6 +224,8 @@ See <https://github.com/NixOS/nixpkgs/issues/481673>.

 - `lunarvim` package has been removed, as it was abandoned upstream and relied on an old version of `neovim` to work properly.

+- `opengfw` package and `services.opengfw` module have been removed as the upstream GitHub repository and website have been shut down.
+
 ## Other Notable Changes {#sec-release-26.05-notable-changes}

 <!-- To avoid merge conflicts, consider adding your item at an arbitrary place in the list instead. -->
@@ -1329,7 +1329,6 @@
  ./services/networking/oink.nix
  ./services/networking/onedrive.nix
  ./services/networking/openconnect.nix
-  ./services/networking/opengfw.nix
  ./services/networking/openvpn.nix
  ./services/networking/opkssh/opkssh.nix
  ./services/networking/ostinato.nix
@@ -452,6 +452,10 @@ in
    (mkRemovedOptionModule [ "services" "gateone" ] ''
      The gateone module was removed since the package was removed alongside much other obsolete python 2.
    '')
+    (mkRemovedOptionModule [ "services" "opengfw" ] ''
+      The opengfw package and services.opengfw module have been removed since the upstream
+      GitHub repository and website have been shut down.
+    '')
    (mkRemovedOptionModule [ "virtualisation" "lxd" ] ''
      LXD has been removed from NixOS due to lack of Nixpkgs maintenance.
      Consider migrating or switching to Incus, or remove from your configuration.
@@ -204,7 +204,12 @@ in
          RuntimeDirectory = "radicle-ci-broker";
          WorkingDirectory = "/run/radicle-ci-broker";

-          BindReadOnlyPaths = config.systemd.services.radicle-node.serviceConfig.BindReadOnlyPaths;
+          ImportCredential = config.systemd.services.radicle-node.serviceConfig.ImportCredential or [ ];
+          LoadCredential = config.systemd.services.radicle-node.serviceConfig.LoadCredential or [ ];
+
+          BindReadOnlyPaths = config.systemd.services.radicle-node.serviceConfig.BindReadOnlyPaths ++ [
+            "/run/credentials/radicle-ci-broker.service/xyz.radicle.node.secret:/var/lib/radicle/keys/radicle"
+          ];
          ReadWritePaths = [ RAD_HOME ];

          ExecStart = "${lib.getExe' cfg.package "cib"} --config ${configFile} process-events";
@@ -9,6 +9,36 @@ let

  cfg = config.services.litellm;
  settingsFormat = pkgs.formats.yaml { };
+
+  tiktokenEncodings = {
+    cl100k_base = {
+      url = "https://openaipublic.blob.core.windows.net/encodings/cl100k_base.tiktoken";
+      hash = "sha256-Ijkht27pm96ZW3/3OFE+7xAPtR0YyTWXoRO8/+hlsqc=";
+    };
+  };
+
+  tiktokenCacheEntries = lib.mapAttrsToList (
+    _: encoding:
+    let
+      cacheKey = builtins.hashString "sha1" encoding.url;
+      sourceFile = pkgs.fetchurl {
+        inherit (encoding) url hash;
+      };
+    in
+    {
+      inherit cacheKey sourceFile;
+    }
+  ) tiktokenEncodings;
+
+  seedTiktokenCacheScript = pkgs.writeShellScript "litellm-seed-tiktoken-cache" ''
+    set -eu
+
+    mkdir -p "$CUSTOM_TIKTOKEN_CACHE_DIR"
+
+    ${lib.concatMapStringsSep "\n" (entry: ''
+      ln -sf ${entry.sourceFile} "$CUSTOM_TIKTOKEN_CACHE_DIR/${entry.cacheKey}"
+    '') tiktokenCacheEntries}
+  '';
 in
 {
  options = {
@@ -132,22 +162,50 @@ in
  };

  config = lib.mkIf cfg.enable {
+    systemd.tmpfiles.rules = [
+      "d '${cfg.stateDir}/ui' 0700 - - - -"
+      "d '${cfg.stateDir}/tiktoken-cache' 0700 - - - -"
+    ];
+
    systemd.services.litellm = {
      description = "LLM Gateway to provide model access, fallbacks and spend tracking across 100+ LLMs.";
      wantedBy = [ "multi-user.target" ];
      after = [ "network.target" ];

-      environment = cfg.environment;
+      environment = {
+        # LiteLLM will try to "restructure" (rewrite) its packaged UI files on startup
+        # to support extensionless routes (e.g. `/ui/login`). In Nix builds the packaged
+        # UI lives in the read-only Nix store, so point it at a writable runtime path.
+        LITELLM_NON_ROOT = "true";
+        LITELLM_UI_PATH = "${cfg.stateDir}/ui";
+
+        # LiteLLM sets TIKTOKEN_CACHE_DIR internally from this variable.
+        CUSTOM_TIKTOKEN_CACHE_DIR = "${cfg.stateDir}/tiktoken-cache";
+      }
+      // cfg.environment;

      serviceConfig =
        let
          configFile = settingsFormat.generate "config.yaml" cfg.settings;
        in
        {
+          ExecStartPre = [
+            # Seed tokenizer cache with fixed-output files so startup does not
+            # depend on outbound network access.
+            seedTiktokenCacheScript
+
+            # LiteLLM may rewrite/copy UI assets with read-only permissions
+            # during previous runs; normalize writability on each start.
+            "${pkgs.runtimeShell} -euc 'chmod -R u+rwX ${cfg.stateDir}/ui'"
+          ];
          ExecStart = "${lib.getExe cfg.package} --host \"${cfg.host}\" --port ${toString cfg.port} --config ${configFile}";
          EnvironmentFile = lib.optional (cfg.environmentFile != null) cfg.environmentFile;
          WorkingDirectory = cfg.stateDir;
-          StateDirectory = "litellm";
+          StateDirectory = [
+            "litellm"
+            "litellm/ui"
+            "litellm/tiktoken-cache"
+          ];
          RuntimeDirectory = "litellm";
          RuntimeDirectoryMode = "0755";
          PrivateTmp = true;
@@ -438,6 +438,7 @@ in
  );

  meta.maintainers = with lib.maintainers; [
+    defelo
    julm
    lorenzleutgeb
  ];
@@ -1,414 +0,0 @@
-{
-  lib,
-  pkgs,
-  config,
-  ...
-}:
-let
-  inherit (lib)
-    mkOption
-    types
-    mkIf
-    optionalString
-    ;
-  cfg = config.services.opengfw;
-in
-{
-  options.services.opengfw = {
-    enable = lib.mkEnableOption ''
-      OpenGFW, A flexible, easy-to-use, open source implementation of GFW on Linux
-    '';
-
-    package = lib.mkPackageOption pkgs "opengfw" { default = "opengfw"; };
-
-    user = mkOption {
-      default = "opengfw";
-      type = types.singleLineStr;
-      description = "Username of the OpenGFW user.";
-    };
-
-    dir = mkOption {
-      default = "/var/lib/opengfw";
-      type = types.singleLineStr;
-      description = ''
-        Working directory of the OpenGFW service and home of `opengfw.user`.
-      '';
-    };
-
-    logFile = mkOption {
-      default = null;
-      type = types.nullOr types.path;
-      example = "/var/lib/opengfw/opengfw.log";
-      description = ''
-        File to write the output to instead of systemd.
-      '';
-    };
-
-    logFormat = mkOption {
-      description = ''
-        Format of the logs. [logFormatMap](https://github.com/apernet/OpenGFW/blob/d7737e92117a11c9a6100d53019fac3b9d724fe3/cmd/root.go#L62)
-      '';
-      default = "json";
-      example = "console";
-      type = types.enum [
-        "json"
-        "console"
-      ];
-    };
-
-    pcapReplay = mkOption {
-      default = null;
-      example = "./opengfw.pcap";
-      type = types.nullOr types.path;
-      description = ''
-        Path to PCAP replay file.
-        In pcap mode, none of the actions in the rules have any effect.
-        This mode is mainly for debugging.
-      '';
-    };
-
-    logLevel = mkOption {
-      description = ''
-        Level of the logs. [logLevelMap](https://github.com/apernet/OpenGFW/blob/d7737e92117a11c9a6100d53019fac3b9d724fe3/cmd/root.go#L55)
-      '';
-      default = "info";
-      example = "warn";
-      type = types.enum [
-        "debug"
-        "info"
-        "warn"
-        "error"
-      ];
-    };
-
-    rulesFile = mkOption {
-      default = null;
-      type = types.nullOr types.path;
-      description = ''
-        Path to file containing OpenGFW rules.
-      '';
-    };
-
-    settingsFile = mkOption {
-      default = null;
-      type = types.nullOr types.path;
-      description = ''
-        Path to file containing OpenGFW settings.
-      '';
-    };
-
-    settings = mkOption {
-      default = null;
-      description = ''
-        Settings passed to OpenGFW. [Example config](https://gfw.dev/docs/build-run/#config-example)
-      '';
-      type = types.nullOr (
-        types.submodule {
-          options = {
-            replay = mkOption {
-              description = ''
-                PCAP replay settings.
-              '';
-              default = { };
-              type = types.submodule {
-                options = {
-                  realtime = mkOption {
-                    description = ''
-                      Whether the packets in the PCAP file should be replayed in "real time" (instead of as fast as possible).
-                    '';
-                    default = false;
-                    example = true;
-                    type = types.bool;
-                  };
-                };
-              };
-            };
-
-            io = mkOption {
-              description = ''
-                IO settings.
-              '';
-              default = { };
-              type = types.submodule {
-                options = {
-                  queueSize = mkOption {
-                    description = "IO queue size.";
-                    type = types.int;
-                    default = 1024;
-                    example = 2048;
-                  };
-                  local = mkOption {
-                    description = ''
-                      Set to false if you want to run OpenGFW on FORWARD chain. (e.g. on a router)
-                    '';
-                    type = types.bool;
-                    default = true;
-                    example = false;
-                  };
-                  rst = mkOption {
-                    description = ''
-                      Set to true if you want to send RST for blocked TCP connections, needs `local = false`.
-                    '';
-                    type = types.bool;
-                    default = !cfg.settings.io.local;
-                    defaultText = "`!config.services.opengfw.settings.io.local`";
-                    example = false;
-                  };
-                  rcvBuf = mkOption {
-                    description = "Netlink receive buffer size.";
-                    type = types.int;
-                    default = 4194304;
-                    example = 2097152;
-                  };
-                  sndBuf = mkOption {
-                    description = "Netlink send buffer size.";
-                    type = types.int;
-                    default = 4194304;
-                    example = 2097152;
-                  };
-                };
-              };
-            };
-            ruleset = mkOption {
-              description = ''
-                The path to load specific local geoip/geosite db files.
-                If not set, they will be automatically downloaded from [Loyalsoldier/v2ray-rules-dat](https://github.com/Loyalsoldier/v2ray-rules-dat).
-              '';
-              default = { };
-              type = types.submodule {
-                options = {
-                  geoip = mkOption {
-                    description = "Path to `geoip.dat`.";
-                    default = null;
-                    type = types.nullOr types.path;
-                  };
-                  geosite = mkOption {
-                    description = "Path to `geosite.dat`.";
-                    default = null;
-                    type = types.nullOr types.path;
-                  };
-                };
-              };
-            };
-            workers = mkOption {
-              default = { };
-              description = "Worker settings.";
-              type = types.submodule {
-                options = {
-                  count = mkOption {
-                    type = types.int;
-                    description = ''
-                      Number of workers.
-                      Recommended to be no more than the number of CPU cores
-                    '';
-                    default = 4;
-                    example = 8;
-                  };
-                  queueSize = mkOption {
-                    type = types.int;
-                    description = "Worker queue size.";
-                    default = 16;
-                    example = 32;
-                  };
-                  tcpMaxBufferedPagesTotal = mkOption {
-                    type = types.int;
-                    description = ''
-                      TCP max total buffered pages.
-                    '';
-                    default = 4096;
-                    example = 8192;
-                  };
-                  tcpMaxBufferedPagesPerConn = mkOption {
-                    type = types.int;
-                    description = ''
-                      TCP max total bufferd pages per connection.
-                    '';
-                    default = 64;
-                    example = 128;
-                  };
-                  tcpTimeout = mkOption {
-                    type = types.str;
-                    description = ''
-                      How long a connection is considered dead when no data is being transferred.
-                      Dead connections are purged from TCP reassembly pools once per minute.
-                    '';
-                    default = "10m";
-                    example = "5m";
-                  };
-                  udpMaxStreams = mkOption {
-                    type = types.int;
-                    description = "UDP max streams.";
-                    default = 4096;
-                    example = 8192;
-                  };
-                };
-              };
-            };
-          };
-        }
-      );
-    };
-
-    rules = mkOption {
-      default = [ ];
-      description = ''
-        Rules passed to OpenGFW. [Example rules](https://gfw.dev/docs/rules)
-      '';
-      type = types.listOf (
-        types.submodule {
-          options = {
-            name = mkOption {
-              description = "Name of the rule.";
-              example = "block google dns";
-              type = types.singleLineStr;
-            };
-
-            action = mkOption {
-              description = ''
-                Action of the rule. [Supported actions](https://gfw.dev/docs/rules#supported-actions)
-              '';
-              default = "allow";
-              example = "block";
-              type = types.enum [
-                "allow"
-                "block"
-                "drop"
-                "modify"
-              ];
-            };
-
-            log = mkOption {
-              description = "Whether to enable logging for the rule.";
-              default = true;
-              example = false;
-              type = types.bool;
-            };
-
-            expr = mkOption {
-              description = ''
-                [Expr Language](https://expr-lang.org/docs/language-definition) expression using [analyzers](https://gfw.dev/docs/analyzers) and [functions](https://gfw.dev/docs/functions).
-              '';
-              type = types.str;
-              example = ''dns != nil && dns.qr && any(dns.questions, {.name endsWith "google.com"})'';
-            };
-
-            modifier = mkOption {
-              default = null;
-              description = ''
-                Modification of specified packets when using the `modify` action. [Available modifiers](https://github.com/apernet/OpenGFW/tree/master/modifier)
-              '';
-              type = types.nullOr (
-                types.submodule {
-                  options = {
-                    name = mkOption {
-                      description = "Name of the modifier.";
-                      type = types.singleLineStr;
-                      example = "dns";
-                    };
-
-                    args = mkOption {
-                      description = "Arguments passed to the modifier.";
-                      type = types.attrs;
-                      example = {
-                        a = "0.0.0.0";
-                        aaaa = "::";
-                      };
-                    };
-                  };
-                }
-              );
-            };
-          };
-        }
-      );
-
-      example = [
-        {
-          name = "block v2ex http";
-          action = "block";
-          expr = ''string(http?.req?.headers?.host) endsWith "v2ex.com"'';
-        }
-        {
-          name = "block google socks";
-          action = "block";
-          expr = ''string(socks?.req?.addr) endsWith "google.com" && socks?.req?.port == 80'';
-        }
-        {
-          name = "v2ex dns poisoning";
-          action = "modify";
-          modifier = {
-            name = "dns";
-            args = {
-              a = "0.0.0.0";
-              aaaa = "::";
-            };
-          };
-          expr = ''dns != nil && dns.qr && any(dns.questions, {.name endsWith "v2ex.com"})'';
-        }
-      ];
-    };
-  };
-
-  config =
-    let
-      format = pkgs.formats.yaml { };
-
-      settings =
-        if cfg.settings != null then
-          format.generate "opengfw-config.yaml" cfg.settings
-        else
-          cfg.settingsFile;
-      rules = if cfg.rules != [ ] then format.generate "opengfw-rules.yaml" cfg.rules else cfg.rulesFile;
-    in
-    mkIf cfg.enable {
-      security.wrappers.OpenGFW = {
-        owner = cfg.user;
-        group = cfg.user;
-        capabilities = "cap_net_admin+ep";
-        source = "${cfg.package}/bin/OpenGFW";
-      };
-
-      systemd.services.opengfw = {
-        description = "OpenGFW";
-        wantedBy = [ "multi-user.target" ];
-        after = [ "network.target" ];
-        path = with pkgs; [ iptables ];
-
-        preStart = ''
-          ${optionalString (rules != null) "ln -sf ${rules} rules.yaml"}
-          ${optionalString (settings != null) "ln -sf ${settings} config.yaml"}
-        '';
-
-        script = ''
-          ${config.security.wrapperDir}/OpenGFW \
-            -f ${cfg.logFormat} \
-            -l ${cfg.logLevel} \
-            ${optionalString (cfg.pcapReplay != null) "-p ${cfg.pcapReplay}"} \
-            -c config.yaml \
-            rules.yaml
-        '';
-
-        serviceConfig = rec {
-          WorkingDirectory = cfg.dir;
-          ExecReload = "${lib.getExe' pkgs.coreutils "kill"} -HUP $MAINPID";
-          Restart = "always";
-          User = cfg.user;
-          StandardOutput = mkIf (cfg.logFile != null) "append:${cfg.logFile}";
-          StandardError = StandardOutput;
-        };
-      };
-
-      users = {
-        groups.${cfg.user} = { };
-        users.${cfg.user} = {
-          description = "opengfw user";
-          isSystemUser = true;
-          group = cfg.user;
-          home = cfg.dir;
-          createHome = true;
-          homeMode = "750";
-        };
-      };
-    };
-  meta.maintainers = with lib.maintainers; [ eum3l ];
-}
@@ -132,12 +132,6 @@ in
  ###### implementation

  config = mkIf config.console.enable {
-    assertions = [
-      {
-        assertion = cfg.loginOptions != null -> cfg.autologinUser == null;
-        message = "services.getty.autoLoginUser has no effect when services.getty.loginOptions is set.";
-      }
-    ];
    # Note: this is set here rather than up there so that changing
    # nixos.label would not rebuild manual pages
    services.getty.greetingLine = mkDefault ''<<< Welcome to ${config.system.nixos.distroName} ${config.system.nixos.label} (\m) - \l >>>'';
@@ -90,7 +90,7 @@ in

      package = mkPackageOption pkgs "kmscon" { };

-      hwRender = mkEnableOption "hardware acceleration + DRM backend";
+      hwRender = mkEnableOption "3D hardware acceleration to render the console";

      fonts = mkOption {
        description = "Fonts used by kmscon, in order of priority.";
@@ -168,7 +168,6 @@ in
            "--"
            loginScript
          ]
-
        ))
      ];

@@ -194,14 +193,10 @@ in
            ) config.services.xserver.xkb
          )
        );
-        render =
-          if cfg.hwRender then
-            [
-              "drm"
-              "hwaccel"
-            ]
-          else
-            [ "no-drm" ];
+        render = optionals cfg.hwRender [
+          "drm"
+          "hwaccel"
+        ];
        fonts =
          optional (cfg.fonts != null)
            "font-name=${lib.concatMapStringsSep ", " (f: f.name) cfg.fonts}";
@@ -72,6 +72,9 @@ in
      ];
    };

+  interactive.sshBackdoor.enable = true;
+  interactive.defaults.virtualisation.graphics = false;
+
  testScript = ''
    import json
    import time
@@ -65,6 +65,7 @@ in

  meta = with pkgs.lib.maintainers; {
    maintainers = [
+      defelo
      julm
      lorenzleutgeb
    ];
@@ -1076,11 +1076,11 @@
    "vendorHash": "sha256-F1AuO/dkldEDRvkwrbq2EjByxjg3K2rohZAM4DzKPUw="
  },
  "pagerduty_pagerduty": {
-    "hash": "sha256-y4lh5jw9bENgVG181lJOsJx3RaR8m+tQnfvY1ONi8kQ=",
+    "hash": "sha256-JiMc7HIowWM0CIWl8NZjmZs8Y/jYPPfsxDGNmgH2S8o=",
    "homepage": "https://registry.terraform.io/providers/PagerDuty/pagerduty",
    "owner": "PagerDuty",
    "repo": "terraform-provider-pagerduty",
-    "rev": "v3.31.4",
+    "rev": "v3.32.0",
    "spdx": "MPL-2.0",
    "vendorHash": null
  },
@@ -0,0 +1,326 @@
+# buildLakePackage: build Lean 4 projects that use the Lake build system.
+#
+# Dependencies can be provided in two ways:
+#   - `leanDeps`: already-packaged Lean libraries from leanPackages.
+#     These are injected into LEAN_PATH via setup hooks and propagated
+#     transitively, similar to Haskell's libraryHaskellDepends.
+#   - `lakeHash`: SRI hash for a fetchLakeDeps FOD that clones git
+#     dependencies listed in lake-manifest.json (like buildGoModule's
+#     vendorHash).  Not needed when all deps are in `leanDeps`.
+#
+# Library output layout:
+#   $out/                         Package root (source + build artifacts)
+#   $out/lakefile.{lean,toml}     Lake package configuration
+#   $out/lean-toolchain           Lean version pin
+#   $out/.lake/build/lib/lean/    Compiled .olean/.ilean files
+#   $out/.lake/build/ir/          Compiled C/object files
+#   $out/nix-support/setup-hook   LEAN_PATH propagation hook
+{
+  lib,
+  stdenv,
+  lean4,
+  gitMinimal,
+  cacert,
+  jq,
+  lndir,
+  stdenvNoCC,
+}:
+
+let
+  fetchLakeDeps = import ./fetch-lake-deps.nix {
+    inherit
+      lib
+      stdenvNoCC
+      gitMinimal
+      cacert
+      jq
+      ;
+  };
+in
+
+lib.extendMkDerivation {
+  constructDrv = stdenv.mkDerivation;
+  excludeDrvArgNames = [
+    "lakeHash"
+    "lakeDeps"
+    "leanDeps"
+    "buildTargets"
+    "isLibrary"
+    "leanPackageName"
+    "overrideLakeDepsAttrs"
+  ];
+  extendDrvArgs =
+    finalAttrs:
+    {
+      nativeBuildInputs ? [ ],
+      passthru ? { },
+
+      # SRI hash for the Lake dependencies FOD.
+      # Set to null if the project has no external dependencies
+      # (or all deps are provided via leanDeps).
+      lakeHash ? null,
+
+      # Pre-built Lake dependencies derivation (overrides lakeHash).
+      lakeDeps ? null,
+
+      # Already-packaged Lean libraries from nixpkgs.
+      # These are added to LEAN_PATH (via setup hook) and propagated
+      # transitively.  Each must be a buildLakePackage output with
+      # .olean files under $out/.lake/build/lib/lean/.
+      leanDeps ? [ ],
+
+      # Lean package name as declared in lakefile.lean/toml.
+      # Defaults to pname.
+      leanPackageName ? finalAttrs.pname,
+
+      # Lake build targets.  Empty list means the default target.
+      buildTargets ? [ ],
+
+      # Whether this is a library (install full package tree with
+      # .olean/.ilean files) or an executable (install binaries only).
+      isLibrary ? true,
+
+      # Override attributes of the lakeDeps derivation.
+      overrideLakeDepsAttrs ? (finalAttrs: previousAttrs: { }),
+
+      meta ? { },
+
+      ...
+    }@args:
+    let
+      lakeDeps' = args.lakeDeps or null;
+      lakeHash = args.lakeHash or null;
+      leanDeps = args.leanDeps or [ ];
+      overrideLakeDepsAttrs = args.overrideLakeDepsAttrs or (_: _: { });
+      buildTargets = args.buildTargets or [ ];
+      isLibrary = args.isLibrary or true;
+      leanPackageName = args.leanPackageName or finalAttrs.pname;
+
+      computedLakeDeps =
+        if lakeDeps' != null then
+          lakeDeps'
+        else if lakeHash == null then
+          null
+        else
+          (fetchLakeDeps {
+            name = finalAttrs.name or "${finalAttrs.pname}-${finalAttrs.version}";
+            inherit (finalAttrs) src;
+            hash = lakeHash;
+            sourceRoot = finalAttrs.sourceRoot or "";
+            patches = finalAttrs.patches or [ ];
+            prePatch = finalAttrs.prePatch or "";
+            postPatch = finalAttrs.postPatch or "";
+            excludePackages = builtins.map (dep: dep.passthru.lakePackageName or dep.pname) allLeanDeps;
+          }).overrideAttrs
+            (lib.toExtension overrideLakeDepsAttrs);
+
+      # Transitively collect all Lean dependencies.  Each buildLakePackage
+      # library stores its own transitive closure in passthru.allLeanDeps,
+      # so this flattens the entire dependency DAG.
+      allLeanDeps = lib.unique (
+        builtins.concatMap (dep: [ dep ] ++ (dep.passthru.allLeanDeps or [ ])) leanDeps
+      );
+    in
+    {
+      strictDeps = true;
+
+      nativeBuildInputs = nativeBuildInputs ++ [
+        lean4
+        gitMinimal
+        jq
+        lndir
+      ];
+
+      # Propagate so downstream packages get transitive LEAN_PATH entries
+      # via each dependency's nix-support/setup-hook.
+      propagatedBuildInputs = lib.optionals isLibrary leanDeps;
+
+      # Executables only need deps at build time.
+      buildInputs = lib.optionals (!isLibrary) leanDeps;
+
+      configurePhase =
+        args.configurePhase or ''
+          runHook preConfigure
+
+          export HOME="$TMPDIR"
+
+          # Disable Lake cloud caching and Reservoir lookups
+          export LAKE_NO_CACHE=1
+          export RESERVOIR_API_URL=""
+
+          # Point leanc at the nix-provided C compiler
+          export LEAN_CC="${stdenv.cc}/bin/cc"
+
+          # Validate that the lean-toolchain file (if present) matches the
+          # Lean toolchain we are building against.  Mismatches between the
+          # toolchain version and the compiler produce confusing errors, so
+          # fail early with a clear message.
+          leanVersion="${lean4.version}"
+          if [ -f lean-toolchain ]; then
+            toolchainVersion=$(sed -n 's/^.*:v\([0-9][0-9.]*\).*/\1/p' lean-toolchain)
+            if [ -n "$toolchainVersion" ] && [ "$toolchainVersion" != "$leanVersion" ]; then
+              echo "buildLakePackage: lean-toolchain requests v$toolchainVersion but lean4 is v$leanVersion" >&2
+              echo "buildLakePackage: update the package or use a matching lean4 version" >&2
+              exit 1
+            fi
+          fi
+
+          ${lib.concatStringsSep "\n" (
+            builtins.map (
+              dep:
+              let
+                name = dep.passthru.lakePackageName or dep.pname;
+              in
+              ''
+                # Fail fast if nix-packaged dep "${name}" was built against a
+                # different Lean version.  This avoids wasting build time when
+                # the package set is mid-update (e.g. lean4 bumped but a dep
+                # has not been updated yet).
+                if [ -f "${dep}/lean-toolchain" ]; then
+                  depToolchain=$(sed -n 's/^.*:v\([0-9][0-9.]*\).*/\1/p' "${dep}/lean-toolchain")
+                  if [ -n "$depToolchain" ] && [ "$depToolchain" != "$leanVersion" ]; then
+                    echo "buildLakePackage: dependency ${name} was built with Lean v$depToolchain but lean4 is v$leanVersion" >&2
+                    echo "buildLakePackage: update ${name} first, or override lean4 in leanPackages" >&2
+                    exit 1
+                  fi
+                fi
+              ''
+            ) allLeanDeps
+          )}
+
+          if [ -n "''${LEAN_PATH:-}" ]; then
+            echo "buildLakePackage: LEAN_PATH=$LEAN_PATH"
+          fi
+
+          mkdir -p .lake/packages
+
+          # Create a minimal empty manifest if none exists.  Lake requires
+          # this file, but when all deps come from leanDeps (nix-managed),
+          # the actual dependency entries come from package-overrides.json.
+          if [ ! -f lake-manifest.json ]; then
+            echo '{"version":"1.1.0","packagesDir":".lake/packages","packages":[]}' \
+              > lake-manifest.json
+          fi
+
+          ${lib.optionalString (computedLakeDeps != null) ''
+            # Copy fetched (not yet nix-packaged) deps into .lake/packages/
+            for dep in ${computedLakeDeps}/*; do
+              depName="$(basename "$dep")"
+              cp -r "$dep" ".lake/packages/$depName"
+              chmod -R u+w ".lake/packages/$depName"
+            done
+          ''}
+
+          ${lib.concatStringsSep "\n" (
+            builtins.map (
+              dep:
+              let
+                name = dep.passthru.lakePackageName or dep.pname;
+              in
+              ''
+                # Install nix-packaged dep "${name}" into .lake/packages/.
+                # lndir creates a symlink tree so artifacts remain as
+                # zero-copy references to the store; writable dirs let Lake
+                # create metadata during workspace initialization.
+                rm -rf ".lake/packages/${name}"
+                mkdir -p ".lake/packages/${name}"
+                lndir -silent "${dep}" ".lake/packages/${name}"
+              ''
+            ) allLeanDeps
+          )}
+
+          # Generate package-overrides.json redirecting deps to local
+          # paths.  Scans .lake/packages/ so that nix-managed deps work
+          # even without a lake-manifest.json (like Haskell's package DB
+          # approach — nix is the sole dependency provider, Lake just
+          # validates against lakefile.lean at build time).
+          if [ -d .lake/packages ] && [ -n "$(ls -A .lake/packages/ 2>/dev/null)" ]; then
+            jq -n --argjson pkgs "$(
+              for dep in .lake/packages/*/; do
+                [ -d "$dep" ] || continue
+                depName="$(basename "$dep")"
+                printf '{"type":"path","name":"%s","inherited":false,"configFile":"lakefile","dir":".lake/packages/%s"}\n' \
+                  "$depName" "$depName"
+              done | jq -s '.'
+            )" '{schemaVersion: "1.1.0", packages: $pkgs}' > .lake/package-overrides.json
+          fi
+
+          runHook postConfigure
+        '';
+
+      buildPhase =
+        args.buildPhase or ''
+          runHook preBuild
+
+          local targets="${lib.concatStringsSep " " buildTargets}"
+          echo "buildLakePackage: building ''${targets:-default targets}"
+
+          lake build --no-ansi $targets
+
+          runHook postBuild
+        '';
+
+      installPhase =
+        args.installPhase or (
+          if isLibrary then
+            ''
+              runHook preInstall
+
+              # Install the complete Lake package tree.  $out/ IS the
+              # package directory — source, lakefile, and pre-built
+              # artifacts under .lake/build/.
+              cp -rT . "$out"
+
+              # Remove build-environment artifacts that reference the
+              # build sandbox or dependency store paths.
+              rm -rf "$out/.lake/packages"
+              rm -f "$out/.lake/package-overrides.json"
+
+              # Install the setup hook so that downstream derivations
+              # (and `nix develop` shells) automatically get this
+              # package's oleans in LEAN_PATH.
+              mkdir -p "$out/nix-support"
+              cp ${./setup-hook.sh} "$out/nix-support/setup-hook"
+
+              # Symlink any built executables into $out/bin/ for
+              # discoverability (e.g. packages that are both libraries
+              # and executables).
+              if [ -d "$out/.lake/build/bin" ]; then
+                mkdir -p "$out/bin"
+                for exe in "$out/.lake/build/bin"/*; do
+                  if [ -f "$exe" ] && [ -x "$exe" ]; then
+                    ln -s "../.lake/build/bin/$(basename "$exe")" "$out/bin/$(basename "$exe")"
+                  fi
+                done
+              fi
+
+              runHook postInstall
+            ''
+          else
+            ''
+              runHook preInstall
+
+              # Install executables only.
+              if [ -d .lake/build/bin ]; then
+                mkdir -p "$out/bin"
+                find .lake/build/bin -type f -executable \
+                  -exec install -Dm755 {} "$out/bin/" \;
+              fi
+
+              runHook postInstall
+            ''
+        );
+
+      passthru = passthru // {
+        inherit computedLakeDeps lean4 allLeanDeps;
+        lakePackageName = leanPackageName;
+        # Canonicalize overrideLakeDepsAttrs as an attribute overlay,
+        # following the same pattern as buildGoModule's overrideModAttrs.
+        overrideLakeDepsAttrs = lib.toExtension overrideLakeDepsAttrs;
+      };
+
+      meta = meta // {
+        platforms = meta.platforms or lean4.meta.platforms;
+      };
+    };
+}
@@ -0,0 +1,95 @@
+# fetchLakeDeps: fixed-output derivation that fetches Lake dependencies.
+#
+# Reads lake-manifest.json from the source tree, clones each git
+# dependency at its pinned revision, and produces a directory of
+# package sources.  The output is hash-verified via `lakeHash`.
+#
+# This follows the same pattern as buildGoModule's `goModules` FOD.
+{
+  lib,
+  stdenvNoCC,
+  gitMinimal,
+  cacert,
+  jq,
+}:
+
+{
+  name,
+  src,
+  hash,
+  sourceRoot ? "",
+  patches ? [ ],
+  prePatch ? "",
+  postPatch ? "",
+  # Package names to skip (e.g. already packaged in nix).
+  excludePackages ? [ ],
+}:
+
+stdenvNoCC.mkDerivation {
+  name = "${name}-lake-deps";
+
+  inherit
+    src
+    sourceRoot
+    patches
+    prePatch
+    postPatch
+    ;
+
+  nativeBuildInputs = [
+    gitMinimal
+    cacert
+    jq
+  ];
+
+  impureEnvVars = lib.fetchers.proxyImpureEnvVars ++ [
+    "GIT_PROXY_COMMAND"
+    "SOCKS_SERVER"
+  ];
+
+  dontConfigure = true;
+
+  buildPhase = ''
+    runHook preBuild
+
+    if [ ! -f lake-manifest.json ]; then
+      echo "fetchLakeDeps: lake-manifest.json not found" >&2
+      exit 1
+    fi
+
+    export HOME="$TMPDIR"
+    export GIT_SSL_CAINFO="$NIX_SSL_CERT_FILE"
+
+    mkdir -p "$TMPDIR/packages"
+
+    jq -c --argjson exclude ${lib.escapeShellArg (builtins.toJSON excludePackages)} \
+      '.packages[] | select(.type == "git") | select(.name as $n | $exclude | index($n) | not)' \
+      lake-manifest.json | while IFS= read -r pkg; do
+      name=$(echo "$pkg" | jq -r '.name')
+      url=$(echo "$pkg" | jq -r '.url')
+      rev=$(echo "$pkg" | jq -r '.rev')
+
+      echo "fetchLakeDeps: cloning $name ($url @ $rev)"
+
+      git clone --filter=blob:none --no-checkout "$url" "$TMPDIR/packages/$name"
+      git -C "$TMPDIR/packages/$name" checkout "$rev" --quiet
+
+      # Remove .git to make output deterministic
+      rm -rf "$TMPDIR/packages/$name/.git"
+    done
+
+    runHook postBuild
+  '';
+
+  installPhase = ''
+    runHook preInstall
+    mv "$TMPDIR/packages" "$out"
+    runHook postInstall
+  '';
+
+  dontFixup = true;
+
+  outputHashMode = "recursive";
+  outputHash = hash;
+  outputHashAlgo = if hash == "" then "sha256" else null;
+}
@@ -0,0 +1,8 @@
+addLeanPath() {
+    local buildLib="$1/.lake/build/lib/lean"
+    if [ -d "$buildLib" ]; then
+        addToSearchPath LEAN_PATH "$buildLib"
+    fi
+}
+
+addEnvHooks "$hostOffset" addLeanPath
@@ -0,0 +1,8 @@
+{
+  lib,
+  callPackage,
+}:
+
+lib.recurseIntoAttrs {
+  weak-minimax = callPackage ./weak-minimax/package.nix { };
+}
@@ -0,0 +1,4 @@
+import WeakMinimax
+
+def main : IO Unit := do
+  IO.println "weak_minimax: verified (maximin <= minimax)"
@@ -0,0 +1,9 @@
+import Mathlib.Order.CompleteLattice.Basic
+
+/-- Weak minimax inequality (weak duality): maximin ≤ minimax.
+For any payoff f into a complete lattice, the best worst-case guarantee
+for the maximizing player never exceeds the minimax value. -/
+theorem weak_minimax {ι κ α : Type*} [CompleteLattice α]
+    (f : ι → κ → α) :
+    ⨆ i, ⨅ j, f i j ≤ ⨅ j, ⨆ i, f i j :=
+  iSup_iInf_le_iInf_iSup f
@@ -0,0 +1,12 @@
+import Lake
+open Lake DSL
+
+package weakMinimax
+
+require "leanprover-community" / "mathlib" @ git "main"
+
+@[default_target] lean_lib WeakMinimax
+
+@[default_target]
+lean_exe weakMinimax.run where
+  root := `Main
@@ -0,0 +1,40 @@
+# Test that buildLakePackage works with nix-only deps (no lake-manifest.json).
+# Builds a Lean proof of the weak minimax inequality using mathlib.
+#
+# Note: building the executable recompiles .c → .c.o for all transitive
+# dependency modules because library packages only ship .olean/.ilean/.c
+# artifacts (the default Lake library facet).  Lake's trace system would
+# reuse pre-built object files if present, but since Lean 4 is rarely
+# used for application code, we defer shipping .o files in library
+# packages to keep store footprint minimal.
+{
+  leanPackages,
+  runCommand,
+}:
+
+let
+  inherit (leanPackages) buildLakePackage mathlib;
+
+  testPackage = buildLakePackage {
+    pname = "weak-minimax";
+    version = "0";
+    src = ./.;
+
+    leanDeps = [ mathlib ];
+  };
+in
+
+runCommand "buildLakePackage-weak-minimax"
+  {
+    nativeBuildInputs = [ testPackage ];
+  }
+  ''
+    mkdir -p $out
+
+    # Verify the executable runs (proof was verified at build time).
+    weakMinimax-run | tee $out/result
+    grep -q "weak_minimax" $out/result
+
+    # Verify library output has compiled oleans.
+    test -d "${testPackage}/.lake/build/lib/lean"
+  ''
@@ -165,6 +165,13 @@ let
        url = "https://github.com/Aider-AI/aider/commit/7201abc56539ae8ee2bf4ea0926f584c9ec5558c.patch";
        hash = "sha256-bjL9nbEQGGNkFczm1hDOMP3b48eRJk17zcivXjOdVnw=";
      })
+
+      # https://github.com/Aider-AI/aider/commit/38716cc5a2621499c50454aa77ee379aa2b0c590
+      (fetchpatch {
+        name = "add-permission-denied-error-to-litellm-exceptions.patch";
+        url = "https://github.com/Aider-AI/aider/commit/38716cc5a2621499c50454aa77ee379aa2b0c590.patch";
+        hash = "sha256-uDIUHbauAmzCfaqx6aswnkUHcmgJi4X2OdMPyn4NeYU=";
+      })
    ];

    disabledTestPaths = [
@@ -50,6 +50,9 @@ rustPlatform.buildRustPackage (finalAttrs: {
      --replace-fail /usr/bin/asusd $out/bin/asusd \
      --replace-fail /bin/sleep ${lib.getExe' coreutils "sleep"}

+    substituteInPlace data/asus-shutdown.service \
+      --replace-fail /usr/bin/asus-shutdown $out/bin/asus-shutdown
+
    substituteInPlace Makefile \
      --replace-fail /usr/bin/grep ${lib.getExe gnugrep}

@@ -30,7 +30,7 @@ appimageTools.wrapType2 {
    description = "Drag-and-drop designer for bootstrap";
    homepage = "https://bootstrapstudio.io/";
    license = lib.licenses.unfree;
-    maintainers = with lib.maintainers; [ khushraj ];
+    maintainers = [ ];
    platforms = [ "x86_64-linux" ];
  };
 }
@@ -6,16 +6,16 @@

 rustPlatform.buildRustPackage (finalAttrs: {
  pname = "complgen";
-  version = "0.8.2";
+  version = "0.8.3";

  src = fetchFromGitHub {
    owner = "adaszko";
    repo = "complgen";
    tag = "v${finalAttrs.version}";
-    hash = "sha256-cJKcyq5zV4eJboYz4l0NoGKhMilk6aPz3j3E2G+7yoU=";
+    hash = "sha256-z4jR2evvC0p306UeULroCLwaa7sjYUh7ENWp17FolAw=";
  };

-  cargoHash = "sha256-2asHTHbh8V2Or+crjNCNNiUN2CGmmsHSJ9XZHKuZhP8=";
+  cargoHash = "sha256-VhfIUP9NjsgoJ0qNUFwWdaZpWAWzSlmVgPI8kNeFVgM=";

  meta = {
    changelog = "https://github.com/adaszko/complgen/blob/v${finalAttrs.version}/CHANGELOG.md";
@@ -11,6 +11,7 @@
  libGLU,
  withLibglut ? !stdenv.hostPlatform.isDarwin,
  libglut,
+  apple-sdk,
 }:

 stdenv.mkDerivation (finalAttrs: {
@@ -29,13 +30,22 @@ stdenv.mkDerivation (finalAttrs: {
  ]
  ++ lib.optional withLibGL libGL
  ++ lib.optional withLibGLU libGLU
-  ++ lib.optional withLibglut libglut;
+  ++ lib.optional withLibglut libglut
+  ++ lib.optionals stdenv.hostPlatform.isDarwin [ apple-sdk ];
+
+  postPatch = lib.optionalString stdenv.hostPlatform.isDarwin ''
+    substituteInPlace configure --replace-fail \
+      '-I/System/Library/Frameworks/GLUT.framework/Headers/' \
+      '-I${apple-sdk}/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/System/Library/Frameworks/GLUT.framework/Headers/'
+  '';

  preConfigure = ''
    substituteInPlace src/Makefile.in \
      --replace games bin
  '';

+  env.CXXFLAGS = "-std=c++98";
+
  meta = {
    description = "Masses and springs simulation game";
    mainProgram = "construo.x11";
@@ -96,7 +96,6 @@ rustPlatform.buildRustPackage (finalAttrs: {
    homepage = "https://dprint.dev";
    license = lib.licenses.mit;
    maintainers = with lib.maintainers; [
-      khushraj
      kachick
      phanirithvij
    ];
@@ -6,16 +6,16 @@

 buildGoModule (finalAttrs: {
  pname = "favirecon";
-  version = "1.0.2";
+  version = "1.0.3";

  src = fetchFromGitHub {
    owner = "edoardottt";
    repo = "favirecon";
    tag = "v${finalAttrs.version}";
-    hash = "sha256-GpPqTtbSVLwNLKpxSb2YMZIOEHgfKn0U6K2f1ISrufc=";
+    hash = "sha256-K8SISs94SRxLAW38GT/mOOvuBktg+y9vKh9BjoJKELM=";
  };

-  vendorHash = "sha256-jjKDiow5sdwKpA1f+Dzkyb8wQuU26MHcafNYhk9H9MM=";
+  vendorHash = "sha256-PA27sDdM8/qTEUo2fYbVowP8R50cPebVPn2SXUH1VHw=";

  ldflags = [
    "-s"
@@ -19,6 +19,7 @@
  glib,
  networkmanager,
  json-glib,
+  glib-networking,
  libadwaita,
  libportal-gtk4,
  libpulseaudio,
@@ -62,6 +63,10 @@ stdenv.mkDerivation (finalAttrs: {
    pipewire
    networkmanager
    json-glib
+    # Not stricly required according to configure phase log, but putting it
+    # here adds gio modules to the GIO_EXTRA_MODULES environment variables - as
+    # required for TLS. See https://github.com/NixOS/nixpkgs/issues/502092
+    glib-networking
    libadwaita
    libportal-gtk4
    libpulseaudio
@@ -29,11 +29,11 @@
 }:
 mkDerivation {
  pname = "gren";
-  version = "0.6.3";
+  version = "0.6.5";
  src = fetchgit {
    url = "https://github.com/gren-lang/compiler.git";
-    sha256 = "0p93wamff539pb242lib2wyfr6alqz96rpyh9xb0a61ix0j3miiz";
-    rev = "54277a25d47b5c20816550ff6deab89026797526";
+    sha256 = "1865x63y0kcp2ax49333i5512vwh845iiyq3b30jm31pr113csvr";
+    rev = "ba2a2153b78086d75fe01ba45bdd630d6f5fc2fc";
    fetchSubmodules = true;
  };
  isLibrary = false;
@@ -72,7 +72,10 @@ mkDerivation {
  testHaskellDepends = [
    base
    bytestring
+    containers
    hspec
+    prettyprinter
+    text
    utf8-string
  ];
  testToolDepends = [ hspec-discover ];
@@ -80,6 +83,6 @@ mkDerivation {
  jailbreak = true;
  homepage = "https://gren-lang.org";
  description = "The `gren` command line interface";
-  license = lib.licenses.bsd3;
+  license = lib.licensesSpdx."BSD-3-Clause";
  mainProgram = "gren";
 }
@@ -11,13 +11,13 @@

 stdenv.mkDerivation (finalAttrs: {
  pname = "gren";
-  version = "0.6.3";
+  version = "0.6.5";

  src = fetchFromGitHub {
    owner = "gren-lang";
    repo = "compiler";
    tag = finalAttrs.version;
-    hash = "sha256-P8Y6JOgxGAVWT9DfbNLHVJnsPBcrUkHEumkU56riI10=";
+    hash = "sha256-eWs2Qsg3jCrBWAP7GAtBkG8RSoljjES6EpdN4IfpxaA=";
  };

  buildInputs = [ nodejs ];
@@ -0,0 +1,37 @@
+diff --git a/CMakeLists.txt b/CMakeLists.txt
+index 365b835..4341de9 100644
+--- a/CMakeLists.txt
+++ b/CMakeLists.txt
+@@ -57,6 +57,7 @@ endif(JPEG_FOUND)
+ include(FindJasper)
+ if(JASPER_FOUND)
+   set(HAVE_JASPER_LIB 1)
+  set(K2PDFOPT_LIB ${K2PDFOPT_LIB} ${JASPER_LIBRARY})
+ endif(JASPER_FOUND)
+ 
+ # paths from willuslib/wgs.c
+@@ -71,9 +72,12 @@ else()
+   message(STATUS "Could NOT find ghostscript executable")
+ endif(GHOSTSCRIPT_EXECUTABLE)
+ 
+-# willus.h
+-# HAVE_GSL_LIB
+-
+pkg_check_modules(GSL gsl)
+if(GSL_FOUND)
+  set(HAVE_GSL_LIB 1)
+  include_directories(SYSTEM ${GSL_INCLUDEDIR})
+  set(K2PDFOPT_LIB ${K2PDFOPT_LIB} ${GSL_LDFLAGS})
+endif(GSL_FOUND)
+ 
+ # libfreetype6 (>= 2.3.9), libjbig2dec0, libjpeg8 (>= 8c), libx11-6, libxext6, zlib1g (>= 1:1.2.0)
+ # MUPDF_STATIC_LDFLAGS misses mupdf-js-none, and doubles libs ...
+@@ -85,7 +89,7 @@ if(MUPDF_FOUND)
+   include_directories(SYSTEM ${MUPDF_INCLUDEDIR})
+   message(STATUS "mupdf libraries: ${MUPDF_LDFLAGS}")
+   set(K2PDFOPT_LIB ${K2PDFOPT_LIB} ${MUPDF_LDFLAGS} 
+-    -lmupdf-js-none -lopenjpeg -ljbig2dec -ljpeg -lfreetype -llcms -lgumbo
+
+   )
+ endif(MUPDF_FOUND)
+ 
@@ -0,0 +1,121 @@
+{
+  lib,
+  stdenv,
+  runCommand,
+  fetchzip,
+  fetchurl,
+  fetchpatch,
+  fetchFromGitHub,
+  cmake,
+  jbig2dec,
+  libjpeg_turbo,
+  libpng,
+  makeWrapper,
+  pkg-config,
+  zlib,
+  enableGSL ? true,
+  gsl,
+  enableGhostScript ? true,
+  ghostscript,
+  enableMuPDF ? true,
+  mupdf,
+  enableDJVU ? true,
+  djvulibre,
+  enableLeptonica ? true,
+  leptonica,
+  # Tesseract support is broken
+  # See: https://github.com/NixOS/nixpkgs/issues/368349
+  # Making GOCR work without Tesseract support is non-trivial
+  fetchDebianPatch,
+}:
+
+# k2pdfopt requires modified versions of mupdf, leptonica, and tesseract.
+# However, Debian just uses system versions with minimal fixes to k2pdfopt's
+# willuslib; some fixes to mupdf and leptoanica have since been upstreamed,
+# some are not relevant on Linux
+# Applying the upstream changes to fresh tesseract with our glibc leads to
+# k2pdfopt that crashes on launch, so we can drop tesseract or use the old
+# version that k2pdfopt wants
+
+stdenv.mkDerivation (finalAttrs: {
+  pname = "k2pdfopt";
+  version = "2.55";
+  src = fetchzip {
+    url = "http://www.willus.com/k2pdfopt/src/k2pdfopt_v${finalAttrs.version}_src.zip";
+    hash = "sha256-orQNDXQkkcCtlA8wndss6SiJk4+ImiFCG8XRLEg963k=";
+  };
+
+  patches = [
+    ./0001-Fix-CMakeLists.patch
+    (fetchDebianPatch {
+      inherit (finalAttrs) pname;
+      version = "${finalAttrs.version}+ds";
+      debianRevision = "3.1";
+      patch = "0007-k2pdfoptlib-k2ocr.c-conditionally-enable-tesseract-r.patch";
+      hash = "sha256-uJ9Gpyq64n/HKqo0hkQ2dnkSLCKNN4DedItPGzHfqR8=";
+    })
+    (fetchDebianPatch {
+      inherit (finalAttrs) pname;
+      version = "${finalAttrs.version}+ds";
+      debianRevision = "3.1";
+      patch = "0009-willuslib-CMakeLists.txt-conditionally-add-source-fi.patch";
+      hash = "sha256-cBSlcuhsw4YgAJtBJkKLW6u8tK5gFwWw7pZEJzVMJDE=";
+    })
+  ];
+
+  postPatch = ''
+    substituteInPlace willuslib/bmpdjvu.c \
+      --replace-fail "<djvu.h>" "<libdjvu/ddjvuapi.h>"
+
+    # Parts of Debian patches
+    substituteInPlace CMakeLists.txt */CMakeLists.txt \
+      --replace-fail 'cmake_minimum_required(VERSION 2.6)' \
+      'cmake_minimum_required(VERSION 3.31)'
+    substituteInPlace willuslib/bmpmupdf.c \
+      --replace-fail 'void pdf_install_load_system_font_funcs(fz_context *ctx);' \
+      'void pdf_install_load_system_font_funcs(fz_context *ctx) {};'
+    substituteInPlace willuslib/wleptonica.c \
+      --replace-fail 'dewarpBuildPageModel_ex(dew1,debug,fit_order);' \
+      'dewarpBuildPageModel(dew1,debug);'
+
+    # Potential memory corruption under benign use, and cheap to fix
+    substituteInPlace willuslib/wfile.c \
+      --replace-fail 'char cmd[MAXFILENAMELEN];' \
+      'char cmd[4*MAXFILENAMELEN];'
+  '';
+
+  nativeBuildInputs = [
+    cmake
+    pkg-config
+    makeWrapper
+  ];
+
+  buildInputs = [
+    jbig2dec
+    libjpeg_turbo
+    libpng
+    zlib
+  ]
+  ++ lib.optional enableGSL gsl
+  ++ lib.optional enableGhostScript ghostscript
+  ++ lib.optional enableMuPDF mupdf
+  ++ lib.optional enableDJVU djvulibre
+  ++ lib.optional enableLeptonica leptonica;
+
+  cmakeFlags = [ (lib.cmakeFeature "CMAKE_C_FLAGS" "-I${finalAttrs.src}/include_mod") ];
+
+  installPhase = ''
+    install -D -m 755 k2pdfopt $out/bin/k2pdfopt
+  '';
+
+  meta = {
+    description = "Optimizes PDF/DJVU files for mobile e-readers (e.g. the Kindle) and smartphones";
+    homepage = "http://www.willus.com/k2pdfopt";
+    changelog = "https://www.willus.com/k2pdfopt/k2pdfopt_version.txt";
+    license = lib.licenses.gpl3;
+    platforms = lib.platforms.linux;
+    maintainers = with lib.maintainers; [
+      raskin
+    ];
+  };
+})
@@ -98,6 +98,7 @@ stdenv.mkDerivation (finalAttrs: {
    maintainers = with lib.maintainers; [
      danielbritten
      jthulhu
+      nadja-y
    ];
    mainProgram = "lean";
  };
@@ -122,7 +122,7 @@ stdenv.mkDerivation rec {
    # we can disable it here.
    "-Ddocumentation=disabled"
  ]
-  ++ lib.optionals stdenv.hostPlatform.isAarch64 [
+  ++ lib.optionals stdenv.hostPlatform.isAarch [
    # we don't have tensorflow-lite to build this
    "-Drpi-awb-nn=disabled"
  ];
@@ -7,16 +7,16 @@

 rustPlatform.buildRustPackage (finalAttrs: {
  pname = "neocmakelsp";
-  version = "0.10.0";
+  version = "0.10.1";

  src = fetchFromGitHub {
    owner = "Decodetalkers";
    repo = "neocmakelsp";
    rev = "v${finalAttrs.version}";
-    hash = "sha256-dviHzaBqsE3NKRf4AeQme/oOcu5GyKjGJBui4ZjjDv8=";
+    hash = "sha256-Zhu3ka4suqvLLZMXC3/sRPW7EBg1YII5T+kVMf/zuH0=";
  };

-  cargoHash = "sha256-FE2DF/DnBKwW01N2wwurQ6F4qIFHMaoGZ1kb8vq86K8=";
+  cargoHash = "sha256-s7Lr0mViKUVNv1BzP8NN7102yAC/RDWkijgUGWgUK7M=";

  nativeBuildInputs = [
    installShellFiles
@@ -100,6 +100,9 @@ let
      (lib.getOutput "static" cudaPackages.cuda_cudart)
      (lib.getBin (cudaPackages.cuda_nvcc.__spliced.buildHost or cudaPackages.cuda_nvcc))
    ];
+
+    # cuda_ccl and cuda_cudart both have a LICENSE file in their output
+    ignoreCollisions = true;
  };

  cudaPath = lib.removeSuffix "-${cudaMajorVersion}" cudaToolkit;
@@ -1,37 +0,0 @@
-{
-  lib,
-  buildGoModule,
-  fetchFromGitHub,
-}:
-
-buildGoModule (finalAttrs: {
-  pname = "opengfw";
-  version = "0.4.1";
-
-  src = fetchFromGitHub {
-    owner = "apernet";
-    repo = "opengfw";
-    tag = "v${finalAttrs.version}";
-    hash = "sha256-6PFfsPfLzzeaImcteX9u/k5pwe3cvSQwT90TCizA3gI=";
-  };
-
-  vendorHash = "sha256-F8jTvgxOhOGVtl6B8u0xAIvjNwVjBtvAhApzjIgykpY=";
-
-  env.CGO_ENABLED = 0;
-
-  meta = {
-    mainProgram = "OpenGFW";
-    description = "Flexible, easy-to-use, open source implementation of GFW on Linux";
-    longDescription = ''
-      OpenGFW is your very own DIY Great Firewall of China, available as a flexible,
-      easy-to-use open source program on Linux. Why let the powers that be have all the fun?
-      It's time to give power to the people and democratize censorship.
-      Bring the thrill of cyber-sovereignty right into your home router
-      and start filtering like a pro - you too can play Big Brother.
-    '';
-    homepage = "https://gfw.dev/";
-    license = lib.licenses.mpl20;
-    platforms = lib.platforms.linux;
-    maintainers = with lib.maintainers; [ eum3l ];
-  };
-})
@@ -14,14 +14,14 @@

 rustPlatform.buildRustPackage (finalAttrs: {
  pname = "radicle-ci-broker";
-  version = "0.26.0";
+  version = "0.27.0";

  src = fetchFromRadicle {
    seed = "seed.radicle.xyz";
    repo = "zwTxygwuz5LDGBq255RA2CbNGrz8";
    node = "z6MkgEMYod7Hxfy9qCvDv5hYHkZ4ciWmLFgfvm3Wn1b2w2FV";
    tag = "v${finalAttrs.version}";
-    hash = "sha256-ns2X+XD1AL7vo9fsAm1WTj/HRBmZ9eJhIH/WYF+j4uM=";
+    hash = "sha256-1MXoAj2pa+fRKbu2WtxZb6ki6l86n2k+uqYYMcas6fA=";
    leaveDotGit = true;
    postFetch = ''
      git -C $out rev-parse --short HEAD > $out/.git_head
@@ -29,7 +29,7 @@ rustPlatform.buildRustPackage (finalAttrs: {
    '';
  };

-  cargoHash = "sha256-dMc11UB8qzP9uIF9eU+ScwCTmUS/6yLkRYfTxZYnCa0=";
+  cargoHash = "sha256-EO3KK9u17YWIwJukIDTQdQ25b0lGMuiC/gImGSYBkgs=";

  postPatch = ''
    substituteInPlace build.rs \
@@ -25,13 +25,13 @@

 rustPlatform.buildRustPackage (finalAttrs: {
  pname = "radicle-desktop";
-  version = "0.8.0";
+  version = "0.9.0";

  src = fetchFromRadicle {
    seed = "seed.radicle.xyz";
    repo = "z4D5UCArafTzTQpDZNQRuqswh3ury";
-    rev = "aeb405aaf53b56a426ab8d68c7f89b8953683224";
-    hash = "sha256-Z/6GdXf3ag/89H8UMD2GNU4CXA8TWyX8dl8uh0CTem8=";
+    tag = "releases/${finalAttrs.version}";
+    hash = "sha256-ruBHhJ0JvbtXd0GonL5rNp733mulVSQJsVzkikQKCK0=";
    leaveDotGit = true;
    postFetch = ''
      git -C $out rev-parse --short HEAD > $out/.git_head
@@ -52,7 +52,7 @@ rustPlatform.buildRustPackage (finalAttrs: {

  npmDeps = fetchNpmDeps {
    inherit (finalAttrs) src;
-    hash = "sha256-lcSNGmIv6u7DT47lOC69BRbVSK5IPiwjtdAS8aVxwqM=";
+    hash = "sha256-x0u75on1Kc+u1u1R1SLLOfmTG5kFVvn2PsaWdH/RB3w=";
  };

  cargoHash = "sha256-z5fnwc7EjSvkyu4zTUyAvVfs6quwH2p9VFDK/TdzZJE=";
@@ -85,9 +85,7 @@ rustPlatform.buildRustPackage (finalAttrs: {
    libsoup_3
    openssl
  ]
-  ++ lib.optionals stdenv.hostPlatform.isLinux [
-    webkitgtk_4_1
-  ];
+  ++ lib.optionals stdenv.hostPlatform.isLinux [ webkitgtk_4_1 ];

  preBuild = ''
    export GIT_HEAD=$(<$src/.git_head)
@@ -120,7 +118,10 @@ rustPlatform.buildRustPackage (finalAttrs: {
    runHook postCheck
  '';

-  passthru.env = finalAttrs.env;
+  passthru = {
+    inherit (finalAttrs) env;
+    updateScript = ./update.sh;
+  };

  meta = {
    description = "Radicle desktop app";
@@ -0,0 +1,5 @@
+#!/usr/bin/env nix-shell
+#!nix-shell -i bash -p coreutils gnugrep common-updater-scripts nix-update
+
+version=$(list-git-tags | grep -oP '^releases/\K\d+\.\d+\.\d+$' | sort -rV | head -1)
+nix-update --version="$version" radicle-desktop
@@ -149,6 +149,11 @@ rustPlatform.buildRustPackage (finalAttrs: {
          services.radicle.package = finalAttrs.finalPackage;
        };
      };
+      ci-broker = nixosTests.radicle-ci-broker.extendNixOS {
+        module = {
+          services.radicle.package = finalAttrs.finalPackage;
+        };
+      };
    };
  };

@@ -6,13 +6,13 @@

 callPackage ./generic.nix rec {
  pname = "shattered-pixel-dungeon";
-  version = "3.3.7";
+  version = "3.3.8";

  src = fetchFromGitHub {
    owner = "00-Evan";
    repo = "shattered-pixel-dungeon";
    tag = "v${version}";
-    hash = "sha256-nWsIaAj4IqQWmNOGFOFJ+oX0Nz6DlWEp/47/qrcZ8qs=";
+    hash = "sha256-FRYuMjDk6UzmLeaR4MoONXYvNng7uC1xkxbDSiI3gnU=";
  };

  patches = [ ];
@@ -13,16 +13,16 @@

 rustPlatform.buildRustPackage (finalAttrs: {
  pname = "tpnote";
-  version = "1.25.17";
+  version = "1.25.19";

  src = fetchFromGitHub {
    owner = "getreu";
    repo = "tp-note";
    tag = "v${finalAttrs.version}";
-    hash = "sha256-XOoqPhWS50kj2n48A0SyOuUZHsoP7YxMrWpzgpTr/DY=";
+    hash = "sha256-bL+28Uv7HxXTEbz11am2wFsNf6qqXgd4XKwiLKwmS/Y=";
  };

-  cargoHash = "sha256-4e06W8Q+pJTcUgfDSHU1ZTMG/55mYvJ6DAX3QeAa9TI=";
+  cargoHash = "sha256-EiLIHrV3YSVkBdKlNkKBN/+XpM+5rcHn6pfUAtsN+vU=";

  nativeBuildInputs = [
    cmake
@@ -1,7 +1,9 @@
 {
  buildRedist,
  cudaAtLeast,
+  cudaOlder,
  lib,
+  fetchpatch,
 }:
 buildRedist {
  redistName = "cuda";
@@ -23,6 +25,18 @@ buildRedist {
    rmdir -v "$PWD/include/cccl"
  '';

+  patches = lib.optionals (cudaAtLeast "12.9" && cudaOlder "13.0") [
+    # Fix missing _CCCL_PP_SPLICE_WITH_IMPL20 in preprocessor.h
+    # https://github.com/NVIDIA/cccl/issues/4967
+    # https://github.com/NVIDIA/cccl/pull/4972
+    (fetchpatch {
+      name = "fix-missing-_CCCL_PP_SPLICE_WITH_IMPL20";
+      url = "https://github.com/NVIDIA/cccl/commit/2c2276d8b19d737cb16811ce2eb761030f472e60.patch";
+      stripLen = 1;
+      hash = "sha256-hYfMFsd7Y8CwuNGaPYG6uEB+lg1TmWSIIU5ToVMULKY=";
+    })
+  ];
+
  # NVIDIA, in their wisdom, expect CCCL to be a directory inside include.
  # https://github.com/NVIDIA/cutlass/blob/087c84df83d254b5fb295a7a408f1a1d554085cf/CMakeLists.txt#L773
  postInstall = lib.optionalString (cudaAtLeast "13.0") ''
@@ -0,0 +1,26 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+}:
+
+buildLakePackage {
+  pname = "lean4-cli";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover";
+    repo = "lean4-cli";
+    tag = "v4.28.0";
+    hash = "sha256-9nX+dozmDAaVb5uKWL14zbILr7aqbVerTyPcN12Niw4=";
+  };
+
+  leanPackageName = "Cli";
+
+  meta = {
+    description = "Command-line argument parser for Lean 4";
+    homepage = "https://github.com/leanprover/lean4-cli";
+    license = lib.licenses.mit;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
@@ -0,0 +1,33 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+}:
+
+buildLakePackage {
+  pname = "lean4-LeanSearchClient";
+  # No lockstep tags; version pinned by mathlib's lake-manifest.json.
+  version = "0-unstable-2026-02-12";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "LeanSearchClient";
+    rev = "c5d5b8fe6e5158def25cd28eb94e4141ad97c843";
+    hash = "sha256-L2aAwn3OeRLVt/VccLdBS0ogqmIIKAwnz94PpAOhaRc=";
+  };
+
+  leanPackageName = "LeanSearchClient";
+
+  # Upstream lean-toolchain lags behind; remove it so the
+  # buildLakePackage toolchain check does not reject this package.
+  postPatch = ''
+    rm -f lean-toolchain
+  '';
+
+  meta = {
+    description = "Lean 4 client for LeanSearch and Moogle proof search";
+    homepage = "https://github.com/leanprover-community/LeanSearchClient";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
@@ -0,0 +1,26 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+}:
+
+buildLakePackage {
+  pname = "lean4-Qq";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "quote4";
+    tag = "v4.28.0";
+    hash = "sha256-BRrSdDJQAsgM/NeSL2FODCez/8zEffjDRWUToGlKDNQ=";
+  };
+
+  leanPackageName = "Qq";
+
+  meta = {
+    description = "Lean 4 compile-time quote and antiquote macros for metaprogramming";
+    homepage = "https://github.com/leanprover-community/quote4";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
@@ -0,0 +1,28 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+  batteries,
+}:
+
+buildLakePackage {
+  pname = "lean4-aesop";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "aesop";
+    tag = "v4.28.0";
+    hash = "sha256-KeP46qtEf4/lgi4iCVuYIQbazufTR4luTbsuia9JkK4=";
+  };
+
+  leanPackageName = "aesop";
+  leanDeps = [ batteries ];
+
+  meta = {
+    description = "White-box automation for Lean 4";
+    homepage = "https://github.com/leanprover-community/aesop";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
@@ -0,0 +1,26 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+}:
+
+buildLakePackage {
+  pname = "lean4-batteries";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "batteries";
+    tag = "v4.28.0";
+    hash = "sha256-3N1MCFsg5UiwBCMAhDK7WwIowMNnhjlFgAsm0UPtGKc=";
+  };
+
+  leanPackageName = "batteries";
+
+  meta = {
+    description = "The batteries-included extended library for Lean 4";
+    homepage = "https://github.com/leanprover-community/batteries";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
@@ -0,0 +1,28 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+  Cli,
+}:
+
+buildLakePackage {
+  pname = "lean4-importGraph";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "import-graph";
+    tag = "v4.28.0";
+    hash = "sha256-fZS8bFQjV7eLZCJwD+SVRzmCcCthrl+PO8vL8U8AOYs=";
+  };
+
+  leanPackageName = "importGraph";
+  leanDeps = [ Cli ];
+
+  meta = {
+    description = "Tools to analyse and visualise Lean 4 import structures";
+    homepage = "https://github.com/leanprover-community/import-graph";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
@@ -0,0 +1,47 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+  batteries,
+  aesop,
+  Qq,
+  proofwidgets,
+  plausible,
+  LeanSearchClient,
+  importGraph,
+  tests,
+}:
+
+buildLakePackage {
+  pname = "lean4-mathlib";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "mathlib4";
+    tag = "v4.28.0";
+    hash = "sha256-7kR0WvEDey5kEdqKKVEO/JgQd1VyB6a+zwPvIV5E5Pg=";
+  };
+
+  leanPackageName = "mathlib";
+  leanDeps = [
+    batteries
+    aesop
+    Qq
+    proofwidgets
+    plausible
+    LeanSearchClient
+    importGraph
+  ];
+
+  passthru.tests = {
+    inherit (tests.lake) weak-minimax;
+  };
+
+  meta = {
+    description = "Mathematical library for Lean 4";
+    homepage = "https://github.com/leanprover-community/mathlib4";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
@@ -0,0 +1,26 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+}:
+
+buildLakePackage {
+  pname = "lean4-plausible";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "plausible";
+    tag = "v4.28.0";
+    hash = "sha256-xuOfeoRPt5L0Rk4fEJPIi1A0aoNIkC1fsh5yeIx5bFI=";
+  };
+
+  leanPackageName = "plausible";
+
+  meta = {
+    description = "Property-based testing framework for Lean 4";
+    homepage = "https://github.com/leanprover-community/plausible";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
@@ -0,0 +1,68 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+  fetchNpmDeps,
+  npmHooks,
+  nodejs,
+}:
+
+let
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "ProofWidgets4";
+    tag = "v0.0.87";
+    hash = "sha256-qXEqNfwUBPnxAtLRkBZTBFhrM4JYl43gLo/PM6HOG7o=";
+  };
+in
+
+buildLakePackage {
+  pname = "lean4-proofwidgets";
+  version = "0.0.87";
+
+  inherit src;
+
+  leanPackageName = "proofwidgets";
+
+  # ProofWidgets has no Lean dependencies (lake-manifest.json packages = []).
+  lakeHash = null;
+
+  nativeBuildInputs = [
+    nodejs
+    npmHooks.npmConfigHook
+  ];
+
+  # Pre-fetched npm dependencies for the TypeScript widget build
+  # (npm/rollup in widget/).  npmConfigHook installs these offline.
+  npmDeps = fetchNpmDeps {
+    name = "lean4-proofwidgets-npm-deps";
+    inherit src;
+    sourceRoot = "source/widget";
+    hash = "sha256-CzBRrreOSytquZ/xFHPlY8r+lz5Bg9Zk9ienRhc8SiY=";
+  };
+  npmRoot = "widget";
+
+  # Lake's widgetJsAll target runs `npm clean-install` which wipes
+  # node_modules and the patched shebangs that npmConfigHook applied.
+  # Wrap npm to skip ci/clean-install (deps already installed) while
+  # passing `npm run build` through — same pattern as llama-cpp/evcc.
+  postConfigure = ''
+    local realNpm
+    realNpm="$(type -P npm)"
+    mkdir -p "$TMPDIR/npm-wrap"
+    cat > "$TMPDIR/npm-wrap/npm" <<WRAPPER
+    #!/bin/sh
+    case "\$1" in ci|clean-install) exit 0 ;; esac
+    exec "$realNpm" "\$@"
+    WRAPPER
+    chmod +x "$TMPDIR/npm-wrap/npm"
+    export PATH="$TMPDIR/npm-wrap:$PATH"
+  '';
+
+  meta = {
+    description = "Interactive UI framework for Lean 4 proof assistants";
+    homepage = "https://github.com/leanprover-community/ProofWidgets4";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
@@ -0,0 +1,83 @@
+#!/usr/bin/env nix-shell
+#!nix-shell -i bash -p nix-update common-updater-scripts curl jq
+
+# Update all leanPackages to match the lean4 version in nixpkgs.
+#
+# All mathlib-ecosystem packages (batteries, aesop, Qq, plausible,
+# importGraph, Cli, mathlib) release with the same version tag as
+# lean4 (lockstep versioning).  ProofWidgets and LeanSearchClient
+# have their own versioning; the correct versions are read from
+# mathlib's lake-manifest.json at the matching lean4 tag.
+#
+# This script only prefetches source hashes — it does not build
+# anything.  Output is a summary suitable for commit messages.
+#
+# Usage:
+#   ./pkgs/development/lean-modules/update.sh
+
+set -euo pipefail
+
+lean4_version=$(nix eval --raw .#lean4.version)
+
+# Snapshot current versions for diffing.
+old_lockstep=$(nix eval --raw .#leanPackages.mathlib.version 2>/dev/null || echo "")
+old_pw=$(nix eval --raw .#leanPackages.proofwidgets.version 2>/dev/null || echo "")
+old_lsc=$(nix eval --raw .#leanPackages.LeanSearchClient.version 2>/dev/null || echo "")
+
+manifest=$(curl -sL "https://raw.githubusercontent.com/leanprover-community/mathlib4/v${lean4_version}/lake-manifest.json")
+
+# Verify that mathlib's dependency set matches what we package.
+# If mathlib adds or removes a dep, this script needs manual updating.
+known_deps="Cli LeanSearchClient Qq aesop batteries importGraph plausible proofwidgets"
+manifest_deps=$(echo "$manifest" | jq -r '[.packages[].name] | sort | join(" ")')
+if [ "$manifest_deps" != "$known_deps" ]; then
+  echo "ERROR: mathlib dependency set has changed" >&2
+  echo "  expected: $known_deps" >&2
+  echo "  got:      $manifest_deps" >&2
+  exit 1
+fi
+
+pw_version=$(echo "$manifest" | jq -r '.packages[] | select(.name == "proofwidgets") | .inputRev' | sed 's/^v//')
+
+lsc_rev=$(echo "$manifest" | jq -r '.packages[] | select(.name == "LeanSearchClient") | .rev')
+lsc_date=$(curl -sL "https://api.github.com/repos/leanprover-community/LeanSearchClient/commits/$lsc_rev" | jq -r '.commit.committer.date[:10]')
+lsc_version="0-unstable-$lsc_date"
+
+# Leaf packages (no leanDeps).
+nix-update leanPackages.batteries        --version="$lean4_version"
+nix-update leanPackages.Qq               --version="$lean4_version"
+nix-update leanPackages.plausible        --version="$lean4_version"
+nix-update leanPackages.Cli              --version="$lean4_version"
+nix-update leanPackages.proofwidgets     --version="$pw_version"
+
+# LeanSearchClient has no lockstep tags; pin to the exact rev mathlib uses.
+update-source-version leanPackages.LeanSearchClient "$lsc_version" \
+  --rev="$lsc_rev"
+
+# Packages with leanDeps.
+nix-update leanPackages.aesop            --version="$lean4_version"
+nix-update leanPackages.importGraph      --version="$lean4_version"
+
+# mathlib (all deps are nix-packaged, no lakeHash needed).
+nix-update leanPackages.mathlib          --version="$lean4_version"
+
+# Summary.
+changes=()
+if [ "$old_lockstep" != "$lean4_version" ]; then
+  changes+=("lockstep packages: $old_lockstep -> $lean4_version")
+fi
+if [ "$old_pw" != "$pw_version" ]; then
+  changes+=("proofwidgets: $old_pw -> $pw_version")
+fi
+if [ "$old_lsc" != "$lsc_version" ]; then
+  changes+=("LeanSearchClient: $old_lsc -> $lsc_version")
+fi
+
+if [ ${#changes[@]} -eq 0 ]; then
+  echo "leanPackages: already up to date at lean4 $lean4_version"
+else
+  echo "leanPackages: update to lean4 $lean4_version"
+  for c in "${changes[@]}"; do
+    echo "  - $c"
+  done
+fi
@@ -0,0 +1,36 @@
+{
+  lib,
+  fetchzip,
+  buildDunePackage,
+  ocaml,
+  findlib,
+  zarith,
+  cppo,
+}:
+
+buildDunePackage (finalAttrs: {
+  pname = "malfunction";
+  version = "0.7.1";
+
+  src = fetchzip {
+    url = "https://github.com/stedolan/malfunction/archive/refs/tags/v${finalAttrs.version}.tar.gz";
+    hash = "sha256-Cpe5rSBvsr3pqbucGZelutPoI+bcQPFCbdcKsE/HieY=";
+  };
+
+  propagatedBuildInputs = [
+    findlib
+    zarith
+  ];
+  nativeBuildInputs = [
+    cppo
+  ];
+
+  meta = {
+    homepage = "http://github.com/stedolan/malfunction";
+    description = "Malfunction is a high-performance, low-level untyped program representation, designed as a target for compilers of functional programming languages.";
+    license = lib.licenses.lgpl21;
+    maintainers = with lib.maintainers; [ _4ever2 ];
+    mainProgram = "malfunction";
+    broken = lib.versionAtLeast ocaml.version "5.4";
+  };
+})
@@ -358,13 +358,13 @@

 buildPythonPackage (finalAttrs: {
  pname = "boto3-stubs";
-  version = "1.42.72";
+  version = "1.42.74";
  pyproject = true;

  src = fetchPypi {
    pname = "boto3_stubs";
    inherit (finalAttrs) version;
-    hash = "sha256-QfxAte69QqzESXZJMarmy9RUPv04F7G0+mC0H1RJ1LY=";
+    hash = "sha256-eBB4I15hx4AAA17OCpK++q+EZ2K2qRvs9rKIczH9AQ0=";
  };

  build-system = [ setuptools ];
@@ -16,7 +16,7 @@

 buildPythonPackage (finalAttrs: {
  pname = "homematicip";
-  version = "2.6.0";
+  version = "2.7.0";
  pyproject = true;

  disabled = pythonOlder "3.12";
@@ -25,7 +25,7 @@ buildPythonPackage (finalAttrs: {
    owner = "hahn-th";
    repo = "homematicip-rest-api";
    tag = finalAttrs.version;
-    hash = "sha256-0i3sXtwEBd9rXOEcoL7E3pCwviCcMcIQcTFFLSV3s+0=";
+    hash = "sha256-UB/zyQZj3aWu3aeR9zJSLOrWKNOWTdTjjQ4y0FjQ8pU=";
  };

  build-system = [
@@ -8,14 +8,14 @@

 buildPythonPackage (finalAttrs: {
  pname = "iamdata";
-  version = "0.1.202603221";
+  version = "0.1.202603231";
  pyproject = true;

  src = fetchFromGitHub {
    owner = "cloud-copilot";
    repo = "iam-data-python";
    tag = "v${finalAttrs.version}";
-    hash = "sha256-Yy9i/bnbsXJt9sxMDDnTka/Tt6Rdv825xDnsCC3XBmE=";
+    hash = "sha256-jJe4bp8CWQseCKnx9OG74kWKylaGyX9Pg+glMk2sIC4=";
  };

  __darwinAllowLocalNetworking = true;
@@ -15,14 +15,14 @@
 }:
 buildPythonPackage rec {
  pname = "ingredient-parser-nlp";
-  version = "2.5.0";
+  version = "2.6.0";
  pyproject = true;

  src = fetchFromGitHub {
    owner = "strangetom";
    repo = "ingredient-parser";
    tag = version;
-    hash = "sha256-xJ+WuTi/vihuliwSOvFWXk23uMUPUQIGP/WeaChwL4U=";
+    hash = "sha256-jssQSzLcIZ6ss9+FksUE9Q9IwkNvQqq57zRUg+KHAhM=";
  };

  build-system = [ setuptools ];
@@ -50,14 +50,14 @@

 buildPythonPackage rec {
  pname = "litellm";
-  version = "1.80.0";
+  version = "1.81.14";
  pyproject = true;

  src = fetchFromGitHub {
    owner = "BerriAI";
    repo = "litellm";
-    tag = "v${version}-stable.1";
-    hash = "sha256-W1tckXXQ9PlqTW5S4ml0X5rcPXSCioubDaSkQxHQrMY=";
+    tag = "v${version}-stable";
+    hash = "sha256-1QYqTsTOynLrLmjzYL4TPxwKagFKFXIQbQ1rfw8TXjc=";
  };

  build-system = [ poetry-core ];
@@ -155,16 +155,16 @@ in
      "sha256-BJ5MKA8jpafHN014Y+pLo1IKcVq1PAfufGlCFwEGSKk=";

  mypy-boto3-backup =
-    buildMypyBoto3Package "backup" "1.42.3"
-      "sha256-ESsxNpqqY56rqbweQLpcLDA25i6+A59hiOB9AUk+W8k=";
+    buildMypyBoto3Package "backup" "1.42.73"
+      "sha256-rL2H5FRbjO5aDNqBabi8TROtC3NPOx9Zkzcjh5jwkeA=";

  mypy-boto3-backup-gateway =
    buildMypyBoto3Package "backup-gateway" "1.42.58"
      "sha256-G3kwLm2IEgXNFrs8V2uCj0su2S3P72FzmWSOEYjlV4c=";

  mypy-boto3-batch =
-    buildMypyBoto3Package "batch" "1.42.72"
-      "sha256-n5buQA3+fBUS3DFwl1s0Oe8h4xyikw7hCmy5ByIQxSg=";
+    buildMypyBoto3Package "batch" "1.42.74"
+      "sha256-Rw4OTwvYRBiDTSpn7MqeaHlXVECFLWvXJg+ENN+yru8=";

  mypy-boto3-billingconductor =
    buildMypyBoto3Package "billingconductor" "1.42.7"
@@ -347,8 +347,8 @@ in
      "sha256-omWYUcr7Aj6r1F1kKAmM32fn9577UeUgqesnIiBIpPQ=";

  mypy-boto3-connectcases =
-    buildMypyBoto3Package "connectcases" "1.42.65"
-      "sha256-iR144ZT1HeBjNTrWCzaq4Z4JuA92Xk6Yo6Rjo7nxyy8=";
+    buildMypyBoto3Package "connectcases" "1.42.74"
+      "sha256-zTXFt/wFhDaeKqCPiGNpldb16HOfcZ6CP3PlcWwg/LU=";

  mypy-boto3-connectparticipant =
    buildMypyBoto3Package "connectparticipant" "1.42.3"
@@ -431,8 +431,8 @@ in
      "sha256-VLjmuBf9xHv0qwv2F3l/14KptFqXVE0OmwPF/WC06NI=";

  mypy-boto3-dynamodb =
-    buildMypyBoto3Package "dynamodb" "1.42.55"
-      "sha256-pEX0Oba8RTL9WSy39EREyPyPOXJxwNkIfnEvcfGW0vk=";
+    buildMypyBoto3Package "dynamodb" "1.42.73"
+      "sha256-P9ngk6jJgqU9VfasPRCdiZV/6Ctcfs5l8nt3Ltelyps=";

  mypy-boto3-dynamodbstreams =
    buildMypyBoto3Package "dynamodbstreams" "1.42.3"
@@ -798,8 +798,8 @@ in
      "sha256-Ru2IODClBpjyDb8JNzBJi9LPY12mg46dpSBz182qkuI=";

  mypy-boto3-lightsail =
-    buildMypyBoto3Package "lightsail" "1.42.3"
-      "sha256-aku0qwarXhKEB3GK/5Qnn07Qn5RMBZo2l2kJzMpXYHI=";
+    buildMypyBoto3Package "lightsail" "1.42.74"
+      "sha256-DdvGA4L+J/aHyJpq2nqK6uov0A4j212h6lMk3gtVu+s=";

  mypy-boto3-location =
    buildMypyBoto3Package "location" "1.42.3"
@@ -962,12 +962,12 @@ in
      "sha256-CGt/WuKol9nVwLHEwNgEsQDzIBhFarJNbq30OpiK0+I=";

  mypy-boto3-omics =
-    buildMypyBoto3Package "omics" "1.42.3"
-      "sha256-o2X4h4K/Cf/TnZG3P5uDjdVmYJRcwPlv6DnSwdzOgc0=";
+    buildMypyBoto3Package "omics" "1.42.74"
+      "sha256-aEOjRqLbfKfWWrJGdwGP8jJHXrORoJM9Q0hxQ+BHmUY=";

  mypy-boto3-opensearch =
-    buildMypyBoto3Package "opensearch" "1.42.64"
-      "sha256-NqLGG7NiCqYkkE5N0o2zfgmXFvo5Vk8dALD8Ra84htc=";
+    buildMypyBoto3Package "opensearch" "1.42.73"
+      "sha256-aRXlQy744sPCF4lUZTLaUXIzHtFUJEB9r6xaYQC6Ric=";

  mypy-boto3-opensearchserverless =
    buildMypyBoto3Package "opensearchserverless" "1.42.29"
@@ -1374,8 +1374,8 @@ in
      "sha256-olIHhtYBAz8+avIUNnLoD2pdMq+TLrB8Mn+haKeUl/0=";

  mypy-boto3-verifiedpermissions =
-    buildMypyBoto3Package "verifiedpermissions" "1.42.33"
-      "sha256-Hu79PPqjMZIddiH3DQyY0XqhbPsXM61BhR6iWKsMcRk=";
+    buildMypyBoto3Package "verifiedpermissions" "1.42.73"
+      "sha256-TwSUJodBgjjNTth4HC8XQ4h20eXCVX+r6Dwl2D7K7n0=";

  mypy-boto3-voice-id =
    buildMypyBoto3Package "voice-id" "1.42.3"
@@ -12,7 +12,7 @@

 buildPythonPackage rec {
  pname = "peakrdl-regblock";
-  version = "1.2.0";
+  version = "1.3.0";

  pyproject = true;

@@ -20,7 +20,7 @@ buildPythonPackage rec {
    owner = "SystemRDL";
    repo = "PeakRDL-regblock";
    tag = "v${version}";
-    hash = "sha256-hVHqdmXsxOoqpo84KPaK+74VPVsl61QyB5b7lFlmA0o=";
+    hash = "sha256-tIQJfz4MeRbu/TvKdAnswRft7u0xoJcoFIXAV+alUes=";
  };

  build-system = [
@@ -11,7 +11,7 @@

 buildPythonPackage rec {
  pname = "peakrdl-rust";
-  version = "0.6.2";
+  version = "0.7.1";

  pyproject = true;

@@ -19,7 +19,7 @@ buildPythonPackage rec {
    owner = "darsor";
    repo = "PeakRDL-rust";
    tag = "v${version}";
-    hash = "sha256-YU2JZGC8AF3mhzwozItgqtWsrs4YEltZiP1rNkPfZ7M=";
+    hash = "sha256-GKozCmWtCb5cUxkBBHpHYPUY6QYILg1452skGoXxThE=";
  };

  build-system = [ uv-build ];
@@ -9,12 +9,12 @@

 buildPythonPackage (finalAttrs: {
  pname = "pyexploitdb";
-  version = "0.3.18";
+  version = "0.3.19";
  pyproject = true;

  src = fetchPypi {
    inherit (finalAttrs) pname version;
-    hash = "sha256-EGZN2KR5H6oVrjrJ7VNONE1Pk61G9hZWnJabaOWlIxo=";
+    hash = "sha256-6lLacEjLsq7d39Ih5aQbXnoiSsHm4O4LV8e22VnMw90=";
  };

  build-system = [ setuptools ];
@@ -10,14 +10,14 @@

 buildPythonPackage rec {
  pname = "pyfronius";
-  version = "0.8.1";
+  version = "0.8.2";
  pyproject = true;

  src = fetchFromGitHub {
    owner = "nielstron";
    repo = "pyfronius";
    tag = version;
-    hash = "sha256-Q1GMt9K9+wohFogXwGyAhyfSxSsmo+80Kca7F7VhksA=";
+    hash = "sha256-KUO5e3UYIm49kgBxidizt77AplojOv4UsnIoDa0Gtv4=";
  };

  build-system = [ setuptools ];
@@ -25,7 +25,6 @@ buildPythonPackage rec {
  dependencies = [ aiohttp ];

  nativeCheckInputs = [
-    aiounittest
    pytestCheckHook
  ];

@@ -20,14 +20,14 @@

 buildPythonPackage (finalAttrs: {
  pname = "pypsrp";
-  version = "0.9.0";
+  version = "0.9.1";
  pyproject = true;

  src = fetchFromGitHub {
    owner = "jborean93";
    repo = "pypsrp";
    tag = "v${finalAttrs.version}";
-    hash = "sha256-EFe587tLTlNEzxhACtlbB0FspDOUvfF3ly0DRtAomuY=";
+    hash = "sha256-a0xTYrdy0SwYQ7NS/hm80BAarjhUazP/I/J7PlsIWIM=";
  };

  build-system = [ setuptools ];
@@ -59,14 +59,14 @@

 buildPythonPackage (finalAttrs: {
  pname = "qcodes";
-  version = "0.55.0";
+  version = "0.56.0";
  pyproject = true;

  src = fetchFromGitHub {
    owner = "microsoft";
    repo = "Qcodes";
    tag = "v${finalAttrs.version}";
-    hash = "sha256-Jk1QfC3jcU0x5lrgnEYdJ2w/HU84xdx3XpDPkXDzPtE=";
+    hash = "sha256-7J1vKMG1/d/8O+j+RmUtVpjFdZB4w0BVoGrIONbr/e4=";
  };

  postPatch = ''
@@ -24,14 +24,14 @@

 buildPythonPackage (finalAttrs: {
  pname = "reptor";
-  version = "0.33";
+  version = "0.34";
  pyproject = true;

  src = fetchFromGitHub {
    owner = "Syslifters";
    repo = "reptor";
    tag = finalAttrs.version;
-    hash = "sha256-Jr8Gr5oGrASK/QAgO7r78/kjtxVsxn1skfkVe3Hx2HM=";
+    hash = "sha256-L4w9QWyj+NyImQKLKWfdosLl+qytPqa+eyRw6p/4GgA=";
  };

  pythonRelaxDeps = true;
@@ -9,14 +9,14 @@

 buildPythonPackage (finalAttrs: {
  pname = "tencentcloud-sdk-python";
-  version = "3.1.60";
+  version = "3.1.62";
  pyproject = true;

  src = fetchFromGitHub {
    owner = "TencentCloud";
    repo = "tencentcloud-sdk-python";
    tag = finalAttrs.version;
-    hash = "sha256-inKl+uTdm/PpWPTVjWFDza1NZpEa/4wO/DXW36VJDZ4=";
+    hash = "sha256-ttWBQSBikQpQareJ97ZvNWm/Nyqn94vfhE4RJDIe0Gc=";
  };

  build-system = [ setuptools ];
@@ -9,13 +9,13 @@

 buildPythonPackage (finalAttrs: {
  pname = "tplink-omada-client";
-  version = "1.5.5";
+  version = "1.5.6";
  pyproject = true;

  src = fetchPypi {
    pname = "tplink_omada_client";
    inherit (finalAttrs) version;
-    hash = "sha256-uefZ1MIt0xuLo1JZEYIJhrwY4V8KG0Rb16+ZY7PwEwI=";
+    hash = "sha256-1euKLSj+nctsk8oY8cKGoCpxEsdfNlINsMeHpvXGhks=";
  };

  build-system = [ hatchling ];
@@ -2,8 +2,8 @@

 grafanaPlugin {
  pname = "yesoreyeram-infinity-datasource";
-  version = "3.7.3";
-  zipHash = "sha256-fsBbEbb8Uys/w/vnMN15WDpYbw4heztH5G30ol2uD0g=";
+  version = "3.7.4";
+  zipHash = "sha256-XRMbMRzTYGnoIN6rXefhiigZ6FX6MkF2yjlwB3bMqDQ=";
  meta = {
    description = "Visualize data from JSON, CSV, XML, GraphQL and HTML endpoints in Grafana";
    license = lib.licenses.asl20;
@@ -53,13 +53,13 @@
 }:

 let
-  version = "2026.1.1";
+  version = "2026.1.2";

  src = fetchFromGitHub {
    owner = "discourse";
    repo = "discourse";
    rev = "v${version}";
-    sha256 = "sha256-sZky/gCCfaEw75NWsUatcxN3gjeKD8jzqzGXkDbcsfU=";
+    sha256 = "sha256-iFopbpr0wr9tkpaoHkyboH22w5P9aq6utuulK4sGar8=";
  };

  ruby = ruby_3_3;
@@ -172,6 +172,8 @@ in

  go = recurseIntoAttrs (callPackage ../build-support/go/tests.nix { });

+  lake = callPackage ../build-support/lake/test { };
+
  pkg-config = recurseIntoAttrs (callPackage ../top-level/pkg-config/tests.nix { });

  buildRustCrate = recurseIntoAttrs (callPackage ../build-support/rust/build-rust-crate/test { });
@@ -962,7 +962,6 @@ mapAliases {
  jsduck = throw "jsduck has been removed, as it was broken and and unmaintained upstream."; # Added 2025-12-02
  julia_19 = throw "Julia 1.9 has reached its end of life and 'julia_19' has been removed. Please use a supported version."; # Added 2025-10-29
  julia_19-bin = throw "Julia 1.9 has reached its end of life and 'julia_19-bin' has been removed. Please use a supported version."; # Added 2025-10-29
-  k2pdfopt = throw "'k2pdfopt' has been removed from nixpkgs as it was broken"; # Added 2025-09-27
  k3s_1_30 = throw "'k3s_1_30' has been removed from nixpkgs as it has reached end of life"; # Added 2025-09-01
  k3s_1_31 = throw "'k3s_1_31' has been removed from nixpkgs as it has reached end of life"; # Added 2025-12-08
  kak-lsp = throw "'kak-lsp' has been renamed to/replaced by 'kakoune-lsp'"; # Converted to throw 2025-10-27
@@ -1499,6 +1498,7 @@ mapAliases {
  opencolorio_1 = throw "'opencolorio_1' has been removed. Use opencolorio instead"; # Added 2026-01-03
  openconnect_gnutls = throw "'openconnect_gnutls' has been renamed to/replaced by 'openconnect'"; # Converted to throw 2025-10-27
  openexr_3 = throw "'openexr_3' has been renamed to/replaced by 'openexr'"; # Converted to throw 2025-10-27
+  opengfw = throw "'opengfw' has been removed because the upstream repository was deleted"; # Added 2026-03-16
  openhmd = throw "'openhmd' has been removed due to being unmaintained upstream"; # Added 2025-11-05
  openimageio2 = throw "'openimageio2' has been renamed to/replaced by 'openimageio'"; # Converted to throw 2025-10-27
  openjdk23 = throw "OpenJDK 23 was removed as it has reached its end of life"; # Added 2025-11-04
@@ -307,6 +307,8 @@ with pkgs;
  buildFHSEnvChroot = callPackage ../build-support/build-fhsenv-chroot { }; # Deprecated; use buildFHSEnv/buildFHSEnvBubblewrap
  buildFHSEnvBubblewrap = callPackage ../build-support/build-fhsenv-bubblewrap { };

+  buildLakePackage = callPackage ../build-support/lake { };
+
  cameractrls-gtk4 = cameractrls.override { withGtk = 4; };

  cameractrls-gtk3 = cameractrls.override { withGtk = 3; };
@@ -2151,7 +2153,7 @@ with pkgs;
    cudaPackages_13_2
    ;

-  cudaPackages_12 = cudaPackages_12_8;
+  cudaPackages_12 = cudaPackages_12_9;

  cudaPackages_13 = cudaPackages_13_0;

@@ -2845,6 +2847,8 @@ with pkgs;

  leanblueprint = with python3Packages; toPythonApplication leanblueprint;

+  leanPackages = callPackage ../top-level/lean-packages.nix { };
+
  inherit (callPackage ../development/tools/lerna { })
    lerna_6
    lerna_8
@@ -0,0 +1,45 @@
+# Lean 4 package set.
+#
+# All packages are built against a single Lean toolchain version.
+# Dependencies between packages use `leanDeps` which propagates
+# .olean files via LEAN_PATH (through setup hooks), similar to how
+# Haskell propagates package.conf.d entries.
+#
+# Overriding lean4 propagates to all packages in the set:
+#   leanPackages.overrideScope (self: super: { lean4 = lean4-custom; })
+#
+# Usage:
+#   leanPackages.batteries
+#   leanPackages.mathlib
+#   leanPackages.callPackage ./my-package.nix { }
+{
+  lib,
+  newScope,
+  lean4,
+}:
+
+lib.makeScope newScope (self: {
+  inherit lean4;
+
+  # Resolve via self.callPackage so overriding lean4 in the scope
+  # propagates to the builder (same pattern as coqPackages).
+  buildLakePackage = self.callPackage ../build-support/lake { };
+
+  batteries = self.callPackage ../development/lean-modules/batteries { };
+
+  aesop = self.callPackage ../development/lean-modules/aesop { };
+
+  Qq = self.callPackage ../development/lean-modules/Qq { };
+
+  proofwidgets = self.callPackage ../development/lean-modules/proofwidgets { };
+
+  plausible = self.callPackage ../development/lean-modules/plausible { };
+
+  LeanSearchClient = self.callPackage ../development/lean-modules/LeanSearchClient { };
+
+  Cli = self.callPackage ../development/lean-modules/Cli { };
+
+  importGraph = self.callPackage ../development/lean-modules/importGraph { };
+
+  mathlib = self.callPackage ../development/lean-modules/mathlib { };
+})
@@ -1187,6 +1187,8 @@ let
          cohttp = cohttp_5_3; # due to cohttp_static_handler pulling in cohttp_5_3
        };

+        malfunction = callPackage ../development/ocaml-modules/malfunction { };
+
        mariadb = callPackage ../development/ocaml-modules/mariadb {
          inherit (pkgs) mariadb;
        };