ramp up stdlib version?

[HuStmpHrrr]

The current release is 1.7.2.

[JacquesCarette]

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

[jpoiret]

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]

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

[JacquesCarette]

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]

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

[andreasabel]

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]

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

[JacquesCarette]

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

[andreasabel]

@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]

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]

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]

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]

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]

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.