Siddharth
Siddharth
@oluwatimilehin Thank you for working on the evaluation! Do you feel that the code is in a mergeable state now? If so, please do merge it, and work on the...
@oluwatimilehin aha, my bad! I meant that we should change the status to "ready for review", to then ask for review from one of us :)
@oluwatimilehin I will do a review now, post-commit, so we can cleanup the PR. In general, I think we should submit a PR that cleans up the implementation in the...
@alexkeizer FWIW, I recommended `typeSum`, and was told that we want the ability to model muxes that take different widths. Chat with @luisacicolini about it. Also, it is possible to...
@alexkeizer For `comb.concat`, it might once again be useful to chat with @luisacicolini about it. IIRC , at some point, I tried to encode the type as you suggested and...
`omega10` claims to take `3.3s` in `instantiate metavars` from inside VScode/nvim, but externally when run with `lean`, takes `195ms`. Is this a time leak? I tried to measure this with...
I'm not sure how to get these files tracked on http://speed.lean-fro.org/lean4/run-detail/b07e1b73-1c45-4917-9065-41b479f55c6c. I guess that someone will need to teach it to also track `speedcenter` tests labeled `omega`?
I added an example that shows a fairly dramatic difference in time between the shell and VSCode: Shell: **1.59s** versus VSCode: **18.5s** for "instantiate metavars". --- tactic execution of Lean.Parser.Tactic.omega...
changelog-library
awaiting-review