Misc cleanups and improvements

[ibbem]

These are mostly just some simple cleanups left on my TODO list.

The exception is 47321e3 which updates Agda and the standard library. I think that's a good idea because, first of all, this will hopefully get rid of some bugs we encountered. We might also get some other improvements (e.g. a performance improvement on NixOS). And lastly, this is probably better for the first impression: When people look at a library and it already uses some outdated dependencies, it leaves the impression that the library is already unmaintained.
The most incompatibilities I encountered where:

• Enabling --large-indices because we make use of it in some places (it was implicitly enabled by default before).
• Changing _≡˘⟨_⟩_ to the new syntax _≡⟨_⟨_ (the standard library changed this for a nice alignment and symmetry)

Related to 8fa5f9f: Should we rename EPVL to something else? I think this name stands for the old paper title "Expressive Power of Variability Languages" right?

Should the README include an example for how to use this library as a dependency in Nix (ba2a8f0)?

[pmbittner]

Hi @ibbem,

thank you for this pull request. Your changes are highly appreciated. :) I left some comments and questions below.

[pmbittner]

Also, I am unsure about the large-indices flag. Where exactly is it needed? I searched for it in the Agda documentation but its description was quite abstract so I did not really understand why we need it.

[pmbittner]

Should we rename EPVL to something else?

Yes we should do. I am currently still thinking about a proper name. :(

[pmbittner]

Should the README include an example for how to use this library as a dependency in Nix (ba2a8f0)?

That would be great! We probably need such an example / setup instructions for a potential artifact submission later on.

[ibbem]

The option --large-indicies is needed for most of our languages because of the 𝕍 argument. A minimal example is

Index : Set₁
Index = Set → Set

data Example : Index → Set where
  value : ∀ i → Example i

Here, Example is rejected because Index : Set₁ whereas Example only constructs a type in Set. This was previously allowed but an inconsistency was discovered and the Agda team decided to disable --large-indicies by default (which was also introduced because of that inconsistency). See agda/agda#6661 for details.

I just noticed that the option which conflicts with --large-indicies is actually still enabled 😅. Unfortunately, we cannot enable --safe to check for such inconsistencies because we use --sized-types.

We can either avoid --large-indicies by refactoring (I have no idea yet how complicated this will get) or add --no-forced-argument-recursion (the option which avoids the inconsistency) where we use --large-indicies. Maybe it's also a good idea to move most options to the .agda-lib file which applies the options to the whole project.

[pmbittner]

Ok interesting. Maybe that is a reason to avoid 𝕍 then and to specialize it to Rose for most definitions. 🤔 Maybe, we can keep 𝕍 in the framework, where most types are somewhat meta (Set_1) but always specialize it for languages and proofs. This is actually how we do it in the paper. For example, CCC semantics would then always produce a Rose tree.

The idea to add the options to the library file sounds good to me.

Someone should build an explicit feature model for Agda. :D

[pmbittner]

You can merge when you think the PR is ready. :) Some items in our discussion might be better suited for future PRs.