Removing unnecessary `@[expose]`

Stream: mathlib4

[Kim Morrison]

When we switched Mathlib to the module system, we added @[expose] public section at the top of every file.

These PRs remove the @[expose] from those files without defs or instances:

PR	Directory	Files	URL
1	Analysis/Calculus	87	https://github.com/leanprover-community/mathlib4/pull/33565
2	Analysis/SpecialFunctions	56	https://github.com/leanprover-community/mathlib4/pull/33567
3	Analysis/Normed	80	https://github.com/leanprover-community/mathlib4/pull/33568
4	Analysis/Complex	52	https://github.com/leanprover-community/mathlib4/pull/33569
5	Algebra/Order	95	https://github.com/leanprover-community/mathlib4/pull/33570
6	Algebra/Group	86	https://github.com/leanprover-community/mathlib4/pull/33571
7	Algebra/rest	62	https://github.com/leanprover-community/mathlib4/pull/33572
8	RingTheory	137	https://github.com/leanprover-community/mathlib4/pull/33573
9	Data	146	https://github.com/leanprover-community/mathlib4/pull/33574
10	Topology	110	https://github.com/leanprover-community/mathlib4/pull/33575
11	MeasureTheory	94	https://github.com/leanprover-community/mathlib4/pull/33576
12	CategoryTheory	59	https://github.com/leanprover-community/mathlib4/pull/33577
13	NumberTheory	69	https://github.com/leanprover-community/mathlib4/pull/33578
14	LinearAlgebra+Order	122	https://github.com/leanprover-community/mathlib4/pull/33579
15	Probability+Geometry	111	https://github.com/leanprover-community/mathlib4/pull/33580
16	Misc	47	https://github.com/leanprover-community/mathlib4/pull/33581

[Yury G. Kudryashov]

I think that we can also remove @[expose] from files with Prop-valued instances only, right?

[Yury G. Kudryashov]

BTW, did Claude prepare the whole PRs, or did it write a metaprogram that identifies these files?

[Yury G. Kudryashov]

Let me post numbers in separate messages, so that we can see the status here.

[Yury G. Kudryashov]

Analysis/Calculus #33565

[Yury G. Kudryashov]

Analysis/SpecialFunctions #33567

[Yury G. Kudryashov]

Analysis/Normed #33568

[Yury G. Kudryashov]

Analysis/Complex #33569

[Yury G. Kudryashov]

Algebra/Order #33570

[Yury G. Kudryashov]

Algebra/Group #33571

[Yury G. Kudryashov]

Algebra/rest #33572

[Yury G. Kudryashov]

RingTheory #33573

[Yury G. Kudryashov]

Data #33574

[Yury G. Kudryashov]

Topology #33575

[Yury G. Kudryashov]

MeasureTheory #33576

[Yury G. Kudryashov]

CategoryTheory #33577

[Yury G. Kudryashov]

NumberTheory #33578

[Yury G. Kudryashov]

LinearAlgebra+Order #33579

[Yury G. Kudryashov]

Probability+Geometry #33580

[Yury G. Kudryashov]

Misc #33581

[Yury G. Kudryashov]

At least some of these PRs fail CI

[Yury G. Kudryashov]

E.g., the measure theory one.

[Kim Morrison]

Yury G. Kudryashov said:

BTW, did Claude prepare the whole PRs, or did it write a metaprogram that identifies these files?

It wrote a script (just some grepping, no Lean metaprogramming)

[Kim Morrison]

The remaining PRs all pass CI.

[Yaël Dillies]

Yury G. Kudryashov said:

I think that we can also remove @[expose] from files with Prop-valued instances only, right?

I can't find the info in the reference manual anymore (looks like the module system section has been entirely reworked), but I thought instances always exposed their body?

[Johan Commelin]

I'm running

$ git diff --word-diff upstream/master... | rg "\[[-+]" | rg -v "^\[-@\[expose\]-\]public section$"

on these locally, to double check that Claude has not been naughty.