08eb78a5b2
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.
36 lines
1.1 KiB
Text
36 lines
1.1 KiB
Text
import Lean
|
|
/-!
|
|
# `warn.sorry` tests
|
|
|
|
When `warn.sorry` is false, don't log the "declaration uses `sorry`" warning.
|
|
-/
|
|
|
|
/-- warning: declaration uses `sorry` -/
|
|
#guard_msgs in
|
|
example : True := sorry
|
|
|
|
#guard_msgs in
|
|
set_option warn.sorry false in
|
|
example : True := sorry
|
|
|
|
/-!
|
|
Synthetic sorries should come with associated errors.
|
|
We want to get an error if there is a synthetic sorry with no associated error.
|
|
However: sometimes there are synthetic sorries in terms that come from other other terms
|
|
that have already been warned about. There is no way to tell if a given synthetic sorry had
|
|
been reported on previously. We want to be able to turn off the warning in this case too.
|
|
If we can tell whether sorries have already been warned about,
|
|
we could direct the user to inform us about elaboration bugs (synthetic sorries with no errors in the message log).
|
|
|
|
So, for now we report them just like a user `sorry`.
|
|
-/
|
|
|
|
elab "synth_sorry" : term <= expectedType => Lean.Meta.mkSorry expectedType true
|
|
|
|
/-- warning: declaration uses `sorry` -/
|
|
#guard_msgs in
|
|
example : True := synth_sorry
|
|
|
|
#guard_msgs in
|
|
set_option warn.sorry false in
|
|
example : True := synth_sorry
|