This PR adds `EquivBEq` and `LawfulHashable` instances to
`String.Slice`.
To this end, we redefine `String.Slice.hash`, which used to be
completely opaque, to be defined as `String.hash s.copy` (and then
`String.hash` remains opaque). We add tests that the `lean_slice_hash`
and `lean_string_hash` functions do indeed satisfy this relationship.
Of course, it would be even better to have a streaming MurmurHash64A
implementation in core that could be used to implement both of these so
that we can avoid the `opaque`, but that is a project for another day.
This PR further enforces that all modules used in compile-time execution
must be meta imported in preparation for enabling
https://github.com/leanprover/lean4/pull/10291
# Breaking changes
Metaprograms that call `compileDecl` directly may now need to call
`markMeta` first where appropriate, possibly based on the value of
`isMarkedMeta` of existing decls. `addAndCompile` should be split into
`addDecl` and `compileDecl` for this in order to insert the call in
between.
This PR sets up the new integrated test/bench suite. It then migrates
all benchmarks and some related tests to the new suite. There's also
some documentation and some linting.
For now, a lot of the old tests are left alone so this PR doesn't become
even larger than it already is. Eventually, all tests should be migrated
to the new suite though so there isn't a confusing mix of two systems.
2026-02-25 13:51:53 +00:00
Renamed from tests/lean/run/string_slice.lean (Browse further)
