CI fails when invoking `happy` on Agda's `Parser.y` file
If you try to add Agda to head.hackage naïvely, the CI will fail when trying to preprocess the Parser.y file with happy, as seen in this failed CI job:
happy: src/full/Agda/Syntax/Parser/Parser.y: hGetContents: invalid argument (invalid byte sequence)
In order to add Agda-2.6.1.3 to head.hackage, I had to work around this issue by hackily remove all Unicode characters from Parser.y. See commit 6d0a6c46. Unfortunately, this workaround doesn't scale, as Agda-2.6.2's Parser.y features a use of Unicode that cannot be easily replaced:
onlyErased' a = case theAttr a of
...
QuantityAttribute q -> case q of
...
Quantityω o -> return $ Just (NotErased o)
That single ω character is the reason why Agda-2.6.2 currently cannot pass through head.hackage's CI. This issue serves as a reminder to figure out why this is and to fix the issue in CI properly.
Edited by Ryan Scott