Merge v2.1.1 into master
#2473
Merge v2.1.1 into master
#2473
Conversation
* Simplify more `Data.Product` import to `Data.Product.Base` * Simplify more `Data.Product` import to `Data.Product.Base` * Indent
A useful improvement to consistency of names,
* `find*` functions for `Data.List` both decidable predicate and boolean function variants * Back to `Maybe.map` * New type for findIndices * Add comments * Respect style guide --------- Co-authored-by: jamesmckinna <[email protected]>
Ahead of a proper review, I have been testing recent PRs against both v2.6.4.3 and v2.7.0, so hopefully any eventual merge of this PR will be a painless transition... ;-) |
There was a problem hiding this comment.
This all looks fine, modulo the structure of CHANGELOG and some of the additional textual suggestions, but none is (I think!) a deal-breaker.
My only thought is that we perhaps try to clear the other remaining non-DRAFT open stdlib-v2.2/agda-v2.6.4.3 PRs (or else: as much of the v2.2 milestone as we can agree upon ;-)) before merging this one, in the interests of marking a clean 'break' between Agda versions? Or, at least, that we discuss this among the maintainer core team before proceeding (ie. observe more than the '2 approvals' rule)?
| @@ -76,11 +76,11 @@ jobs: | |||
| if [[ '${{ github.ref }}' == 'refs/heads/experimental' \ | |||
| || '${{ github.base_ref }}' == 'experimental' ]]; then | |||
| # Pick Agda version for experimental | |||
| echo "AGDA_COMMIT=4d36cb37f8bfb765339b808b13356d760aa6f0ec" >> "${GITHUB_ENV}"; | |||
| echo "AGDA_COMMIT=18cc53941e924b144c0f1f3953280ef726009f7e" >> "${GITHUB_ENV}"; | |||
There was a problem hiding this comment.
I haven't verified that these are the correct commit hashes!
(But, for info: how could/should I, were I to want to?)
|
Consider also rolling the typo change |
|
@MatthewDaggitt @jamesmckinna Would be great the see this being merged quickly, because:
Or maybe I am wrong here and you can advise me a better workflow. |
|
@andreasabel I'm not trying to get in the way, indeed I'm happy to go ahead and merge, but currently waiting on a second 'approve' review, and feedback from @MatthewDaggitt on my own round of comments. I guess we can take the first one as read from you (but please do so explicitly), and once Matthew comes back, happy to proceed... Hope this helps! |
bring the date forward to today
|
Two cosmetic patches applied after @andreasabel 's comments, and will merge now. |
This brings across all the changes on
experimentalandv2.1.1-releasebranches ontomaster. Therefore after this is merged everyone working on the library will need to update to v2.7.0 of Agda.