If you package too many versions of a library, the configuration space may blow up. Most configurations are thus untested and quality of the package set decreases.

It is hard to fix InteractionTrees to make it compatible with latest coq-ext-lib? According to the changelog (https://github.com/coq-community/coq-ext-lib/releases/tag/v0.10.3), there are no breaking changes in that version…

Yeah, I noticed it builds against coq-ext-lib 0.10.3, but the author of InteractionTrees warned against it, because they define some notation at level 60:

https://github.com/DeepSpec/InteractionTrees/blob/d408b9151f7f77d1ab0b8a0f2d57f210e16206ae/theories/Core/ITreeDefinition.v#L243-L249

whereas coq-ext-lib changed said notation to level 61:

https://github.com/coq-community/coq-ext-lib/blob/672e63a575c110cf5c76b42172037b0e1a111f39/theories/Structures/Monad.v#L73-L79

The following script:

From ExtLib Require Import Monad.
From ITree  Require Import Simple.
Import ITreeNotations.
Import MonadNotation.

fails with:

Error:
Notation "_ >=> _" is already defined at level 60 with arguments constr at next level, constr at level 60
while it is now required to be at level 61 with arguments constr at next level, constr at level 61.

which is why InteractionTrees has an upper bound to coq-ext-lib at 0.10.2 in its opam configuration.

I agree about removing the excess versions of all packages, but I think w.r.t. this issue we can either:

• package InteractionTrees as it is in this PR,
• only package InteractionTrees-1.0.0 and not the up-to-date,
  until they solve their forward compatibility.

Thanks for clarifying the issue.

Do we need to package two versions of InteractionTrees or one is enough? In which case, which version?

I think we can just package 1.0.0, and I'll possibly add a more recent version when they have a less complex dependency story. I'll change this PR to reflect this.

@vbgl do you have any input on when to phase out support for older Coq versions?

When maintaining them becomes a pain…

Thank you for your contributions.
This has been automatically marked as stale because it has had no activity for 180 days.
If this is still important to you, we ask that you leave a comment below. Your comment can be as simple as "still important to me". This lets people see that at least one person still cares about this. Someone will have to do this at most twice a year if there is no other activity.
Here are suggestions that might help resolve this more quickly:

1. Search for maintainers and people that previously touched the
   related code and @ mention them in a comment.
2. Ask on the NixOS Discourse. 3. Ask on the #nixos channel on
   irc.freenode.net.

Still important to me, I'll update the PR hopefully in the near future!

Closed by #118134.