Update and try to fix workflow file

Author: TwoFX

.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/Std/CoreTypesAndOperations/StringsAndFormatting.lean

@@ -11,9 +11,28 @@ namespace GroveStdlib.Std.CoreTypesAndOperations
 
 namespace StringsAndFormatting
 
+def highLevelStringTypes : List Lean.Name :=
+  [`String, `String.Slice, `String.Pos, `String.Slice.Pos]
+
+def sliceProducing : AssociationTable (β := Alias Lean.Name) .declaration
+    [`String, `String.Slice,
+     Alias.mk `String.Pos "string-pos-forwards" "String.Pos (forwards)",
+     Alias.mk `String.Pos "string-pos-backwards" "String.Pos (backwards)",
+     Alias.mk `String.Pos "string-pos-noproof" "String.Pos (no proof)",
+     Alias.mk `String.Slice.Pos "string-slice-pos-forwards" "String.Slice.Pos (forwards)",
+     Alias.mk `String.Slice.Pos "string-slice-pos-backwards" "String.Slice.Pos (backwards)",
+     Alias.mk `String.Slice.Pos "string-slice-pos-noproof" "String.Slice.Pos (no proof)"] where
+  id := "slice-producing"
+  title := "String functions returning slices"
+  description := "Operations on strings and string slices that themselves return a new string slice."
+  dataSources n := DataSource.definitionsInNamespace n.inner
+
 end StringsAndFormatting
 
+open StringsAndFormatting
+
 def stringsAndFormatting : Node :=
-  .section "strings-and-formatting" "Strings and formatting" #[]
+  .section "strings-and-formatting" "Strings and formatting"
+    #[.associationTable sliceProducing]
 
-end GroveStdlib.Std.CoreTypesAndOperations
+end GroveStdlib.Std.CoreTypesAndOperations

doc/std/grove/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": "backend",
    "scope": "",
-   "rev": "5896dd4965d1822b44d31cc26fad2fdb83430783",
+   "rev": "d7c744c5c8bd63477c013344f723b679cdb289b2",
    "name": "grove",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",