agda
Set the fixity of mixfix definitions
Using the new -Wall option which I have just introduced, I have
found a lot more mixfix definitions which do not come with a fixity
declaration:
https://gist.github.com/gallais/79386a6ba8826620dc82b3f5d5af2bde
Well, bracketing constructs like [_] or [_,_] do not need a fixity, in fact, since they are neither pre/post nor infix operators, a precedence or associativity value for these does not make sense.
The warning mechanism should be adapted to disregard these.
I've updated the gist with the new set of warnings ignoring well-bracketed mixfix decls
As of Agda 2.6.0 the warnings for the missing fixities should now work properly, so this should be much more doable.
Particularly egregious example in Relation.Binary.Construct.NonStrictToStrict
@gallais can you update the gist please? I think I'm going to spend some of my time working on this.
@JacquesCarette It's just a matter of running agda on Everything with -Wall.
Hi, (I don't know if I am doing it right) I ran -
agda -Wall Everything.agda
locally, but could not reproduce the list of warnings, instead I got an error saying -
/Users/saransh/Code/Mitacs/agda-stdlib/Everything.agda:11,8-18
The name of the top level module does not match the file name. The
module Everything should be defined in one of the following files:
/Users/saransh/Code/Mitacs/agda-stdlib/src/Everything.agda
/Users/saransh/Code/Mitacs/agda-stdlib/src/Everything.lagda
/opt/homebrew/Cellar/agda/2.6.3/libexec/ghc-9.4.4/Agd-2.6.3-d4728884/share/lib/prim/Everything.agda
/opt/homebrew/Cellar/agda/2.6.3/libexec/ghc-9.4.4/Agd-2.6.3-d4728884/share/lib/prim/Everything.lagda
Should I be running agda on something else or with some additional flags? Thanks!
An updated list for reference (will create a PR shortly) - https://gist.github.com/Saransh-cpp/99476398a0bf6fa78f1fc6a26edbb9fc
I hope that @Saransh-cpp was using README/Design/Fixity.agda to set the fixities (I thought a reference to that file was here in the comments, but not so, only inside the linked PR).
Ah I'd forgotten that even existed! Maybe that belongs in the style guide rather than an Agda file?
Anyway @Saransh-cpp, just to check does your PR follow these suggestions? :smile:
If you're happy to "bless" this fixity guide then yes, probably should be integrated into the style guide.
I've added the missing fixity for most of the declarations, but I could not really figure out the fixity for some of them. This gist has an updated list of missing fixities that I could not add (there might be repetitions). I'd be happy to add them in if someone could help me with the values. Thanks!
Edit: Updated list of missing fixities - https://github.com/Saransh-cpp/IdrisButNotAgda/tree/fixities
I will attempt to look at the gist seriously as soon as I can. Still buried with many other things on my plate.
@JacquesCarette does/did #2386 also update README.Design.Fixity to reflect the recent additions/adjustments? (It's on me in my review for not having chased this up until now...)
The remaining 50-odd definitions without a fixity (mostly under Function and Relation...) seem much less readily to admit a classification/categorisation with 'obvious' precedences... anyone care to have a go, or should we pick a default (20, say) and go with that?
Yes, #2386 did update the documentation. I was going to continue slowing picking at this issue until it's done. Yes, it is getting trickier!