problems with structure notation

Stream: general

[Johan Commelin]

@Sebastian Ullrich In https://github.com/leanprover-community/mathlib/pull/1259#issuecomment-514792526 there are some problems mentioned (by Johannes) with structure notation. I have had these problems as well.
Will those be fixed in Lean 4? Currently this is quite painful, even though structure notation produces more readable code than the anonymous version.
Quotes:

jcommelin:
I personally find the "named constructor"-version slightly more readable than the anonymous version.

johoelzl:
True, but there are two problems:

Lean was crashing when writing down the structure syntax (some assertions), and
the auto-parameters took ages to fail

I can use the structure syntax again.

semorrison:
I tend to:

1. Write out all the fields, filled in with sorry (including the auto_param fields).
2. Fill in the meaningful data fields.
3. Try removing the auto_param fields one by one, to see which ones the tactic can handle.
4. Write any remaining proofs.
It's certainly an unfortunate problem that while the data fields are incomplete or broken, Lean wastes a lot of time running auto_param tactics.

johoelzl:
A third problem I have with the structure notation:
Sometimes I write down {field1 := _, field2 := _ }, but instead of showing me the type of field1, I get a type error at field2. I don't remember if there was a solution to this, was this related to the meta-universe problem?

[Mario Carneiro]

The structure notation parser is one of the hackiest and messiest parts of the lean 3 parser, and it is responsible for a lot of bug reports. My guess is it's been completely rewritten, and with any luck it's more reasonable now in lean 4

[Scott Morrison]

Related to this, I (or someone) should put a test in tidy that fails quickly if it finds a sorry in the goal. I know that the tidy auto_params waste lots of CPU time on goals with embedded sorries.

[Scott Morrison]

(This is obviously only relevant while coding, not for library compile times.)