This PR adds support for ignoring user defined borrow annotations. This
can be useful when defining
`extern`/`export` pairs as the `extern` might be infected by borrow
annotations while in `export`
they are already ignored.
This PR adds a benchmark that measures `simp` performance on string
literal equality and inequality for various string lengths and
difference positions.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR ports the C emission pass from IR to LCNF, marking the last step
of the IR/LCNF conversion and thus enabling end-to-end code generation
through the new compilation infrastructure.
This PR adds an `@[mvcgen_witness_type]` tag attribute, analogous to
`@[mvcgen_invariant_type]`, that allows users to mark types as witness
types. Goals whose type is an application of a tagged type are
classified as witnesses rather than verification conditions, and appear
in a new `witnesses` section in the `mvcgen` tactic syntax (before
`invariants`).
Witnesses are concrete values the prover supplies (inspired by
zero-knowledge proofs), as opposed to invariants (predicates maintained
across iterations) or verification conditions (propositions to prove).
The test uses a ZK-inspired example where a `SquareRootWitness` value
must be provided by the prover, with the resulting constraint
auto-discharged.
Changes:
- `src/Lean/Elab/Tactic/Do/Attr.lean`: register `@[mvcgen_witness_type]`
tag attribute and `isMVCGenWitnessType` helper
- `src/Lean/Elab/Tactic/Do/VCGen/Basic.lean`: add `witnesses` field to
`State`, three-way classification in `addSubGoalAsVC`
- `src/Std/Tactic/Do/Syntax.lean`: add `witnesses` section syntax
(before `invariants`), extract shared `goalDotAlt`/`goalCaseAlt` syntax
kinds
- `src/Lean/Elab/Tactic/Do/VCGen.lean`: extract shared
`elabGoalSection`, add `elabWitnesses`, wire up witness labeling and
elaboration
- `tests/elab/mvcgenWitnessType.lean`: end-to-end tests for
witness-only, witness with `-leave`, and combined witness+invariant
scenarios
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds `Invariant.withEarlyReturnNewDo`,
`StringInvariant.withEarlyReturnNewDo`, and
`StringSliceInvariant.withEarlyReturnNewDo` which use `Prod` instead of
`MProd` for the state tuple, matching the new do elaborator's output.
The existing `withEarlyReturn` definitions are reverted to `MProd` for
backwards compatibility with the legacy do elaborator. Tests and
invariant suggestions are updated to use the `NewDo` variants.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR applies `@[mvcgen_invariant_type]` to `Std.Do.Invariant` and
removes the hard-coded fallback in `isMVCGenInvariantType` that was
needed for bootstrapping (cf. #12874). It also extracts
`StringInvariant` and `StringSliceInvariant` as named abbreviations
tagged with `@[mvcgen_invariant_type]`, so that `mvcgen` classifies
string and string slice loop invariants correctly.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds an `@[mvcgen_invariant_type]` tag attribute so that users
can mark
custom types as invariant types for the `mvcgen` tactic. Goals whose
type is an
application of a tagged type are classified as invariants rather than
verification
conditions. The hard-coded check for `Std.Do.Invariant` is kept as a
fallback
until a stage0 update allows applying the attribute directly.
A follow-up PR (after a stage0 update) will apply
`@[mvcgen_invariant_type]` to
`Std.Do.Invariant` and remove the hard-coded fallback.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes a CMake error when the `lake-ci` label is used. The
previous
implementation appended the full `tests/lake/tests/` glob to a base list
that
already included `tests/lake/tests/shake/test.sh`, causing a duplicate
`add_test` name. This uses an if/else to select the appropriate glob
instead.
Discovered via https://github.com/leanprover/lean4/pull/12540 which has
the
`lake-ci` label.
🤖 Prepared with Claude Code
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR makes sure that identifiers with `Meta` or `Simproc` in their
name do not show up in library search results.
For example, `Nat.Simproc.eq_add_gt` can currently be suggested by
library search, even though it is an implementation detail.
Additionally, there are various declarations in mathlib in the
`Mathlib.Meta` namespace that we do not want to suggest.
