chore: Grove: bump version (#9419)

.github/workflows/grove.yml

@@ -51,7 +51,7 @@ jobs:
       - name: Fetch upstream invalidated facts
         if: ${{ steps.should-run.outputs.should-run == 'true' && steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: fetch-upstream
-        uses: TwoFx/grove-action/fetch-upstream@v0.3
+        uses: TwoFx/grove-action/fetch-upstream@v0.4
         with:
           artifact-name: grove-invalidated-facts
           base-ref: master
@@ -95,7 +95,7 @@ jobs:
       - name: Build
         if: ${{ steps.should-run.outputs.should-run == 'true' }}
         id: build
-        uses: TwoFx/grove-action/build@v0.3
+        uses: TwoFx/grove-action/build@v0.4
         with:
           project-path: doc/std/grove
           script-name: grove-stdlib

doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Containers.lean

@@ -30,7 +30,7 @@ def associativeQueryOperations : AssociationTable .subexpression associativeCont
   title := "Associative query operations"
   description := "Operations that take as input an associative container and return a 'single' piece of information (e.g., `GetElem` or `isEmpty`, but not `toList`)."
   dataSources n :=
-    (DataSource.declarationsInNamespace n .definitionsOnly)
+    (DataSource.definitionsInNamespace n)
       |>.map Subexpression.declaration
       |>.or (DataSource.getElem n)
 
@@ -39,7 +39,7 @@ def associativeCreationOperations : AssociationTable .subexpression associativeC
   title := "Associative creation operations"
   description := "Operations that create a new associative container"
   dataSources n :=
-    (DataSource.declarationsInNamespace n .definitionsOnly)
+    (DataSource.definitionsInNamespace n)
       |>.map Subexpression.declaration
       |>.or (DataSource.emptyCollection n)
 
@@ -48,7 +48,7 @@ def associativeModificationOperations : AssociationTable .subexpression associat
   title := "Associative modification operations"
   description := "Operations that both accept and return an associative container"
   dataSources n :=
-    (DataSource.declarationsInNamespace n .definitionsOnly)
+    (DataSource.definitionsInNamespace n)
       |>.map Subexpression.declaration
 
 def associativeCreateThenQuery : Table .subexpression .subexpression .declaration associativeContainers where

doc/std/grove/grove-local.sh

@@ -3,8 +3,10 @@
 lake exe grove-stdlib --full metadata.json
 cd .lake/packages/grove/frontend
 npm install
+cp ../../../../metadata.json public/metadata.json
 if [ -f "../../../../invalidated.json" ]; then
-    GROVE_DATA_LOCATION=../../../../metadata.json GROVE_UPSTREAM_INVALIDATED_FACTS_LOCATION=../../../../invalidated.json npm run dev
+    cp ../../../../invalidated.json public/invalidated.json
+    GROVE_DATA_LOCATION=public/metadata.json GROVE_UPSTREAM_INVALIDATED_FACTS_LOCATION=public/invalidated.json npm run dev
 else
-    GROVE_DATA_LOCATION=../../../../metadata.json npm run dev
-fi
+    GROVE_DATA_LOCATION=public/metadata.json npm run dev
+fi

doc/std/grove/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": "backend",
    "scope": "",
-   "rev": "73631df7077bbd1c7283da8f5165134a27d417fa",
+   "rev": "3e8aabdea58c11813c5d3b7eeb187ded44ee9a34",
    "name": "grove",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",