Merge pull request #152 from Seasawher/update

fix typos and update CI

.github/workflows/book.yml

@@ -11,11 +11,12 @@ jobs:
   book:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v3
+    - name: checkout
+      uses: actions/checkout@v4
 
     - name: install elan
       run: |
-        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $(cat lean-toolchain)
+        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
         echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
     - name: build markdown files by mdgen

.github/workflows/ci.yml

@@ -14,18 +14,7 @@ jobs:
       - name: checkout
         uses: actions/checkout@v4
 
-      - name: install elan
-        run: |
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $(cat lean-toolchain)
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Cache dependencies
-        uses: actions/cache@v3
+      - name: lean action
+        uses: leanprover/lean-action@v1
         with:
-          path: .lake
-          key: deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
-          restore-keys: |
-            deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}
-
-      - name: lake build
-        run: lake build --quiet
+          build-args: "--log-level=warning"

.github/workflows/deploy.yml

@@ -28,7 +28,7 @@ jobs:
 
       - name: install elan
         run: |
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $(cat lean-toolchain)
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
       - name: build markdown files by mdgen
@@ -43,7 +43,7 @@ jobs:
         run: mdbook build
 
       - name: upload artifact
-        uses: actions/upload-pages-artifact@v2
+        uses: actions/upload-pages-artifact@v3
         with:
           path: ./book
 
@@ -57,4 +57,4 @@ jobs:
     steps:
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v3
+        uses: actions/deploy-pages@v4

lean/main/04_metam.lean

@@ -1169,7 +1169,7 @@ useful ones:
   succeeds, `observing?` returns its result. If `x` fails (throws an exception),
   `observing?` backtracks the state and returns `none`. This is a more
   informative version of our `tryM` combinator.
-- `Lean.commitIfNoEx (x : α) : m α` executes `x`. If `x` succeeds,
+- `Lean.commitIfNoEx (x : m α) : m α` executes `x`. If `x` succeeds,
   `commitIfNoEx` returns its result. If `x` throws an exception, `commitIfNoEx`
   backtracks the state and rethrows the exception.
 
@@ -1300,7 +1300,7 @@ Notice that changing the type of the metavariable from `Nat` to, for example, `S
       let reducedExpr ← Meta.reduce constantExpr
       dbg_trace (← ppExpr reducedExpr) -- ...
     ```
-10. [**Constructing Expressions**] Create expression `fun x, 1 + x` in two ways:
+10. [**Constructing Expressions**] Create expression `fun x => 1 + x` in two ways:
   **a)** not idiomatically, with loose bound variables
   **b)** idiomatically.
   In what version can you use `Lean.mkAppN`? In what version can you use `Lean.Meta.mkAppM`?