search

agda / agda-categories

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

ramp up stdlib version? #371

Open HuStmpHrrr opened 1 year ago

HuStmpHrrr commented 1 year ago

The current release is 1.7.2.

JacquesCarette commented 1 year ago

Yep, definitely should do. Not sure when I'll get time, right now is scarily busy for me.

jpoiret commented 1 year ago

At least from my testing, the library type-checks fine with the newer Agda and stdlib versions. #372 is a simple PR to update the requirements, I didn't know what to do with the README since it refers to the latest release.

HuStmpHrrr commented 1 year ago

I think we can make a small release to match the agda and stdlib version?

JacquesCarette commented 1 year ago

Yes, we can. @HuStmpHrrr if you have the time to do it, please do so. I may not get to it until late this week.

HuStmpHrrr commented 1 year ago

I will wait for the change of the PR and then we are good to go.

andreasabel commented 1 year ago

If you never use cubical, you can stick to 1.7.1, which uses --without-K instead of --cubical-compatible and is thus 20% faster to build. If agda-categories, do you use --without-K or --cubical-compatible? (Or just vanilla (implicit) --with-K?)

jpoiret commented 1 year ago

@andreasabel once the stdlib is fully built, --cubical-compatible doesn't have a performance impact on users of the library, right?

JacquesCarette commented 1 year ago

agda-categories still uses --without-K (and safe). We should also add --exact-split, but that is almost always a no-op.

andreasabel commented 1 year ago

@andreasabel once the stdlib is fully built, --cubical-compatible doesn't have a performance impact on users of the library, right?

Not if you have unlimited memory with O(1) access. ;-)
Seriously, I have not benchmarked, but --cubical-compatible generates extra definitions and extra clauses, and these reside in memory, so I am positive about some impact, even though I cannot put a number to it.

ncfavier commented 1 year ago

Do I understand correctly that it's not possible to import agda-categories (which uses --without-K) from a --cubical module in Agda 2.6.3? This used to be possible in 2.6.2.

andreasabel commented 1 year ago

That is correct: https://agda.readthedocs.io/en/v2.6.3/language/cubical-compatible.html#cubical-compatible

Note that code that uses (only) --without-K can not be imported from code that uses --cubical.

So yes, switching to Agda 2.6.3 without bumping --without-K to --cubical-compatible will be a regression, as the library is not usable anymore from --cubical then.

I should retreat my suggestion until we have an easy way (e.g. via library-wide flag) to bump a --without-K library to --cubical-compatible.

HuStmpHrrr commented 1 year ago

maybe we can set a library-wide flag in the lib file? I think we have a few files that actually uses with-K, if flags in the file overrides the flags in the lib file, then I think we just set --cubical-compatible globally.

andreasabel commented 1 year ago

we have a few files that actually uses with-K, if flags in the file overrides the flags in the lib file, then I think we just set --cubical-compatible globally.

Yes, this is exactly what I want to change in Agda, that you can override --cubical-compatible by --with-K. Currently, Agda does not allow you to do that.

JacquesCarette commented 1 year ago

I want to do some proper benchmarking to see the effect of using --cubical-compatible. It depends on where the new code gets automatically added. If it's mostly for data, then it should be minimal. But if records change too, I'm afraid that the performance changes might be substantial.