Is @[protect_proj] obsolete?

Stream: mathlib4

[Lars Ericson]

Algebra.Order.CompleteField on line 62 has this notation

@[protect_proj]
which Lean Infoview marks as an unknown attribute. Is it obsolete? I see the following occurrences in ported mathlib4, most all commented out:

Order/Heyting/Hom.lean:-- @[protect_proj] -- Porting note: Not yet implemented
Order/Heyting/Hom.lean:-- @[protect_proj] -- Porting note: Not yet implemented
Order/Heyting/Hom.lean:-- @[protect_proj] -- Porting note: Not yet implemented
Analysis/BoxIntegral/Partition/Filter.lean:-- @[protect_proj] -- Porting note: Not yet implemented
Algebra/Lie/Basic.lean:/- @[protect_proj] -- Porting note: not (yet) implemented. -/
Algebra/Lie/Basic.lean:/- @[protect_proj] -- Porting note: not (yet) implemented. -/
Algebra/Lie/Basic.lean:/- @[protect_proj] -- Porting note: not (yet) implemented. -/
Algebra/Lie/Basic.lean:/- @[protect_proj] -- Porting note: not (yet) implemented. -/
Algebra/Order/CompleteField.lean:@[protect_proj]
Algebra/Order/Kleene.lean:-- @[protect_proj] -- Porting note: Not yet implemented
Algebra/Order/Kleene.lean:-- @[protect_proj] -- Porting note: Not yet implemented
Algebra/Order/Kleene.lean:-- @[protect_proj] -- Porting note: Not yet implemented
Algebra/Order/Kleene.lean:-- @[protect_proj] -- Porting note: Not yet implemented
Algebra/GCDMonoid/Basic.lean:-- Porting note: mathlib3 had a `@[protect_proj]` here, but adding `protected` to all the fields
Algebra/GCDMonoid/Basic.lean:-- Porting note: mathlib3 had a `@[protect_proj]` here, but adding `protected` to all the fields
Mathport/Syntax.lean:/- S -/ syntax (name := protectProj) "protect_proj" (&" without" (ppSpace ident)+)? : attr
Topology/ContinuousFunction/Basic.lean:--@[protect_proj] -- Porting note: missing attribute?

[Kyle Miller]

https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki

[Kyle Miller]

You now put protected before each field in a structure that used to have @[protect_proj]. You probably should also put a porting note.

[Lars Ericson]

@Kyle Miller lines 62 through 65 have a lot of issues. The original is:

@[protect_proj, ancestor linear_ordered_field conditionally_complete_linear_order]
class conditionally_complete_linear_ordered_field (α : Type*)
  extends linear_ordered_field α renaming max → sup min → inf, conditionally_complete_linear_order α

This gets automatically translated to

@[protect_proj]
class ConditionallyCompleteLinearOrderedField (α : Type _) extends
  "./././Mathport/Syntax/Translate/Command.lean:422:11: unsupported: advanced extends in structure",
  ConditionallyCompleteLinearOrder α

so in addition to the project_proj it is dropping the ancestor and what follows and doesn't like something in the extends perhaps the renaming. The porting wiki doesn't mention these 3 keywords.

[Kyle Miller]

I believe ancestor is obsolete due to changes in how structures work (you can see that uses of ancestor in mathlib3 are no longer present in ported mathlib4). I'm not sure about renaming at the moment

[Kyle Miller]

Looking at CompleteLinearOrder and how it was ported, it looks like what they did was find an equivalent set of things to extend and then manually create a new instance that projects to the missing parent structure. Porting this file seems like it will take some thought.

[Kyle Miller]

Another case study is ConditionallyCompleteLinearOrder

[Kyle Miller]

It looks like these two and ConditionallyCompleteLinearOrderedField are the only three structures in all of mathlib that involve porting extends ... renaming syntax

[Scott Morrison]

!4#4425 removes some porting notes about protect_proj in favour of just adding protected to all fields.

[Lars Ericson]

@Scott Morrisonto replace @[project_proj] is it just a matter of adding protected here:

protected class conditionally_complete_linear_ordered_field (α : Type*)

[Lars Ericson]

In any event I will give up on this file because it has too many expert level porting issues per @Kyle Miller .