CI Failure

[stschaef]

I have Cubical codebase in which I leverage the same workflows as the CI as here. In that repository, the CI started mysteriously failing when downloading and installing Agda.

Moreover, I forked this repository and witness the same CI failures in my fork when using the exact same workflow file as here. Seemingly the Agda parser fails to build. This occurs for me on Agda 2.6.4,2.6.4.1, and 2.7.0.1.

The part I find the strangest is that this workflow had worked previously and then began failing with no change on my end. I would expect this repository to encounter the same issue soon. Any ideas on what might be happening?

[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)
     |             ^^^^^^^^^^^^

[stschaef]

In the Agda build process, even though we're pulling the same commit (2.6.4.1 at 4293e0a) there seems to be a change in the happy lib version.

In my most recent run happy-lib-2.1.1 vs happy-lib-2.0.2 on the last successful run in this repo. This is perhaps then not an issue directly involved with cubical, although this repo could likely be affected by the same problem. I'll test a fresh install of Agda on a VM or something and open an issue in the Agda repo if the issue persists. Unsure if y'all want this issue to remain open or not

[felixwellen]

Keeping us updated is very much appreciated! - I guess we might have the same problem once we switch to a new agda version or the cache is invalidated for some reason.

[felixwellen]

Now the current commit on master seems to fail the CI because of this. I'll try to find a fix. Maybe just by making a new release?

[felixwellen]

I'll just rerun CI, looks like there were upstream fixes.

[maxsnew]

Fixed upstream