CategoryTheory.Adjunction.Basic

Stream: mathlib4

[Matej Penciak]

The file is almost done in the PR !4#2198. It builds, and all the names have been fixed as far as I can tell

The only issue is the linter is complaining about a bunch of declarations. In particular:

• There are a few def/lemma linter problems. It's saying homEquiv_naturality_right, homEquiv_counit, etc... are defs when they should be lemma/theorems. They're Prop valued, so I agree. But if you look at the file, they are theorems! So I'm a little confused about the linter issue

• A bunch of simpNF linter issues... simpNF issues are a bit over my head if I'll be totally honest, so it may be good for someone else to take a look at those and see what's going on.

[Matej Penciak]

I should also say that in the course of filling in the last sorry I was running into some really weird editor bugs, that I'd be curious to see if other people can reproduce:

In particular, I was filling in the homEquiv_naturality_left_symm' field in adjunctionOfEquivLeft, and I had to manually refresh the server (ctrl + X in VSCode) every time I made a change in order for the infoview to update. Beyond that, it was hard to get the infoview to even display anything unless I had an extra done tactic at the bottom.

[Matej Penciak]

Also an issue I've seen that has been a little annoying in the CategoryTheory files in general has been some pretty-printing issues around Prefunctor. Specifically you see a lot of Prefunctor.obj F.toPrefunctor X or Prefunctor.map F.toPrefunctor f when Lean 3 was totally happy with just displaying F.obj X and F.map f which are a lot easier to parse and understand when seen in the infoview.

This is probably related to the way Lean 3 and Lean 4 differ in terms of structure inheritance, but I was curious if there was any way of getting around this issue for UX purposes (or if it shows up in other mathlib4 files as well).

[Johan Commelin]

@Matej Penciak If the linter is making false claims, please just put

-- Porting note: this linter is making several false claims
set_option linter.someName false

at the top of the file.

[Johan Commelin]

I will take a look at the simpNF issues.
I can't really say anything useful about pretty-printing and editor integration. Maybe someone else can chime in on those.

[Johan Commelin]

Hmm, 6/8 of the simpNF lints are complaining about simp lemmas generated by simps.

[Johan Commelin]

Do we have a policy about what to do in such cases?

[Matej Penciak]

Johan Commelin said:

Matej Penciak If the linter is making false claims, please just put

-- Porting note: this linter is making several false claims
set_option linter.someName false

at the top of the file.

It doesn't seem like the defLemma linter is one of the linters I can turn off. I think I saw in another file it's possible to write attribute [nolint defLemma] ... . Should I do that for each of the declarations it's complaining about?

Also the docBlame linter is unhappy about a lot of Prop-valued class fields that don't have docstrings.

It seems like Lean is generally having a hard time distinguishing between Prop and Type in this file for some reason...

[Matthew Ballard]

You can get rid of the defLemma complaints by removing the restate_axiom's and removing the primes from the fields

[Matthew Ballard]

I have just been appeasing docBlame

[Matthew Ballard]

There are also some instructions for simpNF on the porting wiki.

[Matej Penciak]

Matthew Ballard said:

You can get rid of the defLemma complaints by removing the restate_axiom's and removing the primes from the fields

Will things break down the line removing the restate_axioms?

[Matej Penciak]

The description makes it a little unclear as to how it helps

[Matthew Ballard]

It will break but once you remove all the primes from the field names involved Lean will be happy again.

[Matthew Ballard]

restate_axiom was a Lean 3 workaround that is not needed with Lean 4

[Matthew Ballard]

It looks like all the simpNF complaints are simp can prove this. I tried testing a few to see if it was actually true that simp can prove the statement. It wasn't (for those in my sample). In this case, I would nolint simpNF and add a porting note.

[Matthew Ballard]

Matej Penciak said:

I should also say that in the course of filling in the last sorry I was running into some really weird editor bugs, that I'd be curious to see if other people can reproduce:

In particular, I was filling in the homEquiv_naturality_left_symm' field in adjunctionOfEquivLeft, and I had to manually refresh the server (ctrl + X in VSCode) every time I made a change in order for the infoview to update. Beyond that, it was hard to get the infoview to even display anything unless I had an extra done tactic at the bottom.

Yes. It was challenging. I am using neovim for reference.

[Matej Penciak]

Awesome! Thanks, I'll make those changes

[Matej Penciak]

Hmm, one more wrinkle: A couple of the simpNF linter issues are coming from simp lemmas generated by simps! on a constructor, and adding the nolint simpNF attribute doesn't seem to fix those.

[Matthew Ballard]

Yeah, it looks like the nolint attribute is failing on generated declarations and there is no global option to disable this linter. I am not sure what the preferred solution is here @Johan Commelin

[Johan Commelin]

I raised this issue here https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simps.20and.20simpNF.20linter
But there is no solution yet. I think this needs input from people who understand meta code.

[Matthew Ballard]

Perhaps one could short circuit the linter here using the standard pattern with set_option.

[Matthew Ballard]

It wouldn't fix the tracking of generated decls but it would give a global kill switch

[Matthew Ballard]

Ok. You can attach nolint simpNF to the generated declarations using attribute #std4 > nolinting generated decls

[Matthew Ballard]

I did this plus aligned some fields whose names changed. It should be ready now.

[Matej Penciak]

Oh great! The attribute method is good to know going forward