porting dashboard

Stream: mathlib4

[Johan Commelin]

Does anybody understand why https://leanprover-community.github.io/mathlib-port-status/file/category_theory/bicategory/coherence_tactic is still listed as unported?

[Johan Commelin]

We have

-- Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean

! This file was ported from Lean 3 source module category_theory.bicategory.coherence_tactic
! leanprover-community/mathlib commit 3d7987cda72abc473c7cdbbb075170e9ac620042
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.

[Jireh Loreaux]

Is it because of the path change?

[Johan Commelin]

I thought the header was supposed to take care of that...

[Jireh Loreaux]

Oh probably, I was just guessing.

[Eric Wieser]

Does #port-wiki list it as ported?

[Eric Wieser]

Looks like it doesn't. So the unhelpful answer is "the dashboard says it's not ported because that's what the wiki says"

[Johan Commelin]

Ok, so then I invite people to answer the appropriate helpful question :wink:

[Eric Wieser]

I think your script ignores the Tactic directory

[Eric Wieser]

https://github.com/leanprover-community/mathlib4/blob/master/scripts/make_port_status.py#L78-L80

[Eric Wieser]

I think those lines are nonsense

[Eric Wieser]

We should check files for a sync header wherever they are

[Johan Commelin]

yes, I agree.

[Eric Wieser]

https://github.com/leanprover-community/mathlib4/pull/4799

[Eric Wieser]

As usual you'll need to test it on your own machine

[Johan Commelin]

I'm going to test this one in production.

[Johan Commelin]

#port-wiki now says

category_theory.bicategory.coherence_tactic: Yes mathlib4#4610 3d7987cda72abc473c7cdbbb075170e9ac620042

[Eric Wieser]

!4#4800 contains a follow-up to make the archive be included

[Johan Commelin]

Johan Commelin said:

Does anybody understand why https://leanprover-community.github.io/mathlib-port-status/file/category_theory/bicategory/coherence_tactic is still listed as unported?

Now this file is no longer listed. Thanks @Eric Wieser