port dashboard

Stream: mathlib4

[Johan Commelin]

The .decision_nec file on the porting dashboard is a weird artifact that seems related to archive/miu_language/decision_nec.lean. I don't understand how it ends up on the dashboard in this butchered form...

[Mauricio Collares]

I think the dashboard just doesn't like resolving these two relative imports.

[Johan Commelin]

very good catch! If nobody beats me to it, I'll try to PR fixes to ml3 on the train back home.

[Johan Commelin]

Aah, of course you can't actually have absolute imports there.

[Johan Commelin]

So we could hack the dashboard to just exlude these files. Or we ignore them.

[Eric Wieser]

Johan Commelin said:

The .decision_nec file on the porting dashboard is a weird artifact that seems related to archive/miu_language/decision_nec.lean. I don't understand how it ends up on the dashboard in this butchered form...

This ends up on the dashboard because #port-wiki contains lean_core..decision_nec