aya-prover / aya-prover-proto

┗:smiley:┛ ┏:smiley:┓ ┗:smiley:┛
GNU General Public License v3.0
11 stars 0 forks source link

Slightly optimize the pretty printer #754

Closed ice1000 closed 2 years ago

ice1000 commented 2 years ago

Don't merge. This is the patch in #753

ice1000 commented 2 years ago

image

This code is still slow

re-xyr commented 2 years ago

But a benchmark should be a benchmark, not a test.

ice1000 commented 2 years ago

@re-xyr Well, let's put it there so the test suite will warn us about serious performance regression

re-xyr commented 2 years ago

OK. But let's add a separate benchmark section sometime after too.

re-xyr commented 2 years ago

You merged before we reached consensus. so rude

ice1000 commented 2 years ago

OK. But let's add a separate benchmark section sometime after too.

Sure, we can do that, but how to do it? Like a separate package?

ice1000 commented 2 years ago

You merged before we reached consensus. so rude

🥺 Well basically I wanna merge the optimization. Speaking of benchmarking and testing we can change it anyway so

re-xyr commented 2 years ago

Like a separate package?

Can we just make it a gradle command like test?

Speaking of benchmarking and testing we can change it anyway so

You don't get to force push to the master branch.

ice1000 commented 2 years ago

Like a separate package?

Can we just make it a gradle command like test?

I don't know. I think test is built-in and it's hard to change it.

Speaking of benchmarking and testing we can change it anyway so

You don't get to force push to the master branch.

Well, if you really think we should erase the history, force pushing to main should be fine. I can open the permission.

re-xyr commented 2 years ago

I don't know. I think test is built-in and it's hard to change it.

I found this: https://github.com/melix/jmh-gradle-plugin

Well, if you really think we should erase the history, force pushing to main should be fine. I can open the permission.

I don't for this time. I'm just suggesting that it is better we merge after reaching consensus.

ice1000 commented 2 years ago

I don't know. I think test is built-in and it's hard to change it.

I found this: https://github.com/melix/jmh-gradle-plugin

Benchmarks are 'calculating the run-time of a program', but what I did is 'run the code, and throw exception if it's very slow', so it's different thing. I regret calling it a 'benchmark' as it's misleading.

Well, if you really think we should erase the history, force pushing to main should be fine. I can open the permission.

I don't for this time. I'm just suggesting that it is better we merge after reaching consensus.

Ok. But sometimes replies can be late.

ice1000 commented 2 years ago

Ok. But sometimes replies can be late.

Not this time though.

re-xyr commented 2 years ago

Benchmarks are 'calculating the run-time of a program', but what I did is 'run the code, and throw exception if it's very slow', so it's different thing. I regret calling it a 'benchmark' as it's misleading.

But we will have the real benchmarks sometime in the future, so this is a useful reference.

Ok. But sometimes replies can be late.

If there is no open discussion at all, I think one is free to merge.

ice1000 commented 2 years ago

Ok. But sometimes replies can be late.

If there is no open discussion at all, I think one is free to merge.

:ok_hand: