agda / agda-categories

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

Release that's compatible to stdlib 1.7? #287

Closed ice1000 closed 3 years ago

ice1000 commented 3 years ago

Is there going to be this thing

gallais commented 3 years ago

A good first step would be to open a PR changing the CI variable to use 2.6.2 and 1.7 and see whether it builds:

https://github.com/agda/agda-categories/blob/fb92ec3789fa07d0a822aa52d9424cadb3b63088/.github/workflows/ci-ubuntu.yml#L47-L49

JacquesCarette commented 3 years ago

It's going to be a thing, yes. I would be happy to see PRs. My Agda time is mostly being spent on finishing material for a paper, but I can definitely do timely reviews.

Akshobhya1234 commented 3 years ago

I have created a PR #288 as first step. The build is failing with error: Empty `where' block (ignored) in .../NaturalTransformation/NaturalIsomorphism/Monoidal/Braided.agda Error: Process completed with exit code 42.

I need help on how to resolve the issue.

gallais commented 3 years ago

Have you tried removing the empty where block?

Akshobhya1234 commented 3 years ago

Have you tried removing the empty where block?

@gallais Thanks! The build is now successful. Do I need to update in README.md?

turion commented 3 years ago

Do I need to update in README.md?

Yes I think this makes sense in general.

turion commented 3 years ago

Is there going to be a git tag and a release? This would be great, because otherwise it might be broken on nixpkgs: https://github.com/NixOS/nixpkgs/pull/130424#issuecomment-885563001

turion commented 3 years ago

Yes I think this makes sense in general.

See https://github.com/agda/agda-categories/pull/293

JacquesCarette commented 3 years ago

Shoot, I cut the release before I merged that in... I guess I'll do another. Sigh.

JacquesCarette commented 3 years ago

Done.