forked from leanprover/lean4
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix: use MessageData.tagged to mark maxHeartbeat exceptions
Fixes leanprover#5565
- Loading branch information
1 parent
5e8718d
commit 1f38c2f
Showing
6 changed files
with
17 additions
and
42 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
import Lean.Elab.Command | ||
|
||
run_meta do | ||
Lean.tryCatchRuntimeEx | ||
(do | ||
Lean.Core.throwMaxHeartbeat `foo `bar 200) | ||
(fun e => | ||
unless e.isMaxHeartbeat do | ||
throwError "Not a max heartbeat error:{Lean.indentD e.toMessageData}") |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,6 @@ | ||
tcloop.lean:14:2-14:15: error: (deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached | ||
tcloop.lean:14:2-14:15: error: failed to synthesize | ||
B Nat | ||
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached | ||
Use `set_option synthInstance.maxHeartbeats <num>` to set the limit. | ||
Additional diagnostic information may be available using the `set_option diagnostics true` command. | ||
Additional diagnostic information may be available using the `set_option diagnostics true` command. |