Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

measure difference of silent and non-silent processing #468

Closed

Conversation

hendriktews
Copy link
Collaborator

These are just two lines for measuring how long it takes to assert a block. The numbers show up in the Messages buffer. To see the difference between silent and non-silent processing, do it twice with and without proof-full-annotation set (also available in menu PG->Quick Options->Processing->Full Annotation).
I see 10.7 seconds for silent and 10.9 seconds for ≈3000 lines, without loading required modules.

@erikmd
Copy link
Member

erikmd commented May 28, 2020

Hi @hendriktews ! just a minor remark regarding this new feature of GitHub PRs (but maybe you're already aware of it): we can create − or convert, see screenshot below − PRs in "draft mode" to automatically tag them as not-to-be-merged-yet.

2020-05-28_19-57-28_Screenshot_PR-draft-mode

@erikmd erikmd marked this pull request as draft June 23, 2020 17:49
@erikmd erikmd changed the title measure difference of silent and non-silent processing -- do not merge measure difference of silent and non-silent processing Jun 23, 2020
@erikmd
Copy link
Member

erikmd commented Jun 23, 2020

@hendriktews just FYI I converted this PR in "draft mode" as I had proposed in my previous comment

@hendriktews
Copy link
Collaborator Author

hendriktews commented Jun 24, 2020 via email

@erikmd
Copy link
Member

erikmd commented Jun 25, 2020

The discussion in PR #467 has concluded some time ago already
that silent mode is preferred. Therefore we should abandon this
PR.

OK so closing that PR, thanks @hendriktews

@erikmd erikmd closed this Jun 25, 2020
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.

None yet

2 participants