Merge remote-tracking branch 'origin/nightly-with-mathlib' into joach…

…im/tailrec

.github/workflows/ci.yml

@@ -244,21 +244,21 @@ jobs:
                 "check-level": 2,
                 "cross": true,
                 "shell": "bash -euxo pipefail {0}"
-              },
-              {
-                "name": "Web Assembly",
-                "os": "ubuntu-latest",
-                // Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
-                "CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32 -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/",
-                "wasm": true,
-                "cmultilib": true,
-                "release": true,
-                "check-level": 2,
-                "cross": true,
-                "shell": "bash -euxo pipefail {0}",
-                // Just a few selected tests because wasm is slow
-                "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\""
               }
+              // {
+              //   "name": "Web Assembly",
+              //   "os": "ubuntu-latest",
+              //   // Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
+              //   "CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32 -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/",
+              //   "wasm": true,
+              //   "cmultilib": true,
+              //   "release": true,
+              //   "check-level": 2,
+              //   "cross": true,
+              //   "shell": "bash -euxo pipefail {0}",
+              //   // Just a few selected tests because wasm is slow
+              //   "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\""
+              // }
             ];
             console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`)
             return matrix.filter((job) => level >= job["check-level"])

.gitpod.Dockerfile

@@ -0,0 +1,14 @@
+# You can find the new timestamped tags here: https://hub.docker.com/r/gitpod/workspace-full/tags
+FROM gitpod/workspace-full
+
+USER root
+RUN apt-get update && apt-get install git libgmp-dev libuv1-dev cmake ccache clang -y && apt-get clean
+
+USER gitpod
+
+# Install and configure elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+ENV PATH="/home/gitpod/.elan/bin:${PATH}"
+# Create a dummy toolchain so that we can pre-register it with elan
+RUN mkdir -p /workspace/lean4/build/release/stage1/bin && touch /workspace/lean4/build/release/stage1/bin/lean && elan toolchain link lean4 /workspace/lean4/build/release/stage1
+RUN mkdir -p /workspace/lean4/build/release/stage0/bin && touch /workspace/lean4/build/release/stage0/bin/lean && elan toolchain link lean4-stage0 /workspace/lean4/build/release/stage0

.gitpod.yml

@@ -0,0 +1,11 @@
+image:
+    file: .gitpod.Dockerfile
+
+vscode:
+  extensions:
+    - leanprover.lean4
+
+tasks:
+  - name: Release build
+    init: cmake --preset release
+    command: make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)

README.md

@@ -6,7 +6,8 @@ This is the repository for **Lean 4**.
 - [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/)
-- [Manual](https://lean-lang.org/lean4/doc/)
+- [Documentation Overview](https://lean-lang.org/lean4/doc/)
+- [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)
 - [External Contribution Guidelines](CONTRIBUTING.md)

doc/SUMMARY.md

@@ -13,61 +13,13 @@
   - [The Well-Typed Interpreter](examples/interp.lean.md)
   - [Dependent de Bruijn Indices](examples/deBruijn.lean.md)
   - [Parametric Higher-Order Abstract Syntax](examples/phoas.lean.md)
-
-# Language Manual
-<!-- - [Using Lean](./using_lean.md) -->
-<!-- - [Lexical Structure](./lexical_structure.md) -->
-<!-- - [Expressions](./expressions.md) -->
-<!-- - [Declarations](./declarations.md) -->
-- [Organizational features](./organization.md)
-  - [Sections](./sections.md)
-  - [Namespaces](./namespaces.md)
-  - [Implicit Arguments](./implicit.md)
-  - [Auto Bound Implicit Arguments](./autobound.md)
-<!-- - [Dependent Types](./deptypes.md) -->
-<!--   - [Simple Type Theory](./simptypes.md) -->
-<!--   - [Types as objects](./typeobjs.md) -->
-<!--   - [Function Abstraction and Evaluation](./funabst.md) -->
-<!--   - [Introducing Definitions](./introdef.md) -->
-<!--   - [What makes dependent type theory dependent?](./dep.md) -->
-<!-- - [Tactics](./tactics.md) -->
-- [Syntax Extensions](./syntax.md)
-  - [The `do` Notation](./do.md)
-  - [String Interpolation](./stringinterp.md)
-  - [User-Defined Notation](./notation.md)
-  - [Macro Overview](./macro_overview.md)
-  - [Elaborators](./elaborators.md)
-  - [Examples](./syntax_examples.md)
+  - [Syntax Examples](./syntax_examples.md)
     - [Balanced Parentheses](./syntax_example.md)
     - [Arithmetic DSL](./metaprogramming-arith.md)
-- [Declaring New Types](./decltypes.md)
-  - [Enumerated Types](./enum.md)
-  - [Inductive Types](./inductive.md)
-  - [Structures](./struct.md)
-  - [Type classes](./typeclass.md)
-  - [Unification Hints](./unifhint.md)
-- [Builtin Types](./builtintypes.md)
-  - [Natural number](./nat.md)
-  - [Integer](./int.md)
-  - [Fixed precision unsigned integer](./uint.md)
-  - [Float](./float.md)
-  - [Array](./array.md)
-  - [List](./list.md)
-  - [Character](./char.md)
-  - [String](./string.md)
-  - [Option](./option.md)
-  - [Thunk](./thunk.md)
-  - [Task and Thread](./task.md)
-- [Functions](./functions.md)
-- [Monads](./monads/intro.md)
-  - [Functor](./monads/functors.lean.md)
-  - [Applicative](./monads/applicatives.lean.md)
-  - [Monad](./monads/monads.lean.md)
-  - [Reader](./monads/readers.lean.md)
-  - [State](./monads/states.lean.md)
-  - [Except](./monads/except.lean.md)
-  - [Transformers](./monads/transformers.lean.md)
-  - [Laws](./monads/laws.lean.md)
+
+# Language Manual
+
+- [The Lean Reference Manual](./reference.md)
 
 # Other
 

doc/book.toml

@@ -3,7 +3,7 @@ authors = ["Leonardo de Moura", "Sebastian Ullrich"]
 language = "en"
 multilingual = false
 src = "."
-title = "Lean Manual"
+title = "Lean Documentation Overview"
 
 [build]
 build-dir = "out"