Basic porting questions

Stream: mathlib4

[Anatole Dedecker]

Hi everyone! After successfully porting a rather trivial file in mathlib4#582, I started working on a port of control.basic (yes, I'm starting from files low in the priority queue in order not to block too much people while I learn how to port efficiently), and I have a few small questions:

• if I understand correctly, simp attributes can no longer be used in the file where they are declared, is that right? If so, what is the expected solution for that? To be more explicit, I'm thinking about docs#simp_attr.functor_norm, which is used multiple times in control.basic (note: it also seems to be used in control.functor, so it looks like some transitive import through tactic is ignored by the port_status script). Should I create an intermediate file just for introducing the simp attribute?
• what is the current attitude regarding small mismatches in the order of implicit arguments? Most of the dubious translation messages from mathport seem to be reporting this sort of inconsistencies, and I'm not sure if we want to fix them or consider that we only need to ensure the order of explicit arguments
• more specific to control.basic: the docs#fish operator is already defined in the core library as docs4#Bind.KleisliRight, and the precedence issue mentioned in this comment seems to no longer apply, so I'll just be removing the definition. Should I change the names of the following lemmas to replace fish by KleisliRight?

[Anatole Dedecker]

I opened a WIP PR as mathlib4#588 if anyone wants to have a look

[Heather Macbeth]

After a porting PR is merged, should I as the author update the port status from

No: PR mathlib4#585

to

Yes: PR mathlib4#585

? Or is this something that should be left to the porting leaders?

Same question about how to "verify" that the file is ported.

[Scott Morrison]

Yes, it's helpful if you check that, although I'm trying to remember to do it as I bors merge as well. It's still a bit of a mess, sadly.

[Scott Morrison]

The verification step has so far not been happening at all. :-(

[Heather Macbeth]

OK, I made the update for that one, and I will keep an eye out for any announcements about changes to the workflow :)