ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
492 stars 89 forks source link

also omit proofs with bullets and braces #772

Closed hendriktews closed 5 months ago

hendriktews commented 5 months ago

Currently bullets and braces are classified as commands that prevent proof omission, which is wrong.

erikmd commented 5 months ago

Hi @hendriktews ! sorry for the nitpick, but I believe that you used the Merge/Rebase button (?), which has 2 drawbacks documented in https://github.com/ProofGeneral/PG/wiki/Checklist-for-testing-and-reviewing-a-PR#merging-a-pr

so AFAICT, it'd be preferable we either use Merge/Sqash or "regular" Merge (for PRs with several commits) next time.

Kind regards

hendriktews commented 5 months ago

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?

erikmd commented 5 months ago

Hi @hendriktews, thanks for your comment.

We don't sign commits

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

do you consider the PR numbers valuable?

a bit (because it may refer to the related discussion in PR comments) but I can agree that this is subjective!

because of the linear history

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")

erikmd commented 5 months ago

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, so that it is possible that none of the intermediate commits (before the tip of upstream/master after the merge-rebase) builds successfully, even if all commits of the pr-branch were fine.

(but admittedly, this is a minor risk as the most important thing is that the tip of master if fine)

erikmd commented 5 months ago

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?