search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
362 stars 68 forks source link

make it work with the agda stdlib v2.0 (c12568c64) #352

Closed cmcmA20 closed 8 months ago

cmcmA20 commented 2 years ago

^subj

MatthewDaggitt commented 2 years ago

A heads up that v2.0 is not released so I wouldn't recommend merging this in, unless you want your users to have to upgrade to the unstable library version.

cmcmA20 commented 2 years ago

Let it chill until then, I will update it after release.

JacquesCarette commented 1 year ago

I think that release of v2.0 might be pretty soon, so it might be worth revisiting this now-ish to be ready for it.

cmcmA20 commented 1 year ago

Tested with agda master 269204b682 Works on agda-stdlib master 7c5f3ff90

JacquesCarette commented 1 year ago

Thanks. [Note: there seems to be two outstanding conflicts?]

cmcmA20 commented 1 year ago

Sorry I forgot to rebase, now it's fine. agda-lib file conflict can't be resolved, I tested only 2.0 and not 1.7.2. Do you wanna wait for 2.0?

JacquesCarette commented 1 year ago

Very nice work - I will take it in as soon as 2.0 becomes live.

It would be nice to have the same setup here as stdlib does (i.e. have an experimental branch where this could go in right away), I've just never had the time to prep the infrastructure.

JacquesCarette commented 8 months ago

So now that stdlib 2.0 is 'essentially' live, it would be nice to revisit this. Looks like things have broken since this was last looked at.

cmcmA20 commented 8 months ago

The changes are extensive, I'll take a look during the weekend.

JacquesCarette commented 8 months ago

If you give me permission to push to your branch, I can help.

JacquesCarette commented 8 months ago

In the end, 64 different places needed to be fixed to push things to 2.0, and this was done in #406 which has been merged. So this one is no longer needed - but keep PRs coming!