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.
51 lines
1.4 KiB
Text
51 lines
1.4 KiB
Text
/-!
|
||
# Error recovery for anonymous constructor notation
|
||
https://github.com/leanprover/lean4/issues/9591
|
||
|
||
When errToSorry is enabled, and too few arguments are provided, now it inserts `sorry`s
|
||
while logging an error (rather than throwing an error).
|
||
-/
|
||
|
||
/--
|
||
error: Insufficient number of fields for `⟨...⟩` constructor: Constructor `Prod.mk` has 2 explicit field, but none were provided
|
||
---
|
||
info: have this := (sorry, sorry);
|
||
this : Nat × Nat
|
||
-/
|
||
#guard_msgs in #check show Nat × Nat from ⟨⟩
|
||
|
||
/--
|
||
error: Insufficient number of fields for `⟨...⟩` constructor: Constructor `Prod.mk` has 2 explicit field, but only 1 was provided
|
||
---
|
||
info: have this := (2, sorry);
|
||
this : Nat × Nat
|
||
-/
|
||
#guard_msgs in #check show Nat × Nat from ⟨2⟩
|
||
|
||
/--
|
||
error: Insufficient number of fields for `⟨...⟩` constructor: Constructor `Prod.mk` has 2 explicit field, but only 1 was provided
|
||
---
|
||
error: Unknown constant `Nat.su`
|
||
|
||
Note: Inferred this name from the expected resulting type of `.su`:
|
||
Nat
|
||
---
|
||
info: have this := (sorry, sorry);
|
||
this : Nat × Nat
|
||
-/
|
||
#guard_msgs in #check show Nat × Nat from ⟨.su⟩
|
||
|
||
/--
|
||
info: have this := (2, 3);
|
||
this : Nat × Nat
|
||
-/
|
||
#guard_msgs in #check show Nat × Nat from ⟨2,3⟩
|
||
|
||
/-!
|
||
The `first` tactic disables errToSorry, which is how the first `exact` throws an exception rather than logging an error.
|
||
-/
|
||
/--
|
||
info: have this := (2, 3);
|
||
this : Nat × Nat
|
||
-/
|
||
#guard_msgs in #check show Nat × Nat by first | exact ⟨1⟩ | exact ⟨2,3⟩
|