Slightly reorganising the test suite to follow its documentation

[Mbodin]

Kind: documentation / infrastructure.

This is a split of PR #12821 containing only the parts touching the documentation and the test suite.

Fixes #10902.

[Mbodin]

I feel that I shouldn’t squash the first commit with the others: it fixes a separate issue and only touches documentation. Maybe leaving the second commit unsquashed is fine too as it only adds a test and does not reorganise anything?

I think that it is safe to squash the last two, adding @herbelin as co-author. Would that be fine?

[Mbodin]

(Sorry for the multiple forced-push: I kept getting the wrong commit message for the first commit.)

[SkySkimmer]

The test for #5996 is wrong btw (compare with the examle in the issue)

[Mbodin]

Good catch! I didn’t change it: I just moved it so that it would be tested by the continuous integration system (it is currently ignored by it).

The current test is as follows:

Goal Type.
  let c := constr:(prod nat nat) in
  let c' := (eval pattern nat in c) in
  let c' := lazymatch c' with ?f _ => f end in
  let c'' := lazymatch c' with fun x : Set => ?f => constr:(forall x : Type, f) end in
  let _ := type of c'' in
  exact c''.
Defined.

It basically corresponds to #5996 (comment) Do you think that it should be like #5996 (comment) instead? I’m afraid that I don’t know anything about #5996 to have an opinion here.

[herbelin]

The current test is basically one that I cooked at some time. Indeed, it does not fully solve the original issue. I don't know what to do. @SkySkimmer, would you like we add the original example to the file, with a Fail on the Defined, and move the whole file to bugs/opened (thus also keeping the first - current - part of the file as a working example)?

[jfehrle]

Approving the doc change. I'll leave it to others to approve the test changes.

These are small changes and somewhat related. There's no code change that affects users. I suggest squashing these commits after review is complete, just before merging.

There's a tradeoff between giving many detailed commits and having a concise, readable commit history. For code changes, we're more careful about not combining unrelated changes into a single commit. This makes the commit history more understandable and it's easier to back out changes if unexpected issues arise afterward.

When I'm submitting a PR with changes that are complex and there may multiple rounds of review, I often put the review-related changes into a new commit, imaginatively names "Review # N" so the reviewers can easily verify the incremental changes. And then squash them just before merging.

[coqbot]

For your complete information, the job build:base+async in allow failure mode has failed for commit 7286696: Apply suggestions from code review

[herbelin]

Looks good and as expected. Shall merge tomorrow if no more comments by then.

[SkySkimmer]

5996 is still wrong.

[SkySkimmer]

This doesn't belong in this PR.

[Mbodin]

I agree that there are two separate things in this PR. Should I split it again?

[SkySkimmer]

Yes, and then squash.

[SkySkimmer]

@SkySkimmer, would you like we add the original example to the file, with a Fail on the Defined, and move the whole file to bugs/opened (thus also keeping the first - current - part of the file as a working example)?

Sure that sounds fine

[Mbodin]

I added the original example. Please double-check as I’m not familiar with issue 5996.

[herbelin]

@SkySkimmer: Do we split the PR again in two? If yes, maybe can we do it ourselves to avoid adding a burden on @Mbodin who already helped a lot?

[jfehrle]

Do we split the PR again in two?

Meaning splitting it into 2 commits, not into 2 PRs? One with the doc change, one with the test changes?

[Mbodin]

I’m fine with doing it, actually ☺ (I’m learning the way PR works along the way, and I actually did appreciate the learning curve ☺)
I will first try squashing into two commits (with the documentation change, and the test-suite change), then we can split the PR or leave it as-is, depending on which is better for the git history (I don’t have much opinion on which is better).

[SkySkimmer]

I will first try squashing into two commits (with the documentation change, and the test-suite change)

No, you should split first imo

[Mbodin]

I just did the PR split ☺

[coqbot]

For your complete information, the job test-suite:4.11+trunk+dune in allow failure mode has failed for commit 81ed307: Adding the example of bug #2904 into the test suite, and reorganising the test files.

[herbelin]

As far as I understand, this is ready. Will then merge tomorrow.