[ bug ] missing commits from v2.0 onwards

[jamesmckinna]

The current version(s) (v2.0 through v2.3, master) no longer seem to have @Taneb 's commits from the ostensibly-merged #1913 . What's happened to them? What else might be missing? There are 508 merged PRs since 2021-07-01 (beginning of v2.x version line)... sigh. Any way we can automate checking what's missing?

From 2023-04-17 (a day of infamy), each my fault (hash refers to the offending revert commit; PR to the missing merged commits)

• opposite of a Ring [clean version of pr #1900] #1910 commit ccd9677
• punchOut preserves ordering #1913 commit bb73b03
• Wellfounded proof for sum relations #1920 commit 18ae346
• two whitespace violations #1922 commit 46e4477

I hope that's it! 🤦
UPDATED: The guilty party is me; the guilty PR is #1926 , and otherwise I think is localised to that bit of the commit history.

How do I/we undo this mess?

[jamesmckinna]

Heroic effort by @JacquesCarette on #2794 ! Many thanks!