check_yaml

Stream: mathlib4

[Yaël Dillies]

In #18884, the check_yaml.sh script failed me, apparently because I used 4 levels of indentation for some declarations instead of exactly 3. Can this be fixed? I do want the extra level of indentation here

[Damiano Testa]

Of course it can be fixed! :wink:

[Yaël Dillies]

Thanks Damiano for volunteering :heart:

[Damiano Testa]

:speak_no_evil:

[Damiano Testa]

What exactly should be the checked format, then?

[Damiano Testa]

The script has these lines consecutively:

overview_decls = tiered_extract(overview)
assert all(len(n) == 3 for n, _ in overview_decls)
overview_decls = flatten_names(overview_decls)

undergrad_decls = tiered_extract(undergrad)
assert all(len(n) >= 3 for n, _ in undergrad_decls)
undergrad_decls = flatten_names(undergrad_decls)

and the middle check of the first block is the failing one.

[Damiano Testa]

Changing the check to match >= 3 as in the second would likely make CI pass your current test, but I am not completely sure of the implications that this has.

[Damiano Testa]

Looking at the two files that are checked by this action, it looks reasonable to me to allow the "at least 3 tiers" in both.

[Damiano Testa]

However, it may be good to hear an opinion of someone who did not just look at the two files for the first time in years...

[Damiano Testa]

Btw, I think that you may get this error, once you get past the limit of 3:

Entries in `docs/overview.yaml` refer to declarations that don't exist. Please correct the following:
  Combinatorics :: Ramsey theory :: Hindman's theorem: FS_partition_regular

[Damiano Testa]

I don't understand why the lean script does the right thing with the undergrad file, but gets confused by the overview file.

[Damiano Testa]

Oh, is it maybe docs#Hindman.FS_partition_regular ?

[Damiano Testa]

So, the modified script may have found a bug in the PR!

[Damiano Testa]

So, if you merge branch#test/combinatorics_overview into your PR, CI should pass.

[Yaël Dillies]

@Damiano Testa, it works! Could you open a PR?

[Damiano Testa]

#18910

[Patrick Massot]

The relevant question is: do we really want such nesting? This is meant to be a very high level overview. Maybe you’re putting too many details.

[Patrick Massot]

Since this doesn’t seem to trigger much discussion, let me be more explicit: I am rather skeptical that this is needed. Other areas of math don’t seem to need it.

[Andrew Yang]

An arguement for 4 is: If we were to follow MSC to organise the overview, then the declarations will naturally be living in the 4-th layer.

[Yaël Dillies]

Patrick Massot said:

The relevant question is: do we really want such nesting? This is meant to be a very high level overview. Maybe you’re putting too many details.

Other areas of math don't seem to need it.

From your request earlier, I gathered that there were not enough results mentioned in the overview. Hence I do not really think that other areas of maths having less results mentioned and not as many nestings is an indication that I have done something wrong.

[Patrick Massot]

You can mention more results without increasing depth.