Closed treeowl closed 3 years ago
you could try adding some cabal install agda --constraint 'boxes installed'
somewhere at the end, however, you'll risk getting false positives if agda
(or some other build-dep of agda
breaks)
@hvr, thanks. Is there a way to make it only do that for the latest released GHC? I don't want to burn a bunch of time with all that for every version.
As of today (2019-08-20), we are using Boxes, besides for printing debug messages and benchmark statistics, only for printing the OperatorInformation
error. Part of the code is this:
https://github.com/agda/agda/blob/5751371fd442fb19cf41f7a8a878dc1aa80050fe/src/full/Agda/TypeChecking/Errors.hs#L958-L983
That is to say, the exact rendering of the boxes is not so critical, and I suppose the basic correctness is tested by your build matrix already? (Otherwise, you might be able to extract a test case manually from the code in Agda.TypeChecking.Errors
!?)
There's full matrix of GHC-7.0...
Agda is by far the most important package depending on this one; I want to be aware of any breakage in Agda builds induced by future changes here. I don't know how to set that up, and I don't know if it's possible to do it cheaply enough, but it would be very nice.