doc: grove: update and add String data (#11551)

This PR bumps Grove to the latest revision and starts adding data about
the `String` library.

Just a small start, more to come.

Author: TwoFX

.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/workflows/grove.yml

@@ -65,6 +65,7 @@ jobs:
           workflow: ci.yml
           path: artifacts
           name: "build-Linux release"
+          allow_forks: true
           name_is_regexp: true
 
       - name: Unpack toolchain

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