What to do about reverted PRs and compatibility with 2.6.2

[mortberg]

@L-TChen I just reverted two of your PRs:

#701
#702

as they broke compatibility with 2.6.2 which is the current version we're using to develop the library. I hope this won't cause any new problems with the CI.

Before merging any PRs that break compatibility with 2.6.2 we should discuss if we want to do this. I don't think we should do this as it's such a headache to make sure that everyone is using the same version of Agda and it's much easier if we're all just using the latest official release. Once 2.6.3 is out we can update the library

[L-TChen]

It is not just agda/cubical itself but also agda/agda is checking cubical as part of CI. So, if the library on the master is not compatible with the master branch of agda/agda, the Agda's CI will break too.

I can think of at least two possible "solutions"

1. Ignore cubical entirely during Agda's CI.
2. Create an experimental branch like the standard library agda-stdlib so that the master maintain the compatibility with 2.6.2 and the experimental branch accumulate commits compatible with the lastest commit, i.e. 2.6.3 but the stable release 2.6.2.

[Saizan]

We could have an experimental branch, but in the past Agda developers with that problem just made an ad-hoc branch to reference from agda/master. It worked fine enough since you have to specify a commit for the git submodule system anyway, and not a branch.

[L-TChen]

Agda developers with that problem just made an ad-hoc branch to reference from agda/master.

If Agda 2.6.3 has breaking changes which are not compatible with any commit on agda/cubical, then it won't work.

In this particular case, though, agda/cubical defines

cubical/Cubical/Reflection/Base.agda

Lines 49 to 51 in 1c56f58

	extend*Context : ∀ {ℓ} {A : Type ℓ} → List (R.Arg R.Type) → R.TC A → R.TC A
	extend*Context [] tac = tac
	extend*Context (a ∷ as) tac = R.extendContext a (extend*Context as tac)

which is not used anywhere else. It is safe to remove this function so that the agda/agda on the master branch can still check agda/cubical without any issue.

However, IMO it is wise to have a branch like experimental to check if the cubical library is compatible with the latest Agda.

[Saizan]

I meant an ad-hoc branch of agda/cubical, containing the commit that agda/master can reference.

But I guess let's agree to call that branch experimental, so that if there are multiple compatibility changes to make they are collected in one place, and cubical developers can merge it into master when the new Agda version releases.

We should probably write about this in CONTRIBUTING.md

[L-TChen]

Aha, I see. Thanks for the clarification.

We should probably write about this in CONTRIBUTING.md

That will be nice. I looked for guidance in vain and every release of agda/cubical targets at a different version of Agda made me believe that the master branch is for the next release of Agda.

[xekoukou]

I too believed that the master branch was for the latest agda.

cubical/INSTALL.md

Line 4 in 1c56f58

The cubical library should compile on the latest development version

cubical/README.md

Line 4 in 1c56f58

This library compiles with the master branch of the development

[Saizan]

I think it's been for the latest agda for a while, but currently there are not as many cubical changes going on so the incentives are reversed.

[mortberg]

I agree that making changes that keeps the library compatible with both Agda master and the latest release is the best (so @L-TChen can feel free to comment or remove the code that causes problems). If this is not possible I think that having an experimental branch would be good.

As @xekoukou notes the documentation needs to be updated to reflect that the master branch of the library is now mainly intended to work on the latest release of Agda. I'm super busy these days, so can someone else make a PR with this change before we forget?

[felixwellen]

#717 at least made changes to README and INSTALL, updating the phrase 'latest development version of Agda' with' to 'latest official release of Agda'. I guess there might still be other places that need some changing.

[mortberg]

Thanks! Closing this now