This PR annotates the shadowing main definitions of `bv_decide`,
`mvcgen` and similar tactics in `Std` with the semantically richer
`tactic_alt` attribute so that `verso` will not warn about overloads.
This fixesleanprover/verso#535.
This PR adds a simple implementation of MePo, from "Lightweight
relevance filtering for machine-generated resolution problems" by Meng
and Paulson.
This needs tuning, but is already useful as a baseline or test case.
---------
Co-authored-by: Thomas Zhu <thomas.zhu.sh@hotmail.com>
This PR fixes constant folding for UIntX in the code generator. This
optimization was previously simply dead code due to the way that uint
literals are encoded.
This PR implements module docstrings in Verso syntax, as well as adding
a number of improvements and fixes to Verso docstrings in general. In
particular, they now have language server support and are parsed at
parse time rather than elaboration time, so the snapshot's syntax tree
includes the parsed documentation.
This PR adds vectored write for TCP and UDP (that helps a lot with not
copying the arrays over and over) and fix a RC issue in TCP and UDP
cancel functions with the line `lean_dec((lean_object*)udp_socket);` and
a similar one that tries to decrement the object inside of the `socket`.
This PR adds a code action for `grind` parameters. We need to use
`set_option grind.param.codeAction true` to enable the option. The PR
also adds a modifier to instruct `grind` to use the "default" pattern
inference strategy.
This PR reduces noise in the 'Equivalence classes' section of the
`grind` diagnostics. It now uses a notion of *support expressions*.
Right now, it is hard-coded, but we will probably make it extensible in
the future. The current definition is
- `match`, `ite` and `dite`-applications. They have builtin support in
`grind`.
- Cast-like applications used by `grind`: `toQ`, `toInt`, `Nat.cast`,
`Int.cast`, and `cast`
- `grind` gadget applications (e.g., `Grind.nestedDecidable`)
- Projections of constructors (e.g., `{ x := 1, y := 2}.x`)
- Auxiliary arithmetic terms constructed by solvers such as `cutsat` and
`ring`.
If an equivalence class contains at most one non-support term, it goes
into the “others” bucket. Otherwise, we display the non-support elements
and place the support terms in a child node.
**BEFORE**:
<img width="1397" height="1558" alt="image"
src="https://github.com/user-attachments/assets/4fd4de31-7300-4158-908b-247024381243"
/>
**AFTER**:
<img width="840" height="340" alt="image"
src="https://github.com/user-attachments/assets/05020f34-4ade-49bf-8ccc-9eb0ba53c861"
/>
**Remark**: No information is lost; it is just grouped differently."
This PR adds an alternative implementation of `Deriving Ord` based on
comparing `.ctorIdx` and using a dedicated matcher for comparing same
constructors (added in #10152). The new option
`deriving.ord.linear_construction_threshold` sets the constructor count
threshold (10 by default) for using the new construction.
It also (unconditionally) changes the implementation for enumeration
types to simply compare the `ctorIdx`.
This PR implements `mvcgen invariants?` for providing initial invariant
skeletons for the user to flesh out. When the loop body has an early
return, it will helpfully suggest `Invariant.withEarlyReturn ...` as a
skeleton.
```lean
def mySum (l : List Nat) : Nat := Id.run do
let mut acc := 0
for x in l do
acc := acc + x
return acc
/--
info: Try this:
invariants
· ⇓⟨xs, acc⟩ => _
-/
#guard_msgs (info) in
theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
generalize h : mySum l = r
apply Id.of_wp_run_eq h
mvcgen invariants?
all_goals admit
def nodup (l : List Int) : Bool := Id.run do
let mut seen : HashSet Int := ∅
for x in l do
if x ∈ seen then
return false
seen := seen.insert x
return true
/--
info: Try this:
invariants
· Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _)
-/
#guard_msgs (info) in
theorem nodup_suggest_invariant (l : List Int) : nodup l ↔ l.Nodup := by
generalize h : nodup l = r
apply Id.of_wp_run_eq h
mvcgen invariants?
all_goals admit
```
This PR fixes a potential miscompilation when using non-exposed type
definitions using the module system by turning it into a static error. A
future revision may lift the restriction by making the compiler metadata
independent of the current module.
This PR makes `mvcgen` reduce through `let`s, so that it progresses over
`(have t := 42; fun _ => foo t) 23` by reduction to `have t := 42; foo
t` and then introducing `t`.
This PR ensures that issues reported by the E-matching module are
displayed only when `set_option grind.debug true` is enabled. Users
reported that these messages are too distracting and not very useful.
They are more valuable for library developers when annotating their
libraries.
This PR adds an alternative implementation of `DerivingBEq` based on
comparing `.ctorIdx` and using a dedicated matcher for comparing same
constructors (added in #10152), to avoid the quadratic overhead of the
default match implementation. The new option
`deriving.beq.linear_construction_threshold` sets the constructor count
threshold (10 by default) for using the new construction. Such instances
also allow `deriving ReflBEq, LawfulBeq`, although these proofs for
these properties are still quadratic.
