Skip to content

`build-master` job succeeds even when Agda fails to compile

While scrolling through this recent build-master CI log from the master branch, I noticed that Agda-2.6.1.3 was failing to compile:

Building executable 'agda' for Agda-2.6.1.3..
[1 of 2] Compiling Main             ( src/main/Main.hs, dist/build/agda/agda-tmp/Main.o )
[2 of 2] Linking dist/build/agda/agda
Installing executable agda-mode in /root/.cabal/store/ghc-9.3.20220301/incoming/new-6881/root/.cabal/store/ghc-9.3.20220301/Agda-2.6.1.3-67e795e6c172ad05e0614bd3ad0ca692fe7d41c5a11f3ead860e5b1538bf91e7/bin
Warning: The directory
/root/.cabal/store/ghc-9.3.20220301/incoming/new-6881/root/.cabal/store/ghc-9.3.20220301/Agda-2.6.1.3-67e795e6c172ad05e0614bd3ad0ca692fe7d41c5a11f3ead860e5b1538bf91e7/bin
is not in the system search path.
Installing library in /root/.cabal/store/ghc-9.3.20220301/incoming/new-6881/root/.cabal/store/ghc-9.3.20220301/Agda-2.6.1.3-67e795e6c172ad05e0614bd3ad0ca692fe7d41c5a11f3ead860e5b1538bf91e7/lib
Installing executable agda in /root/.cabal/store/ghc-9.3.20220301/incoming/new-6881/root/.cabal/store/ghc-9.3.20220301/Agda-2.6.1.3-67e795e6c172ad05e0614bd3ad0ca692fe7d41c5a11f3ead860e5b1538bf91e7/bin
Warning: The directory
/root/.cabal/store/ghc-9.3.20220301/incoming/new-6881/root/.cabal/store/ghc-9.3.20220301/Agda-2.6.1.3-67e795e6c172ad05e0614bd3ad0ca692fe7d41c5a11f3ead860e5b1538bf91e7/bin
is not in the system search path.
/builds/ghc/head.hackage/ci/run/test-Agda-2.6.1.3/dist-newstyle/tmp/src-6881/Agda-2.6.1.3/src/data/lib/prim/Agda/Builtin/Char/Properties.agda:11,36-69
Could not parse the application primCharToNat a ≡ primCharToNat b
Operators used in the grammar:
  ≡ (infix operator, level 4) [_≡_ (/builds/ghc/head.hackage/ci/run/test-Agda-2.6.1.3/dist-newstyle/tmp/src-6881/Agda-2.6.1.3/src/data/lib/prim/Agda/Builtin/Equality.agda:7,6-9)]
when scope checking primCharToNat a ≡ primCharToNat b
Error: Failed to typecheck /builds/ghc/head.hackage/ci/run/test-Agda-2.6.1.3/dist-newstyle/tmp/src-6881/Agda-2.6.1.3/src/data/lib/prim/Agda/Builtin/Char/Properties.agda!
Generating Agda library interface files...
... /builds/ghc/head.hackage/ci/run/test-Agda-2.6.1.3/dist-newstyle/tmp/src-6881/Agda-2.6.1.3/src/data/lib/prim/Agda/Builtin/Bool.agda
... /builds/ghc/head.hackage/ci/run/test-Agda-2.6.1.3/dist-newstyle/tmp/src-6881/Agda-2.6.1.3/src/data/lib/prim/Agda/Builtin/Char.agda
... /builds/ghc/head.hackage/ci/run/test-Agda-2.6.1.3/dist-newstyle/tmp/src-6881/Agda-2.6.1.3/src/data/lib/prim/Agda/Builtin/Char/Properties.agda
cabal: Failed to build Agda-2.6.1.3 (which is required by test-Agda-1.0). See
the build log above for details.

Despite this, the CI reports the job having succeeded! This is concerning, since I wouldn't have noticed this if it weren't for a careful reading of the logs.

I'm not sure how long this has been going on for. I wonder if !203 (merged) affected the build-failure-counting logic somehow.