diff --git a/.github/workflows/grove.yml b/.github/workflows/grove.yml index 2faaaac2f4..dd56b03b16 100644 --- a/.github/workflows/grove.yml +++ b/.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 diff --git a/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Containers.lean b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Containers.lean index 8ff63aa233..7e5b7e11e1 100644 --- a/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Containers.lean +++ b/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 diff --git a/doc/std/grove/grove-local.sh b/doc/std/grove/grove-local.sh index 175af37249..11fc302747 100755 --- a/doc/std/grove/grove-local.sh +++ b/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 \ No newline at end of file + GROVE_DATA_LOCATION=public/metadata.json npm run dev +fi diff --git a/doc/std/grove/lake-manifest.json b/doc/std/grove/lake-manifest.json index dcf9ca55c7..65a17d4ce5 100644 --- a/doc/std/grove/lake-manifest.json +++ b/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",