porting questions

Stream: mathlib4

[Kevin Buzzard]

Should there be a porting FAQ?

Two questions I have so far:

I don't know the algorithm for imports. It's been claimed that data.sigma.basic is ready for porting but none of the imports

--import Mathlib.Meta.Univs
--import Mathlib.Tactic.Lint.Default
--import Mathlib.Tactic.Ext

seem to work for me. In the file itself we have attributes such as @[nolint simp_nf] and @[ext] which are giving me errors in mathlib4. Right now I am unclear about whether I should be just commenting this stuff out, commenting it out with some specificically crafted TODO so that people will be able to find their way back to them later, giving up on porting this file and waiting for the attributes to work, asking how to make them work, etc etc (can we make them work yet?)

Second question: A theorem which was proved with by simp in mathlib3 isn't being proved by simp in mathlib4. Everything is very basic here and I can just prove the theorem by hand anyway -- but should I worry about this and/or investigate, or just find a proof which compiles and move on?

[Patrick Massot]

https://github.com/leanprover-community/mathlib4/wiki is meant to be the FAQ.

[Patrick Massot]

The answer to the second question is that the python script discards every import that starts with tactic or meta because the file layouts are not compatible in those regions.

[Kevin Buzzard]

Do you happen to know whether @[ext] or @[nolint] are up and running yet?

[David Renshaw]

there seem to be examples of both:
https://github.com/leanprover-community/mathlib4/blob/f4484bd81205d3066e378c7855c9a82ec3881b06/Mathlib/Order/Basic.lean#L348
https://github.com/leanprover-community/mathlib4/blob/f4484bd81205d3066e378c7855c9a82ec3881b06/Mathlib/Init/Logic.lean#L307

[Kevin Buzzard]

Aah this is a technique I need to learn: look at what is already there. Thanks! I am a programming amateur.

[Jannis Limperg]

(wrong thread)

[David Renshaw]

looks like the ext tactic has some todos: https://github.com/leanprover/std4/blob/a502f259aa9fc035a19794cd90ae0244541b4a89/Std/Tactic/Ext.lean#L98

[Kevin Buzzard]

Aah it's in std4, I wasn't even looking in the right repo!