Skip to content

Conversation

@Kha
Copy link
Member

@Kha Kha commented Jan 4, 2023

Fixes #2005

@Kha
Copy link
Member Author

Kha commented Jan 4, 2023

!bench

@Kha Kha force-pushed the uncovered-stx-match branch from 896bf20 to d8387db Compare January 4, 2023 14:06
@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 896bf20.Found no runs to compare against.

@Kha
Copy link
Member Author

Kha commented Jan 4, 2023

Well yes, perhaps you should prioritize benchmarking the base commit first then!

@Kha
Copy link
Member Author

Kha commented Jan 4, 2023

Using current master as the base commit, no regressions in generated code size, which was the main metric I was curious about http://speedcenter.informatik.kit.edu/velcom/compare/bab50d33-13a1-40c4-85a0-fda5f93f8b22/to/c389a319-3dfa-4864-90f1-a9438cb0f770?hash1=fa4cbd93ee5b4e37f5aa70060f7c3b64b1a83ee9

@Kha Kha merged commit de0a569 into leanprover:master Jan 9, 2023
@Kha Kha deleted the uncovered-stx-match branch January 9, 2023 12:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Bug in syntax match

2 participants