Move bugs that have been closed on Bugzilla

[tchajed]

To find these bugs, I searched for all the open bugs that are resolved by visiting the following URL, run from the root of the Coq sources.

$ echo 'https://coq.inria.fr/bugs/buglist.cgi?bug_id_type=anyexact&bug_status=RESOLVED&list_id=331382&product=Coq&query_format=advanced&resolution=FIXED&bug_id='$(ls test-suite/bugs/opened/*.v | grep -o '\d\+' | tr '\n' ',')

[maximedenes]

There is something odd here. Usually when moving a test case from open to closed, you need to invert the logic of the test (typically remove Fail).

The test case 1501.v is incorrect. In fact, I'm guessing the bug should have been closed with INVALID.
2456.v still fails, for a different reason, so it may be a regression.
2814.v seems a legitimate move since it now fails whereas it was emitting an anomaly before.
3100.v is similar
3320.v is probably not really testing the bug
3794.v I don't understand why the bug is closed.

[Zimmi48]

Tagging as help wanted because I'm guessing the lack of response from @tchajed means that he doesn't really want to spend more time on this.

[tchajed]

Ok, I checked the new list of resolved bugs in opened/. Here are the details from manually checking each bug:

• setoid_rewrite in lambda-abstraction. #1501: example was invalid, but added Matthieu Sozeau's example (with a small fix for implicits).
• "Anomaly: Uncaught exception Option.IsNone. Please report." on [induction] #2814: still fails, but not with an anomaly (added an Undo to try to trigger the bug)
• Uncaught exception: Not_found when defining idtoeqv with an omitted argument to the eliminator. #3209: removed duplicate copy in bugs/opened/
• Anomaly: error with no safe_id attached: Uncaught exception Stm.Vcs_aux.Expired.. Please report. #3320: still fails, but not with an anomaly
• Uncaught exception Tacred.Redelimination with Hint Resolve #3916: removed duplicate copy in bugs/opened
• Error: in _: Conversion test raised an anomaly #3100: still fails, but not with an anomaly
• Anomaly: unknown constant in Print Assumptions #3948: removed duplicate copy in bugs/opened
• dependent destruction: Error: catchCommuteDetails is used in hypothesis X. #2456: fixed, and amended slightly
• Regression caused by universe polymorphism -- interaction with canonical structures? #3230: fixed, example works
• Anomaly: Evar ?X11 was not declared. Please report. ([admit] in the typeclass database loses evars?) #3938: fixed, example works

not addressed:

• [typeclasses eauto with core] can't solve some goals that [eauto] can #3794: the bug report says the behavior is buggy and it hasn't changed - I think this bug should remain open
• [abstract] typeclass resolution hints give very strange behavior (and an abundance of Anomaly: Uncaught exception Not_found. Please report.) (regression since 8.4) #4781: clearly still open, due to a regression
• [apply with] broke in v8.5 (regression since 8.5pl1, 8.4) #4813: indeed goes through with Program, but not otherwise - was this ever fixed?

[mattam82]

This looks fine to me, indeed the changes to 1501 are alright. For issue #4813 this is another instance where a bidirectional typechecking flag or something more general to control inference would be useful.

[Zimmi48]

There is no code owner for the test-suite (maybe for the same reason that there is no code owner for CHANGES). @maximedenes do you want to take care of this PR?

[Zimmi48]

@mattam82 Since you approved this and it has no owner, will you take care of merging it?
@tchajed Can you rebase? It should be straightforward.

[tchajed]

Rebased.

[maximedenes]

I'll merge, since this has been approved.