From 9f1cb0f57cad1cb4545e2562f4ccbcf8861ebfc9 Mon Sep 17 00:00:00 2001
From: Nadja Yang <git@njy.dev>
Date: Mon, 9 Mar 2026 06:03:06 -0400
Subject: [PATCH] buildLakePackage: add weak-minimax test

Verifies that buildLakePackage works with nix-only deps (no
lake-manifest.json).  Builds a proof of the weak minimax inequality
from Mathlib.Order.CompleteLattice.Basic using leanDeps = [ mathlib ].
---
 pkgs/build-support/lake/test/default.nix      |  8 ++++
 .../lake/test/weak-minimax/Main.lean          |  4 ++
 .../lake/test/weak-minimax/WeakMinimax.lean   |  9 +++++
 .../lake/test/weak-minimax/lakefile.lean      | 12 ++++++
 .../lake/test/weak-minimax/package.nix        | 40 +++++++++++++++++++
 .../lean-modules/mathlib/default.nix          |  5 +++
 pkgs/test/default.nix                         |  2 +
 7 files changed, 80 insertions(+)
 create mode 100644 pkgs/build-support/lake/test/default.nix
 create mode 100644 pkgs/build-support/lake/test/weak-minimax/Main.lean
 create mode 100644 pkgs/build-support/lake/test/weak-minimax/WeakMinimax.lean
 create mode 100644 pkgs/build-support/lake/test/weak-minimax/lakefile.lean
 create mode 100644 pkgs/build-support/lake/test/weak-minimax/package.nix

diff --git a/pkgs/build-support/lake/test/default.nix b/pkgs/build-support/lake/test/default.nix
new file mode 100644
index 000000000000..b31cb5f70d5c
--- /dev/null
+++ b/pkgs/build-support/lake/test/default.nix
@@ -0,0 +1,8 @@
+{
+  lib,
+  callPackage,
+}:
+
+lib.recurseIntoAttrs {
+  weak-minimax = callPackage ./weak-minimax/package.nix { };
+}
diff --git a/pkgs/build-support/lake/test/weak-minimax/Main.lean b/pkgs/build-support/lake/test/weak-minimax/Main.lean
new file mode 100644
index 000000000000..490b95b07e82
--- /dev/null
+++ b/pkgs/build-support/lake/test/weak-minimax/Main.lean
@@ -0,0 +1,4 @@
+import WeakMinimax
+
+def main : IO Unit := do
+  IO.println "weak_minimax: verified (maximin <= minimax)"
diff --git a/pkgs/build-support/lake/test/weak-minimax/WeakMinimax.lean b/pkgs/build-support/lake/test/weak-minimax/WeakMinimax.lean
new file mode 100644
index 000000000000..2930f68e93eb
--- /dev/null
+++ b/pkgs/build-support/lake/test/weak-minimax/WeakMinimax.lean
@@ -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
diff --git a/pkgs/build-support/lake/test/weak-minimax/lakefile.lean b/pkgs/build-support/lake/test/weak-minimax/lakefile.lean
new file mode 100644
index 000000000000..9937799396d1
--- /dev/null
+++ b/pkgs/build-support/lake/test/weak-minimax/lakefile.lean
@@ -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
diff --git a/pkgs/build-support/lake/test/weak-minimax/package.nix b/pkgs/build-support/lake/test/weak-minimax/package.nix
new file mode 100644
index 000000000000..5e6114486792
--- /dev/null
+++ b/pkgs/build-support/lake/test/weak-minimax/package.nix
@@ -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"
+  ''
diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix
index 475f40e7d9b0..77d935a79a44 100644
--- a/pkgs/development/lean-modules/mathlib/default.nix
+++ b/pkgs/development/lean-modules/mathlib/default.nix
@@ -9,6 +9,7 @@
   plausible,
   LeanSearchClient,
   importGraph,
+  tests,
 }:
 
 buildLakePackage {
@@ -33,6 +34,10 @@ buildLakePackage {
     importGraph
   ];
 
+  passthru.tests = {
+    inherit (tests.lake) weak-minimax;
+  };
+
   meta = {
     description = "Mathematical library for Lean 4";
     homepage = "https://github.com/leanprover-community/mathlib4";
diff --git a/pkgs/test/default.nix b/pkgs/test/default.nix
index acd0982ed5f8..27bd1bb34d04 100644
--- a/pkgs/test/default.nix
+++ b/pkgs/test/default.nix
@@ -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 { });