max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: lake: query :deps output (#12105)

Browse source 
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`).
This commit is contained in:
Mac Malone 2026-01-22 12:52:43 -05:00 • committed by GitHub
parent 3bfeb0bc1f
commit f9af240bc4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 19 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/lake/Lake/Config/OutFormat.lean
View file

@ -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`. -/

1
tests/lake/tests/query/dep/lakefile.toml Normal file
View file

@ -0,0 +1 @@
name = "dep"

2
tests/lake/tests/query/lakefile.lean
View file

@ -3,6 +3,8 @@ open System Lake DSL
package test
require dep from "dep"
lean_lib lib where
srcDir := "lib"
roots := #[`A, `B, `C]

4
tests/lake/tests/query/test.sh
View file

@ -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