Preserve backwards compatibility across Agda versions

[turion]

I get this error message:

Checking Everything (/build/source/Everything.agda).
 Checking Algebra (/build/source/src/Algebra.agda).
/build/source/src/Algebra.agda:8,1-44
Unrecognized option: --cubical-compatible
when scope checking the declaration
  import Algebra

That's probably because the option was just implemented in 2.6.3. Maybe this is intended, but I find it quite difficult to break backwards compatibility so fast.

[MatthewDaggitt]

Hi @turion, this is an excellent point, but unfortunately this is a limitation of Agda itself rather than the standard library. The interface Agda presents has changed, and there's no way facility in Agda to write different code that depends on the version of Agda being used. Therefore, we can't maintain compatibility with the previous version of Agda.

We would use definitely make use that feature if it were available, so if you are keen for this then I would open an issue on the main Agda repo requesting conditional compilation be added.

[turion]

I see, thanks for the explanation! My perspective is as a maintainer for the Agda ecosystem in NixOS. I guess we'll try and update the standard library together with agda in this case then.