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