feat: grind chapter (#451)

This PR adds a chapter to the reference manual on `grind`.

---------

Co-authored-by: Leonardo de Moura <[email protected]>
Co-authored-by: David Thrane Christiansen <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>

Author: 4 people

.github/workflows/ci.yml

@@ -58,7 +58,6 @@ jobs:
         run: |
           set -o pipefail
           curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 

.vale/styles/Lean/Names.yml

@@ -1,20 +1,23 @@
+# This file suggests correct capitalizations / accents for names.
 extends: substitution
 message: Use '%s' instead of '%s'.
 level: error
 ignorecase: true
+# In this list, the key is case-insensitive, and the value should contain the correct case.
 swap:
   - 'de moura': 'de Moura'
   - 'de bruijn': 'de Bruijn'
   - 'blott': 'Blott'
   - 'carneiro': 'Carneiro'
   - 'collatz': 'Collatz'
   - 'lua': 'Lua'
-  - 'Madelaine': 'Madelaine'
+  - 'madelaine': 'Madelaine'
   - 'mathlib': 'Mathlib'
   - 'merkin': 'Merkin'
   - 'peano': 'Peano'
   - 'selsam': 'Selsam'
   - 'simons': 'Simons'
   - 'ullrich': 'Ullrich'
   - 'wadler': 'Wadler'
+  - 'grober': 'Gröbner'
 

.vale/styles/config/ignore/names.txt

@@ -14,3 +14,9 @@ Streicher
 Streicher's
 Ullrich
 Wadler
+Wojciech
+Nawrocki
+Nawrocki's
+Rustan
+Leino
+Leino's

.vale/styles/config/ignore/terms.txt

@@ -24,6 +24,7 @@ constructorless
 conv
 cumulative
 cumulativity
+cutsat
 deallocate
 deallocated
 deallocates
@@ -195,3 +196,4 @@ unparenthesized
 uploader
 upvote
 walkthrough
+zulip

Manual.lean

@@ -16,6 +16,7 @@ import Manual.Axioms
 import Manual.Terms
 import Manual.Tactics
 import Manual.Simp
+import Manual.Grind
 import Manual.BasicTypes
 import Manual.BasicProps
 import Manual.NotationsMacros
@@ -92,6 +93,8 @@ Thus, this reference manual does not draw a barrier between the two aspects, but
 
 {include 0 Manual.Simp}
 
+{include 0 Manual.Grind}
+
 {include 0 Manual.BasicProps}
 
 {include 0 Manual.BasicTypes}