connect maxHeartbeats in CoreM to kernel variable max_heartbeats#1364
connect maxHeartbeats in CoreM to kernel variable max_heartbeats#1364bollu wants to merge 7 commits intoleanprover:masterfrom
Conversation
|
Thanks for your contribution! Please make sure to follow our Commit Convention. |
|
The basic approach looks good (assuming it works :) ). Is there anything left to do apart from cleaning up the PR? |
| def addAndCompile [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] [MonadLog m] [AddMessageContext m] (decl : Declaration) : m Unit := do | ||
| addDecl decl; | ||
| compileDecl decl | ||
| def addAndCompile [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] [MonadLog m] [AddMessageContext m] (maxHeartbeats: Nat) (decl : Declaration) : m Unit := do |
There was a problem hiding this comment.
| def addAndCompile [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] [MonadLog m] [AddMessageContext m] (maxHeartbeats: Nat) (decl : Declaration) : m Unit := do | |
| def addAndCompile (decl : Declaration) : CoreM Unit := do |
I think we should avoid the extra argument here. (And adding a MonadHeartbeat class feels overkill here, this isn't even a combinator.)
src/Lean/Meta/SynthInstance.lean
Outdated
| structure Context where | ||
| maxResultSize : Nat | ||
| maxHeartbeats : Nat | ||
| maxHeartbeats : Nat := 6543 |
|
I didn't run the test suite while I was at the hackathon since my laptop is quite small :) On coming back home and running the test suite, I find a large number of tests break: https://gist.github.com/bollu/f8608a2849bde346c64d7f6ebb10ca71 I'll be debugging this tomorrow, but if anyone has any quick guesses as to why this might be the case, I'd appreciate it! |
|
For "quick guesses", |
|
@bollu Are you still planning to work on this PR, or should I close it? |
|
@leodemoura Closed to clear Lean's PR queue; I shall send a completed PR once the solution does not fail on seemingly unrelated test cases. |
No description provided.