New PR, CI failing

Stream: new members

[Arnoud van der Leer]

Hi! I moved some code over from infinity-categories in the PR #35287. The guide mentioned announcing this on zulip. Is this the right channel for that?

Also, how do I get the label infinity-cosmos to be added to the PR?
Ah, apparently I had to write infinity-cosmos without backticks.

And the CI seems to be failing, because the file I added "cannot be imported"? I generated Mathlib.lean using lake exe mk_all, but it seems that this change is breaking the CI.

[Chris Henson]

The error is because you need some adjustments to use the new module system. You'll see most other files begin with

module

public import ...

@[expose] public section

[Chris Henson]

Also you'll want to run lake exe mk_all --module.

[Arnoud van der Leer]

Ah, thanks

[Arnoud van der Leer]

Once I fixed that, I was getting a lot of errors of the form

Note: A public declaration `Category` exists but is imported privately; consider adding `public import Mathlib.CategoryTheory.Category.Basic`.
Error: error: Mathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean:61:23: Unknown identifier `Category`

I have tried to fix that by adding about 8 public import statements. Was that indeed the correct fix?

[Kevin Buzzard]

Just copy what is done in other files in mathlib and you should be ok