To avoid user confusion, there should be just one manual.
This PR deletes the old manual, adding a link to the new one; the
website config will redirect these pages to the corresponding new manual
content.
This PR replaces `List.lt` with `List.Lex`, from Mathlib, and adds the
new `Bool` valued lexicographic comparatory function `List.lex`. This
subtly changes the definition of `<` on Lists in some situations.
`List.lt` was a weaker relation: in particular if `l₁ < l₂`, then
`a :: l₁ < b :: l₂` may hold according to `List.lt` even if `a` and `b`
are merely incomparable
(either neither `a < b` nor `b < a`), whereas according to `List.Lex`
this would require `a = b`.
When `<` is total, in the sense that `¬ · < ·` is antisymmetric, then
the two relations coincide.
Mathlib was already overriding the order instances for `List α`,
so this change should not be noticed by anyone already using Mathlib.
We simultaneously add the boolean valued `List.lex` function,
parameterised by a `BEq` typeclass
and an arbitrary `lt` function. This will support the flexibility
previously provided for `List.lt`,
via a `==` function which is weaker than strict equality.
Breaking changes:
To build Lean from source on Windows, it is now necessary to install the
[Windows
SDK](https://developer.microsoft.com/en-us/windows/downloads/windows-sdk/).
The build instructions have been updated to reflect this. Note that the
Windows SDK is **not** needed to compile Lean programs using a Lean
toolchain obtained using `elan`. The Windows SDK is only needed to build
Lean itself from source.
Furthermore, we are dropping support for Windows versions older than
Windows 10 1903 (released in May 2019).
No Windows version that is still supported by Microsoft as part of
mainstream support is affected by this.
The following Windows versions are still supported by Microsoft as part
of commercial extended support but are no longer supported by Lean:
- Windows 10 Enterprise LTSC 2015
- Windows 10 Enterprise LTSC 2016
- Windows 10 Enterprise LTSC 2019
- Windows Server 2019
https://github.com/leanprover/vscode-lean4/pull/521 changed the display
name of the VS Code extension so that it can be found more easily when
searching for "Lean" (before it would appear far down in the list). This
PR updates the quickstart guide to reflect this fact.
Updates the user widget manual to account for more recent changes. One
issue is that the samples no longer work on https://live.lean-lang.org/
because it uses an outdated version of the `@leanprover/infoview` NPM
package. They work on https://lean.math.hhu.de/ and in recent versions
of the VSCode extension.
previously, `#eval` would happily evaluate expressions that contain
`sorry`, either explicitly or because of failing tactics. In conjunction
with operations like array access this can lead to the lean process
crashing, which isn't particularly great.
So how `#eval` will refuse to run code that (transitively) depends on
the `sorry` axiom (using the same code as `#print axioms`).
If the user really wants to run it, they can use `#eval!`.
Closes#1697
This PR updates the screenshots and instructions in the quickstart guide
for the most recent Lean 4 VS Code extension version and makes a small
stylistic change suggested by @semorrison.
This makes it reflect how we are writing release notes for 4.9.0,
including how to handle the `releases_drafts` folder and how and when to
update `RELEASES.md`.
Co-authored-by: Kim Morrison <kim@tqft.net>
This is from a ~~pair~~triple programming session with @tydeu and
@mhuisi.
If stage 1 is built with `-DUSE_LAKE=ON`, the CMake run will generate
`lakefile.toml` files for the root, `src`, and `tests`. These Lake
configuration files can then be used to build core oleans. While they do
not yet allow Lake to be used to build the Lean binaries. they do allow
Lake to be used for working interactively with the Lean source. In our
preliminary experiments, this allowed updates to `Init.Data.Nat` to be
noticed automatically when reloading downstream files, rather than
requiring a full manual compiler rebuild. This will make it easier to
work on the system.
As part of this change, Lake is added to stage 0. This allows Lake to
function in `src`, which uses the stage 0 toolchain.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Extends Lean's incremental reporting and reuse between commands into
various steps inside declarations:
* headers and bodies of each (mutual) definition/theorem
* `theorem ... := by` for each contained tactic step, including
recursively inside supported combinators currently consisting of
* `·` (cdot), `case`, `next`
* `induction`, `cases`
* macros such as `next` unfolding to the above
*Incremental reuse* means not recomputing any such steps if they are not
affected by a document change. *Incremental reporting* includes the
parts seen in the recording above: the progress bar and messages. Other
language server features such as hover etc. are *not yet* supported
incrementally, i.e. they are shown only when the declaration has been
fully processed as before.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
The layout algorithm, while somewhat finicky, is (unfortunately)
necessary for C code to interface with lean structures. This adds a
(AFAIK) complete description of the layout algorithm, including a worked
example large enough to make it possible to reconstruct the whole
decision diagram.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Expands on #3971 to do something useful even before the PR enters the
queue:
If stage0 changes are detected in the PR, set the changes-stage0 label
(which
has a tooltip to explain what this entail), and also remove the label if
it no
longer applies.
Complement to #3967 , adds a `(since := "<date>")` field to
`@[deprecated]` so that metaprogramming code has access to the
deprecation date for e.g. bulk removals. Also adds `@[deprecated
"deprecation message"]` to optionally replace the default text
"`{declName}` has been deprecated, use `{newName}` instead".
@semorrison, does this include all the answers to the questions I asked
in our thread? I think so!
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
