search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
585 stars 237 forks source link

Reflection.AST.Definition doesn't compile in release candidate #2462

Closed alexarice closed 3 months ago

alexarice commented 3 months ago

Pretty much as described in the title. There's a duplicate infixity, and after fixing that there are some more involved errors which I haven't tried to fix.

alexarice commented 3 months ago

It looks like the "more involved errors" is just me using the wrong version of Agda, though the duplicate fixity definition still makes the build fail for me with Agda 2.7.0

MatthewDaggitt commented 3 months ago

Thanks! I'm confused about how I missed that. I ran the tests before tagging it. Must have been on the wrong branch. I'll create a new one now.

alexarice commented 3 months ago

Is there not a CI pass that runs runhaskell GenerateEverything.hs && agda Everything.agda -i .? Feel like this would catch most issues

MatthewDaggitt commented 3 months ago

There is but until https://github.com/agda/agda-stdlib/pull/2444 is merged in, it didn't get run and I just ran the tests manually. I've just pushed a fix to the v2.1-release branch. Any chance you can quickly try downloading it and seeing if it works for you? I'll then a make a new release candidate.

alexarice commented 3 months ago

Works on my end

MatthewDaggitt commented 3 months ago

Thanks!