Skip to content

measure difference of silent and non-silent processing#468

Closed
hendriktews wants to merge 1 commit into
ProofGeneral:masterfrom
hendriktews:measure-non-silent
Closed

measure difference of silent and non-silent processing#468
hendriktews wants to merge 1 commit into
ProofGeneral:masterfrom
hendriktews:measure-non-silent

Conversation

@hendriktews

Copy link
Copy Markdown
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

erikmd commented May 28, 2020

Copy link
Copy Markdown
Contributor

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

erikmd commented Jun 23, 2020

Copy link
Copy Markdown
Contributor

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

@hendriktews

hendriktews commented Jun 24, 2020 via email

Copy link
Copy Markdown
Collaborator Author

@erikmd

erikmd commented Jun 25, 2020

Copy link
Copy Markdown
Contributor

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.

2 participants