mathlib3port 404

Stream: mathlib4

[Kevin Buzzard]

Is the below problem caused by the fact that I'm eagerly trying to port a file without all its dependencies having been ported? I just wanted to experiment locally with porting the next file on the route to Ext.

buzzard@buster:~/lean-projects/mathlib4$ ./scripts/start_port.sh Mathlib/Algebra/Category/ModuleCat/Limits.lean
Checking out a new branch in a temporary working tree
Downloading latest version from mathlib3port
curl: (22) The requested URL returned error: 404
buzzard@buster:~/lean-projects/mathlib4$

[Mario Carneiro]

currently I see Algebra/Category/Module/Limits.lean in mathlib3port

[Mario Carneiro]

you might want to try using that name and then moving it where it is supposed to go

[Ruben Van de Velde]

Yeah, it's a name mismatch between the mathport output and mathlib 4 (the Cat :cat:)

[Mario Carneiro]

I'm not sure how people are handling file renames ATM

[Ruben Van de Velde]

Run the script with the mathport name, then in the first manual commit git mv the file and update Mathlib.lean

[Kevin Buzzard]

Thanks to both of you!