Merge branch 'master' into wojciech/hashmap_deceq

Author: wkrozowski

.gitattributes

@@ -4,6 +4,7 @@ RELEASES.md merge=union
 stage0/** binary linguist-generated
 # The following file is often manually edited, so do show it in diffs
 stage0/src/stdlib_flags.h -binary -linguist-generated
+doc/std/grove/GroveStdlib/Generated/** linguist-generated
 # These files should not have line endings translated on Windows, because
 # it throws off parser tests. Later lines override earlier ones, so the
 # runner code is still treated as ordinary text.

.github/ISSUE_TEMPLATE/bug_report.md

@@ -9,7 +9,7 @@ assignees: ''
 
 ### Prerequisites
 
-Please put an X between the brackets as you perform the following steps:
+<!-- Please put an X between the brackets as you perform the following steps: -->
 
 * [ ] Check that your issue is not already filed:
       https://github.com/leanprover/lean4/issues

.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.4
+        uses: TwoFx/grove-action/fetch-upstream@v0.5
         with:
           artifact-name: grove-invalidated-facts
           base-ref: master
@@ -65,6 +65,7 @@ jobs:
           workflow: ci.yml
           path: artifacts
           name: "build-Linux release"
+          allow_forks: true
           name_is_regexp: true
 
       - name: Unpack toolchain
@@ -95,7 +96,7 @@ jobs:
       - name: Build
         if: ${{ steps.should-run.outputs.should-run == 'true' }}
         id: build
-        uses: TwoFx/grove-action/build@v0.4
+        uses: TwoFx/grove-action/build@v0.5
         with:
           project-path: doc/std/grove
           script-name: grove-stdlib

.github/workflows/pr-release.yml

@@ -127,7 +127,7 @@ jobs:
               description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}",
             });
 
-      - name: Add label
+      - name: Add toolchain-available label
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: actions/github-script@v8
         with:
@@ -515,6 +515,18 @@ jobs:
         run: |
           git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
 
+      - name: Add mathlib4-nightly-available label
+        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
+        uses: actions/github-script@v8
+        with:
+          script: |
+            await github.rest.issues.addLabels({
+              issue_number: ${{ steps.workflow-info.outputs.pullRequestNumber }},
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              labels: ['mathlib4-nightly-available']
+            })
+
       # We next automatically create a reference manual branch using this toolchain.
       # Reference manual CI will be responsible for reporting back success or failure
       # to the PR comments asynchronously (and thus transitively SubVerso/Verso).

CMakeLists.txt

@@ -44,7 +44,9 @@ if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     set(CADICAL_CXX c++)
     if (CADICAL_USE_CUSTOM_CXX)
       set(CADICAL_CXX ${CMAKE_CXX_COMPILER})
-      set(CADICAL_CXXFLAGS "${LEAN_EXTRA_CXX_FLAGS}")
+      # Use same platform flags as for Lean executables, in particular from `prepare-llvm-linux.sh`,
+      # but not Lean-specific `LEAN_EXTRA_CXX_FLAGS` such as fsanitize.
+      set(CADICAL_CXXFLAGS "${CMAKE_CXX_FLAGS}")
       set(CADICAL_LDFLAGS "-Wl,-rpath=\\$$ORIGIN/../lib")
     endif()
     find_program(CCACHE ccache)

doc/std/grove/GroveStdlib/Generated.lean

@@ -4,6 +4,7 @@ import GroveStdlib.Generated.«associative-creation-operations»
 import GroveStdlib.Generated.«associative-modification-operations»
 import GroveStdlib.Generated.«associative-create-then-query»
 import GroveStdlib.Generated.«associative-all-operations-covered»
+import GroveStdlib.Generated.«slice-producing»
 
 /-
 This file is autogenerated by grove. You can manually edit it, for example to resolve merge
@@ -20,3 +21,4 @@ def restoreState : RestoreStateM Unit := do
   «associative-modification-operations».restoreState
   «associative-create-then-query».restoreState
   «associative-all-operations-covered».restoreState
+  «slice-producing».restoreState