cubical
cubical copied to clipboard
agda
Reflection API changing in Agda 2.6.3
The current master of cubical does not build with Agda master, breaking here:
https://github.com/agda/cubical/blob/43e0bf07f06bc4a713f3c55d97a13922b426813e/Cubical/Reflection/Base.agda#L51
extendContext expects one more argument now:
extendContext : ∀ {a} {A : Set a} → String → Arg Type → TC A → TC A
Agda's reflection API changed in https://github.com/agda/agda/issues/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.
Looks there was some effort to move to a more recent version of Agda, but it was reverted:
- #697
- #701
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?
@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.)
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).
