Skip to content

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