also omit proofs with bullets and braces #772
Conversation
hendriktews
force-pushed
the
omit-bullets
branch
from
822c986
to
9e9f499
Compare
There was a problem hiding this comment.
Very good point, thanks @hendriktews !
I proofread the PR and everything looks good to me.
Currently bullets and braces are classified as commands that prevent proof omission, therefore proofs containing bullets or braces are never omitted. The new tests is therefore expected to fail.
Proofs terminated with Admitted should count as failing in the statistics, even when Coq accepts the proofs without error. The ERT test is marked expected fail, however, this is not possible for the tests of goal coq-proof-stat-batch-test, therefore the expected output is wrong, such that these tests succeed.
Change `proof-check-chunks' such that Admitted proofs are reported as failing.
hendriktews
force-pushed
the
omit-bullets
branch
from
242a671
to
b5241e8
Compare
|
Hi @hendriktews ! so AFAICT, it'd be preferable we either use Merge/Sqash or "regular" Merge (for PRs with several commits) next time. Kind regards |
|
yes, I prefer merge/rebase because of the linear history. Personally, I would not consider the mentioned drawbacks as a problem. We don't sign commits, the only problem remains are the PR numbers. Do you consider the PR numbers valuable? |
|
Hi @hendriktews, thanks for your comment.
yes and no → we don't have a policy to sign commits manually, but github does automatically sign commits for any squash or regular merge, which is an (admittedly small) upside
a bit (because it may refer to the related discussion in PR comments) but I can agree that this is subjective!
Yes, the merge/rebase will produce a completely linear history. What are the upsides of this git tree from your opinion? (just try to understand all the arguments so that we may agree it's better to either "never do a regular merge", or "always do a regular merge or squash-merge") |
|
BTW, this makes me think that there might be a small risk when doing a merge/rebase: if upstream/master has extra commits not part of the pr-branch (still without creating a conflict), the merge/rebase creates commits that have a totally different SHA1 and git tree, (but admittedly, this is a minor risk as the most important thing is that the tip of master if fine) |
|
again, sorry for the nitpick! but I'm happy to discuss whether I should do things differently (or not), from your viewpoint. Maybe: do you think that emacs-lisp repositories are a bit specific? |
Currently bullets and braces are classified as commands that prevent proof omission, which is wrong.