I need to leave it here for a bit; I'll label as help wanted because some dsimp is not tidying up as much as it should be and I'm not very good with debugging that kind of thing. I'm not going to touch this for at least 12 hours

Ok so the problems with porting this file are the following.

1. Lean continually PANICs meaning I continually need to restart Lean. Experiencing this on two different machines. Seems very hard to minimise. More precisely: if I edit a line of code there may be a panic, or, even worse, there just may be garbage in the infoview (complaining about stuff which isn't there) and red underlines underlining the wrong thing. In either case I have to restart Lean.

2. A non-terminal dsimp is broken and it's hard to fix. It's the proof of map₂_associator on line 301. In Lean 3 we have a lot of G.map etc; in Lean 4 it's the far uglier PrelaxFunctor.map G.toPrelaxFunctor and once you see the lean 3 goal (which has about 20 variants of this) you'll see the problem. It might be that some simp lemmas are missing because I had some problems with reassoc on lines 215, 226 etc.

Help!

Update: I fixed the non-terminal simp. The PANICs are still annoying and I can't reliably reproduce (they occur when editing, not compiling). The file is noisy because I don't understand attribute [reassoc]. If someone could confirm that the 9 instances of restate_axiom can be removed (and the corresponding 9 fields of structures renamed to not have primes at the end) I'd be much obliged: I was not aware of the relevant Lean 4 change. The file is now compiling but noisy.

OK this should be compiling now. One thing I wasn't sure about is removing various primes from the names of structure fields. My understanding (possibly incorrect) of Matt's comment above is that I can do this and then drop all the restate_axiom stuff. Example: the Lean 3 definition of Pseudofunctor has a lot of primes in structure fields here but I've removed them all (and also the corresponding restate_axiom stuff just afterwards). Is this right?

I'm about to update the module docstring and then hopefully this is ready to go.

OK this should be compiling now. One thing I wasn't sure about is removing various primes from the names of structure fields. My understanding (possibly incorrect) of Matt's comment above is that I can do this and then drop all the restate_axiom stuff. Example: the Lean 3 definition of Pseudofunctor has a lot of primes in structure fields here but I've removed them all (and also the corresponding restate_axiom stuff just afterwards). Is this right?

I'm about to update the module docstring and then hopefully this is ready to go.

I got it from here

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style