From f9af240bc41f870807436ed058faa30166aaf767 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Thu, 22 Jan 2026 12:52:43 -0500
Subject: [PATCH] fix: lake: `query :deps` output (#12105)

This PR fixes the `lake query` output for targets which produce an
`Array` or `List` of a value with a custom `QueryText` or `QueryJson`
instance (e.g., `deps` and `transDeps`).
---
 src/lake/Lake/Config/OutFormat.lean      | 14 ++++++++++++--
 tests/lake/tests/query/dep/lakefile.toml |  1 +
 tests/lake/tests/query/lakefile.lean     |  2 ++
 tests/lake/tests/query/test.sh           |  4 ++++
 4 files changed, 19 insertions(+), 2 deletions(-)
 create mode 100644 tests/lake/tests/query/dep/lakefile.toml

diff --git a/src/lake/Lake/Config/OutFormat.lean b/src/lake/Lake/Config/OutFormat.lean
index c98a882ae0..2bd85e7d13 100644
--- a/src/lake/Lake/Config/OutFormat.lean
+++ b/src/lake/Lake/Config/OutFormat.lean
@@ -25,9 +25,15 @@ export ToText (toText)
 
 public instance (priority := 0) [ToString α] : ToText α := ⟨toString⟩
 
+@[inline] public def listToLines (as : List α) (f : α → String) : String :=
+  as.foldl (s!"{·}{f ·}\n") "" |>.dropEnd 1 |>.copy
+
+@[inline] public def arrayToLines (as : Array α) (f : α → String) : String :=
+  as.foldl (s!"{·}{f ·}\n") "" |>.dropEnd 1 |>.copy
+
 public instance : ToText Json := ⟨Json.compress⟩
-public instance [ToText α] : ToText (List α) := ⟨(·.foldl (s!"{·}{toText ·}\n") "" |>.dropEnd 1 |>.copy)⟩
-public instance [ToText α] : ToText (Array α) := ⟨(·.foldl (s!"{·}{toText ·}\n") "" |>.dropEnd 1 |>.copy)⟩
+public instance [ToText α] : ToText (List α) := ⟨(listToLines · toText)⟩
+public instance [ToText α] : ToText (Array α) := ⟨(arrayToLines · toText)⟩
 
 /-- Class used to format target output as text for `lake query`. -/
 public class QueryText (α : Type u) where
@@ -38,6 +44,8 @@ export QueryText (queryText)
 
 public instance (priority := 0) : QueryText α := ⟨fun _ => ""⟩
 public instance (priority := low) [ToText α] : QueryText α := ⟨toText⟩
+public instance [QueryText α] : QueryText (List α) := ⟨(listToLines · queryText)⟩
+public instance [QueryText α] : QueryText (Array α) := ⟨(arrayToLines · queryText)⟩
 public instance : QueryText Unit := ⟨fun _ => ""⟩
 
 attribute [deprecated QueryText (since := "2025-07-25")] ToText
@@ -51,6 +59,8 @@ export QueryJson (queryJson)
 
 public instance (priority := 0) : QueryJson α := ⟨fun _ => .null⟩
 public instance (priority := low) [ToJson α] : QueryJson α := ⟨toJson⟩
+public instance [QueryJson α] : QueryJson (List α) := ⟨(Json.arr <| ·.toArray.map queryJson)⟩
+public instance [QueryJson α] : QueryJson (Array α) := ⟨(Json.arr <| ·.map queryJson)⟩
 public instance : QueryJson Unit := ⟨fun _ => .null⟩
 
 /-- Class used to format target output for `lake query`. -/
diff --git a/tests/lake/tests/query/dep/lakefile.toml b/tests/lake/tests/query/dep/lakefile.toml
new file mode 100644
index 0000000000..0bb4f14177
--- /dev/null
+++ b/tests/lake/tests/query/dep/lakefile.toml
@@ -0,0 +1 @@
+name = "dep"
diff --git a/tests/lake/tests/query/lakefile.lean b/tests/lake/tests/query/lakefile.lean
index 932fa600ec..15c28e8298 100644
--- a/tests/lake/tests/query/lakefile.lean
+++ b/tests/lake/tests/query/lakefile.lean
@@ -3,6 +3,8 @@ open System Lake DSL
 
 package test
 
+require dep from "dep"
+
 lean_lib lib where
   srcDir := "lib"
   roots := #[`A, `B, `C]
diff --git a/tests/lake/tests/query/test.sh b/tests/lake/tests/query/test.sh
index 85085dd7ed..0eccf1bc63 100755
--- a/tests/lake/tests/query/test.sh
+++ b/tests/lake/tests/query/test.sh
@@ -20,6 +20,10 @@ test_eq '"foo"' query foo --json
 test_eq "B" query +A:imports
 test_eq '["C","B"]' query +A:transImports --json
 
+# Test querying deps
+test_eq "dep" query :deps
+test_eq '["dep.1"]' query :transDeps --json
+
 echo "# UNCOMMON TESTS"
 set -x