fix: grind sort internalization

This PR ensures sorts are internalized by `grind`.

src/Init/Grind/Tactics.lean

@@ -182,7 +182,10 @@ namespace Lean.Parser.Tactic
 
 syntax grindErase    := "-" ident
 syntax grindLemma    := ppGroup((Attr.grindMod ppSpace)? ident)
--- `!` for enabling minimal indexable subexpression restriction
+/--
+The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
+when selecting patterns.
+-/
 syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? ident)
 syntax grindParam    := grindErase <|> grindLemma <|> grindLemmaMin
 

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -1396,7 +1396,9 @@ def EMatchTheoremKind.toSyntax (kind : EMatchTheoremKind) : CoreM (TSyntax ``Par
 private def save (ref : Syntax) (thm : EMatchTheorem) (isParam : Bool) (minIndexable : Bool) : SelectM Unit := do
   -- We only save `thm` if the pattern is different from the ones that were already found.
   if (← get).thms.all fun thm' => thm.patterns != thm'.patterns then
-    let pats ← thm.patterns.mapM fun p => (ppPattern p).toString
+    let pats ← thm.patterns.mapM fun p => do
+      let pats ← addMessageContextFull (ppPattern p)
+      pats.format
     let openBracket  := if isParam then "" else "["
     let closeBracket := if isParam then "" else "]"
     let msg := s!"{closeBracket} for pattern: {pats}"

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -380,7 +380,13 @@ where
     trace_goal[grind.internalize] "[{generation}] {e}"
     match e with
     | .bvar .. => unreachable!
-    | .sort .. => return ()
+    | .sort .. =>
+      /-
+      **Note**: It may seem wasteful to create ENodes for sorts, but it is useful for the E-matching module.
+      The E-matching module assumes that the arguments of an internalized application have also been internalized,
+      unless they are `grind` gadgets.
+      -/
+      mkENode' e generation
     | .fvar .. =>
       mkENode' e generation
       checkAndAddSplitCandidate e

src/lake/Lake/CLI/Init.lean

@@ -296,7 +296,7 @@ jobs:
       issues: write        # Grants permission to create or update issues
       pull-requests: write # Grants permission to create or update pull requests
     needs: check-for-updates
-    if: ${{ needs.check-for-updates.outputs.is-update-available }}
+    if: ${{ needs.check-for-updates.outputs.is-update-available == 'true' }}
     strategy: # Runs for each update discovered by the `check-for-updates` job.
       max-parallel: 1 # Ensures that the PRs/issues are created in order.
       matrix:

src/lake/tests/lean/test.sh

@@ -17,7 +17,7 @@ test_out '"options":{"weak.foo":"bar"}' -v lean Lib/Basic.lean
 # Test that imported workspace modules are pre-resolved
 # for both other workspace modules and external files
 test_out '"importArts":{"Lib.Basic":["' -v lean Lib.lean
-test_out '"importArts":{"Lib.Basic":["' -v lean Test.lean
+test_out '"importArts":{"Lib' -v lean Test.lean
 
 # Test running a file works outside the workspace and working directory
 test_out '"name":"_unknown"' -v lean ../../examples/hello/Hello.lean

tests/lean/run/grind_sort_intern.lean

@@ -0,0 +1,16 @@
+def f (α : Sort u) (_ : α) : Nat := 0
+
+theorem feq : f (List α) x = 0 := rfl
+
+/--
+error: `grind` failed
+case grind
+h : ¬f Prop True = 0
+⊢ False
+-/
+#guard_msgs in
+example: f Prop True = 0 := by
+  grind -verbose [feq] -- must not produce error `Prop` has not been internalized
+
+example: f Prop True = 0 := by
+  grind [f]