Checklist for testing and reviewing a PR

Guidelines to fetch and test a Pull Request (say, PR #200) locally

install the git-pr and git-prw extra Git commands;
cd in the PG repository (in the sequel, we assume the remote origin is bound to URL [email protected]:ProofGeneral/PG.git);
run git pr 200 origin to fetch a read-only branch for PR #200 (or git prw 200 origin -f to get a read-and-write branch).

The CHANGES file must be updated, at least for new features and user-facing enhancements.
The CI checks must be green (otherwise in the case of a "spurious failure", you may want to append an excerpt of the failing log in issue #537).
Each non-trivial PR should have been tested by one maintainer (see the Guidelines above)
Ideally, the standard Elisp conventions (recommended by MELPA maintainers: Emacs Lisp conventions & Emacs Lisp Style Guide) should be followed for the added code.

In particular, the following remark (taken from the Emacs Lisp coding conventions) is paramount:

You should choose a short word to distinguish your program from other Lisp programs. The names of all global symbols in your program, that is the names of variables, constants, and functions, should begin with that chosen prefix. Separate the prefix from the rest of the name with a hyphen, -.

This practice helps avoid name conflicts, since all global variables in Emacs Lisp share the same name space, and all functions share another name space.

Use two hyphens to separate prefix and name if the symbol is not meant to be used by other packages.

There are 3 PR merging strategies in GitHub (Merge, Merge/Squash, Merge/Rebase).

But for merging PRs, we should rather use Merge or Merge/Squash:

Merge is always a good, standard choice;
Merge/Squash is especially fine if we don't want to keep the commit history of the PR branch or if the PR already contains only one commit;
whereas Merge/Rebase has two drawbacks:
1. there is no mention anywhere of the PR number in the generated commits messages;
2. and the resulting commits are not GPG-signed (cf. the missing Verified badge on those commits).
actually Merge/Rebase might be handy only in the case of "nested PR merging" (namely: we would Merge/Rebase an intermediate PR into a feature branch (for which the intermediate PR number would be useless), then create a subsequent PR, and finally Merge it from the feature branch to the master branch itself).