I have a Cubical agda codebase whose CI is failing to build Agda 2.6.4.1 (as well as 2.6.4 and 2.7.0.1). The CI workflows have worked for months and just recently began to fail. I've also forked the cubical repo, and CI fails in all of the exact same spots, so there are no spurious changes from my end.
After digging through all of the logs, I believe this is due to silent change in dependencies for Agda, even though I am trying to build at a pinned commit. The only diff I have found between the last successful build and the more recent failing ones is the version of happy-lib. In my most recent run happy-lib-2.1.1 vs happy-lib-2.0.2 on the last successful build.
I think an upper limit on the version for this library should fix the issue, but I am not sure
The specific commands that fail:
git clone https://github.com/agda/agda --branch v2.6.4.1 --depth=1
cd agda
mkdir -p doc
touch doc/user-manual.pdf
cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
cd ..
rm -rf agda
which eventually fails when building the parser
[147 of 429] Compiling Agda.Syntax.Parser.Layout ( src/full/Agda/Syntax/Parser/Layout.hs, dist/build/Agda/Syntax/Parser/Layout.o, dist/build/Agda/Syntax/Parser/Layout.dyn_o )
[148 of 429] Compiling Agda.Syntax.Parser.Parser ( dist/build/Agda/Syntax/Parser/Parser.hs, dist/build/Agda/Syntax/Parser/Parser.o, dist/build/Agda/Syntax/Parser/Parser.dyn_o )
dist/build/Agda/Syntax/Parser/Parser.hs:8776:12: error:
Error: Not in scope: ‘Prelude.null’
Suggested fixes:
• Perhaps use one of these:
‘Prelude.all’ (imported from Prelude),
‘Prelude.not’ (imported from Prelude),
‘Prelude.sum’ (imported from Prelude)
• Perhaps you want to remove ‘null’ from the explicit hiding list
in the import of ‘Prelude’
(dist/build/Agda/Syntax/Parser/Parser.hs:42:1-30).
|
8776 | if Prelude.null catch_frames_new
| ^^^^^^^^^^^^
dist/build/Agda/Syntax/Parser/Parser.hs:8787:13: error:
Error: Not in scope: ‘Prelude.null’
Suggested fixes:
• Perhaps use one of these:
‘Prelude.all’ (imported from Prelude),
‘Prelude.not’ (imported from Prelude),
‘Prelude.sum’ (imported from Prelude)
• Perhaps you want to remove ‘null’ from the explicit hiding list
in the import of ‘Prelude’
(dist/build/Agda/Syntax/Parser/Parser.hs:42:1-30).
|
8787 | Prelude.null (Prelude.filter (\(HappyCons _ (HappyCons h _),_) -> EQ(st,h)) catch_frames)
| ^^^^^^^^^^^^
All occurring on Ubuntu 22.04.5 LTS, cabal 3.6.2.0, ghc 9.4.7
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4