Reflection API changing in Agda 2.6.3

[andreasabel]

The current master of cubical does not build with Agda master, breaking here:

cubical/Cubical/Reflection/Base.agda

Line 51 in 43e0bf0

extend*Context (a ∷ as) tac = R.extendContext a (extend*Context as tac)

extendContext expects one more argument now:

extendContext    : ∀ {a} {A : Set a} → String → Arg Type → TC A → TC A

Agda's reflection API changed in agda/agda#5715 (unreleased, scheduled for Agda 2.6.3).

Maybe you should maintain a branch that builds with latest Agda master. This branch could be merged into master once you bump to a new release of Agda (from master). Currently we (Agda devs) cannot really test (from the Agda side) whether cubical and Agda are still in sync. If such a branch existed, we could pin our cubical submodule to this branch and run Agda on it from our testsuite/CI.

[andreasabel]

Looks there was some effort to move to a more recent version of Agda, but it was reverted:

• [ ci ] Use the latest Agda but check cubical without NoEquivWhenSplitting warnings #697
• Revert "[ ci ] Use the latest Agda but check cubical without NoEquivWhenSplitting warnings" #701

[mortberg]

Ah, yes indeed the current version of the library is supposed to build on the latest release of Agda to not force us to update our Agda installations all the time when working on the library. Having a branch that builds on Agda master would indeed be ideal. How about calling it Agda-master or something?

[MatthewDaggitt]

If you wanted to be consistent with the standard library, we call it experimental (see our docs)

[andreasabel]

@mortberg @MatthewDaggitt

If you wanted to be consistent with the standard library, we call it experimental (see our docs)

Maybe standard-library could rename it to Agda-master instead?
experimental is ambiguous, and quite frankly, I am often confused. It could refer to experimental features either in Agda or the standard-library...
Agda-master is a clearly purposed name.
(Too bad git doesn't (allow to) attach comments to branches.)

[L-TChen]

Having a branch that builds with the latest development version of Agda is ideal, but for this issue, it also makes sense to remove extend*Context (#745).

[felixwellen]

This is outdated by now, cubical typechecks with agda 2.6.3