unknown attributes

Stream: mathlib4

[Rémy Degenne]

I ported data.nat.log in mathlib4#1089 but I had to comment out two attributes which were unknown: pp_nodot and mono. What should I do about those?
Should the PR wait for a mono tactic (only the attribute is used here, not the tactic itself)? That might be one of the tactics that should be replaced by an aesop rule set? (although mono is usually non-finishing, so perhaps not)
As for pp_nodot, I don't even know what it does in lean 3.

[Johan Commelin]

pp_nodot is an instruction for the pretty printer to not use dot-notation.

[Moritz Doll]

I had the same thought about mono a few days ago:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Tactic.20porting.20assignments/near/316258985

I am still trying to port data.fin.basic, which seems to be very high priority, but after that I might take a look at porting mono (if no one else wants to do it).

[Rémy Degenne]

Then I'll mark the PR as WIP until mono is ported or it becomes blocking for something urgent (which seems unlikely).

[Moritz Doll]

if it is only the attribute, then you can just leave a porting note

[Rémy Degenne]

Right. I've done that. The PR is ready for review then.

[Ruben Van de Velde]

Should it be clog or cLog?

[Scott Morrison]

Moritz Doll said:

I had the same thought about mono a few days ago:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Tactic.20porting.20assignments/near/316258985

I am still trying to port data.fin.basic, which seems to be very high priority, but after that I might take a look at porting mono (if no one else wants to do it).

I would suggest trying to build this on top of solve_by_elim.

[Scott Morrison]

(Post #856, which I really need to finish, unless someone else wants to help. :-)

[Heather Macbeth]

mathlib4#856 in case anyone else wondered :)

[Heather Macbeth]

Scott Morrison said:

I would suggest trying to build this on top of solve_by_elim.

For @Moritz Doll or anyone thinking of implementing mono on top of solve_by_elim: I think this is blocked by mathlib4#856 (providing a .noBackTracking option), because mono is not a finishing tactic and therefore has to have deterministic end state. Jannis already made this point in discussion whether mono could be implemented on top of aesop:

Jannis Limperg said:

After a quick look at mono, it seems like Aesop could probably replace terminal mono* calls, but not non-terminal mono calls.