Alex Rice

How would pinning a version in stackage work? I assume this would need to be done upstream. I am not quite sure how this generates problems with maintance, as wouldn't...

There is a line https://github.com/commercialhaskell/stackage/blob/e96f08afccf1112598816a47cc9c52b4600cead6/build-constraints.yaml#L2347 here however I guess the `< 0` is saying not to build it? Also are you suggesting adding multiple versions of the same package to...

How does this allow multiple versions to be built?

Just to check, the issue with pinning an old version here is that eventually the dependencies will update versions and could break the pinned version, and the pinned version would...

Did you find a solution for this? I've been having the same error (also on nixpkgs unstable)

> Perhaps one could make Agda keep track of whether `-Werror` would have made Agda reject the code. Then code that would not have been rejected could be made compatible...

Ah I reread what you said and that makes sense now. This would seem to fix the problem. Another solution could be for `-Werror` to not propagate into libraries, though...

> This didn't seem to be a thing in agda 2.6.1.2 Just checked and this likely is a thing in agda 2.6.1.2 but cubical only added -Werror to their build...

`-W error` feels slightly different to something like `--auto-inline` or `--without-K` as my guess is that `-W error` shouldn't fundamentally change the way type checking is done, and only reject...

Should probably be noted that a potential half-way solution for this would be to allow the results of different typechecks to be stored, so that if you type check `A.agda`...