Set the fixity of mixfix definitions

[MatthewDaggitt]

Set the fixity of <? in Data.Nat.Properties.

[MatthewDaggitt]

Closed with 5f4c67e

[gallais]

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

[andreasabel]

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.

[gallais]

I've updated the gist with the new set of warnings ignoring well-bracketed mixfix decls

[MatthewDaggitt]

As of Agda 2.6.0 the warnings for the missing fixities should now work properly, so this should be much more doable.

[MatthewDaggitt]

Particularly egregious example in Relation.Binary.Construct.NonStrictToStrict

[JacquesCarette]

@gallais can you update the gist please? I think I'm going to spend some of my time working on this.

[gallais]

@JacquesCarette It's just a matter of running agda on Everything with -Wall.

[Saransh-cpp]

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!

[gallais]

You're probably missing -i .

[Saransh-cpp]

Ah, thanks! Works!

[Saransh-cpp]

An updated list for reference (will create a PR shortly) - https://gist.github.com/Saransh-cpp/99476398a0bf6fa78f1fc6a26edbb9fc

[JacquesCarette]

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).

[MatthewDaggitt]

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? 😄

[JacquesCarette]

If you're happy to "bless" this fixity guide then yes, probably should be integrated into the style guide.

[Saransh-cpp]

Oops, just saw the comments. I was indeed following the design guide!

[Saransh-cpp]

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

[JacquesCarette]

I will attempt to look at the gist seriously as soon as I can. Still buried with many other things on my plate.

[jamesmckinna]

Can the (updated) list be sorted, please?

[Saransh-cpp]

Should be sorted now!

[jamesmckinna]

@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...)

[jamesmckinna]

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?

[JacquesCarette]

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!