Merge remote-tracking branch 'origin/nightly-with-mathlib' into paul/iterators/initial

Author: datokrat

.github/workflows/build-template.yml

@@ -193,7 +193,7 @@ jobs:
         run: |
           ulimit -c unlimited  # coredumps
           time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
-        if: (matrix.wasm || !matrix.cross) && inputs.check-level >= 1
+        if: (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.name == 'Linux release')
       - name: Test Summary
         uses: test-summary/action@v2
         with:

.github/workflows/nix-ci.yml

@@ -7,8 +7,9 @@
 /.github/ @kim-em
 /RELEASES.md @kim-em
 /src/kernel/ @leodemoura
+/src/library/compiler/ @zwarich
 /src/lake/ @tydeu
-/src/Lean/Compiler/ @leodemoura
+/src/Lean/Compiler/ @leodemoura @zwarich
 /src/Lean/Data/Lsp/ @mhuisi
 /src/Lean/Elab/Deriving/ @kim-em
 /src/Lean/Elab/Tactic/ @kim-em

CODEOWNERS

@@ -2,25 +2,24 @@ This is the repository for **Lean 4**.
 
 # About
 
-- [Quickstart](https://lean-lang.org/lean4/doc/quickstart.html)
+- [Quickstart](https://lean-lang.org/documentation/setup/)
 - [Homepage](https://lean-lang.org)
 - [Theorem Proving Tutorial](https://lean-lang.org/theorem_proving_in_lean4/)
 - [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
-- [Documentation Overview](https://lean-lang.org/lean4/doc/)
+- [Documentation Overview](https://lean-lang.org/documentation/)
 - [Language Reference](https://lean-lang.org/doc/reference/latest/)
 - [Release notes](RELEASES.md) starting at v4.0.0-m3
-- [Examples](https://lean-lang.org/lean4/doc/examples.html)
+- [Examples](https://lean-lang.org/documentation/examples/)
 - [External Contribution Guidelines](CONTRIBUTING.md)
-- [FAQ](https://lean-lang.org/lean4/doc/faq.html)
 
 # Installation
 
-See [Setting Up Lean](https://lean-lang.org/lean4/doc/setup.html).
+See [Setting Up Lean](https://lean-lang.org/documentation/setup/).
 
 # Contributing
 
 Please read our [Contribution Guidelines](CONTRIBUTING.md) first.
 
 # Building from Source
 
-See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html) (documentation source: [doc/make/index.md](doc/make/index.md)).
+See [Building Lean](doc/make/index.md).

README.md

@@ -0,0 +1,10 @@
+# Developer Documentation and Examples
+
+This directory contains documentation that describes how to work on
+Lean itself, as well as examples that are included in documentation
+that's hosted on the Lean website.  The `make` directory contains
+information on building Lean, and the `dev` directory describes how to
+work on Lean.
+
+The [documentation section](https://lean-lang.org/documentation) has
+links to documentation that describes how to use Lean itself.