This PR fixes a parallelism regression where linters that e.g. check for
errors in the command would no longer find such messages.
---------
Co-authored-by: damiano <adomani@gmail.com>
`[wf_preprocess]` expects a dsimp theorem, which in `Init` temporarily
have a simplistic syntactic representation until a more robust solution
is implemented.
This PR fixes the generation of functional induction principles for
functions with nested nested well-founded recursion and late fixed
parameters. This is a follow-up for #7166. Fixes#8093.
This PR is a follow up to #8055 and implements a `Selector` for async
TCP in order to allow IO multiplexing using TCP sockets.
As we must not commit to actually fetching data from the socket buffer
this cannot be implemented by just racing on `recv?`. Instead we perform
a call to `uv_read_start` and pass an `alloc_cb` that allocates no
memory at all. According to the docs of
[`uv_alloc_cb`](https://docs.libuv.org/en/v1.x/handle.html#c.uv_alloc_cb)
this is guaranteed to give us a `UV_ENOBUFS` in the relevant callback.
Thus we can first run this "zero read" and then go into one of three
cases:
1. We get cancelled before the zero read completes, in this case just
cancel the zero read and give up.
2. The zero read completes and we loose the race for completing the
`select`, in this case just don't do anything anymore
3. The zero read completes and we win the race for completing the
`select`, in this case we perform the actual read on the socket. As we
know that data is available already (since the read callback of the zero
read is only triggered if data actually is available) we know that the
subsequent actual read should complete right away.
In this way we avoid any data loss if we loose the race.
This PR contains the theorem proving that signed division x.toInt /
y.toInt only overflows when `x = intMin w` and `y = allOnes w` (for `0 <
w`).
To show that this is the *only* case in which overflow happens, we refer
to overflow for negation
(`BitVec.sdivOverflow_eq_negOverflow_of_neg_one`): in fact,
`x.toInt/(allOnes w).toInt = - x.toInt`, i.e., the overflow conditions
are the same as `negOverflow` for `x`, and then reason about the signs
of the operands with the respective theorems.
These BitVec theorems themselves rely on numerous `Int.ediv_*` theorems,
that carefully set the bounds of signed division for integers.
co-authored by @bollu, @tobiasgrosser
This PR makes sure that the functional induction priciples for mutually
recursive structural functions with extra parameters are split deeply,
as expected.
This PR ensures that for modules opted into the experimental module
system, we do not import module docstrings or declaration ranges.
Excluding declaration docstrings as well would require some more work to
make `[inherit_doc]` leave a mere reference to the other declaration
instead of copying its docstring eagerly.
This PR adds an implementation of an async IO multiplexing framework as
well as an implementation of it for the `Timer` API in order to
demonstrate it.
The main motivation is to have fair and data loss free multiplexing of
event sources.
To illustrate two situations where just naively racing two tasks that
read from an event source might be the wrong thing:
1. Suppose we are waiting on two channel reads that are continuously
being filled up. As the first channel will always be ready when we start
its receive function it will instantly resolve the race before the
second one can even try. Thus the path where we receive data from the
second channel gets starved. For this reason we want to try in random
order (for fairness) if the event sources already have data available
for us.
2. Suppose we are waiting on two socket reads and both happen to finish
at the same time. As we are now only going to select one of them to
execute further, we are going to loose data on the second one (unless
there is a user written buffering mechanism involved) as we are going to
disregard the buffer it received and do a new receive next time. For
this reason it is important to wait for an event source to be available
without committing to actually fetching some data until we know that
this particular event source is going to win the select race.
The implementation is inspired by the Oslo framework written by
@haesbaert as well as Go's
[`select`](https://go.dev/src/runtime/select.go) implementation. Given a
list of event sources to select one from it is going to:
1. Randomly shuffle them
2. Attempt to fetch data from them (in their new random order) without
blocking (for fairness). If any of them succeeds return right away.
3. If none has data available right away set all of them up to resolve a
promise. They will then race to win the right to resolve that promise.
Only the data source that wins the race is allowed to then actually
fetch data, ensuring that no other event source actually fetches data
and then fails to deliver it to the consumer.
Follow up PRs are going to add implementations of `Selector` for
`Std.Channel` as well as TCP and UDP sockets.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR makes two improvements to the local context when there are
autobound implicits in `variable`s. First, the local context no longer
has two copies of every variable (the local context is rebuilt if the
types of autobound implicits have metavariables). Second, these
metavariables get names using the same algorithm used by binders that
appear in declarations (with `mkForallFVars'` instead of
`mkForallFVars`).
This removes the last use of `Term.addAutoBoundImplicits'`, which
inherently has this variable duplication issue.
This PR implements tactics called `extract_lets` and `lift_lets` that
manipulate `let`/`let_fun` expressions. The `extract_lets` tactic
creates new local declarations extracted from any `let` and `let_fun`
expressions in the main goal. For top-level lets in the target, it is
like the `intros` tactic, but in general it can extract lets from deeper
subexpressions as well. The `lift_lets` tactic moves `let` and `let_fun`
expressions as far out of an expression as possible, but it does not
extract any new local declarations. The option `extract_lets +lift`
combines these behaviors.
This is a re-implementation of `extract_lets` and `lift_lets` from
mathlib. The new `extract_lets` is like doing `lift_lets; extract_lets`,
but it does not lift unextractable lets like `lift_lets`. The
`lift_lets; extract_lets` behavior is now handled by `extract_lets
+lift`. The new `lift_lets` tactic is a frontend to `extract_lets +lift`
machinery, which rather than creating new local definitions instead
represents the accumulated local declarations as top-level lets.
There are also conv tactics for both of these. The `extract_lets` has a
limitation due to the conv architecture; it can extract lets for a given
conv goal, but the local declarations don't survive outside conv. They
get zeta reduced immediately upon leaving conv.
This PR makes the following modifications to the new comm ring procedure
in `grind`
1. Adds data-structures for representing equations (and their
justifications), basis, and queue of equations to be processed.
2. Adds `RingM` helper monad.
3. Adds equation simplification main loop
This PR adds support to `grind` for detecting unsatisfiable commutative
ring equations when the ring characteristic is known. Examples:
```lean
example (x : Int) : (x + 1)*(x - 1) = x^2 → False := by
grind +ring
example (x y : Int) : (x + 1)*(x - 1)*y + y = y*x^2 + 1 → False := by
grind +ring
example (x : UInt8) : (x + 1)*(x - 1) = x^2 → False := by
grind +ring
example (x y : BitVec 8) : (x + 1)*(x - 1)*y + y = y*x^2 + 1 → False := by
grind +ring
```
This PR implements basic support for `CommRing` in `grind`. Terms are
already being reified and normalized. We still need to process the
equations, but `grind` can already prove simple examples such as:
```lean
open Lean.Grind in
example [CommRing α] (x : α) : (x + 1)*(x - 1) = x^2 - 1 := by
grind +ring
open Lean.Grind in
example [CommRing α] [IsCharP α 256] (x : α) : (x + 16)*(x - 16) = x^2 := by
grind +ring
example (x : Int) : (x + 1)*(x - 1) = x^2 - 1 := by
grind +ring
example (x : UInt8) : (x + 16)*(x - 16) = x^2 := by
grind +ring
example (x : Int) : (x + 1)^2 - 1 = x^2 + 2*x := by
grind +ring
example (x : BitVec 8) : (x + 16)*(x - 16) = x^2 := by
grind +ring
example (x : BitVec 8) : (x + 1)^2 - 1 = x^2 + 2*x := by
grind +ring
```
This PR ensures that `mkAppM` can be used to construct terms that are
only type-correct at at default transparency, even if we are in
`withReducible` (e.g. in simp), so that simp does not stumble over
simplifying `let` expression with simplifiable type.reliable.
Here is a reproducer of the issue this solves:
```
example (a b : Nat) (h : a = b):
(let _ : id Bool := true; a) = (let _ : Bool := true; b) := by
simp -zeta -zetaDelta [h]
```
This fixes#7826.
This PR fixes several issues in the `CommRing` multivariate polynomial
library:
1. Replaces the previous array type with the universe polymorphic
`RArray`.
2. Properly eliminates cancelled monomials.
3. Sorts monomials in decreasing order.
4. Marks the parameter `p` of the `IsCharP` class as an output
parameter.
5. Adds `LawfulBEq` instances for the types `Power`, `Mon`, and `Poly`.
This PR adds the option `debug.terminalTacticsAsSorry`. When enabled,
terminal tactics such as `grind` and `omega` are replaced with `sorry`.
Useful for debugging and fixing bootstrapping issues.
This PR moves `ReflBEq` to `Init.Core` and changes `LawfulBEq` to extend
`ReflBEq`.
**BREAKING CHANGES:**
- The `refl` field of `ReflBEq` has been renamed to `rfl` to match
`LawfulBEq`
- `LawfulBEq` extends `ReflBEq`, so in particular `LawfulBEq.rfl` is no
longer valid
This PR modifies the syntax of `induction`, `cases`, and other tactics
that use `Lean.Parser.Tactic.inductionAlts`. If a case omits `=> ...`
then it is assumed to be `=> ?_`. Example:
```lean
example (p : Nat × Nat) : p.1 = p.1 := by
cases p with | _ p1 p2
/-
case mk
p1 p2 : Nat
⊢ (p1, p2).fst = (p1, p2).fst
-/
```
This works with multiple cases as well. Example:
```lean
example (n : Nat) : n + 1 = 1 + n := by
induction n with | zero | succ n ih
/-
case zero
⊢ 0 + 1 = 1 + 0
case succ
n : Nat
ih : n + 1 = 1 + n
⊢ n + 1 + 1 = 1 + (n + 1)
-/
```
The `induction n with | zero | succ n ih` is short for `induction n with
| zero | succ n ih => ?_`, which is short for `induction n with | zero
=> ?_ | succ n ih => ?_`. Note that a consequence of parsing is that
only the last alternative can omit `=>`. Any `=>`-free alternatives
before an alternative with `=>` will be a part of that alternative.
Rationale:
- In the future we may require `tacticSeq` to be indented. For
one-constructor types, this lets the rest of the tactic sequence not
need indentation.
- This is a semi-structured alternative to the `cases'`/`induction'`
tactics in mathlib.
This PR ensure that `bv_decide` can handle the simp normal form of a
shift.
Consider:
```lean
theorem test1 (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0)
: b <<< s = 0 := by
bv_decide
```
This works out, however:
```lean
theorem test2 (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0)
: b <<< s = 0 := by
simp
bv_decide
```
this fails because the `simp` normal form adds `toNat` to the right hand
argument of the `<<<` and `bv_decide` cannot deal with shifts by
non-constant `Nat`.
Discovered by @spdskatr
This PR fixes a bug in bv_decide where if it was presented with a match
on an enum with as many arms as constructors but the last arm being a
default match it would (wrongly) give up on the match.
This PR ensures that after `main` is finished we still wait on dedicated
tasks instead of exiting forcefully. If users wish to violently kill
their dedicated tasks at the end of main instead they can run
`IO.Process.exit` at the end of `main` instead.
This PR modifies `all_goals` so that in recovery mode it commits changes
to the state only for those goals for which the tactic succeeds (while
preserving the new message log state). Before, we were trusting that
failing tactics left things in a reasonable state, but now we roll back
and admit the goal. The changes also fixes a bug where we were rolling
back only the metacontext state and not the tactic state, leading to an
inconsistent state (a goal list with metavariables not in the
metacontext). Closes#7883
Alternatively we could stop on the first error, however it is helpful to
see what the tactic did to each goal while interactively writing a
tactic script. There is some non-monotonicity here though since tactics
can solve for metavariables that appear in successive goals, and
conceivably a later goal succeeds only if a previous one does. Given
that the non-monotonicity is limited to recovery mode (which is for
example the RHS and not the LHS of the `<;>` combinator), we think this
is acceptable.
Another justification for the change to roll back the state on each
failure is that we need to admit goals in the failing cases. When a
tactic throws an error, we cannot assume the goal list is meaningful.
Rolling back lets us admit just the goal the tactic started with,
without needing to try to work out which new metavariables should be
admitted in the error state, allowing the tactic to continue trying the
tactic on the next goal.
