Periodic reports

Stream: general

[Damiano Testa]

It was suggested in this thread that there might be interest to have a periodic report on some generic global information about mathlib. I personally find this very interesting!

This would be a bot that periodically posts a message on Zulip with some mathlib statistics.

I think that there are two main decisions to take:

• what should be the frequency (possible ranges: never...daily -- more is probably too much?);
• what statistics would the community like to see!

I am going to start two polls, one for frequency and one for possible topics: please vote your favourite or suggest more!

PS I am happy to try to implement the automation and the statistics, but if you ask for something too wild, I may not be able to do it! :smile:

[Damiano Testa]

/poll Frequency
Daily
Weekly
Biweekly
Monthly

[Damiano Testa]

/poll Mathlib statistic (could be more than one)
Top five popular tactics since last post
Net change in number of lines of Mathlib
Number of new declarations
Number of invisible (autogenerated) declarations
Number of docstrings
Longest proof (expression)
Longest proof (syntax)
Most popular starting tactic
Most popular finishing tactic

[Matthew Ballard]

Zulip is good but a bit incestuous. I was only half joking with the LinkedIn suggestion. Where does one disseminate this information to broader public these days?

[Patrick Massot]

We already have a statistics webpage. But we could indeed post something on mastodon for instance.

[Damiano Testa]

Ok, I guess that maybe I should also start a poll on where this should be posted! Maybe I will wait to see what information surfaces above, though.

[Yaël Dillies]

I can't seem to add options to the pole? I meant to add Slowest proofs and Slowest files

[Damiano Testa]

I had forgotten about the statistics page that Patrick mentioned! The number of theorems and the number of lines are already mentioned there, and these were the two most prominent features that were requested. This was easy!

[Damiano Testa]

The next one up seems to be number of new modules with docstrings (I guess that this means a file that did not exist the previous week and that contains at least one doc-string?).

[Damiano Testa]

I can look into either incorporating this information on the webpage or prepare a bot that posts on Zulip.

[Damiano Testa]

Even if we decide to post somewhere else, probably testing it in-house is a good idea.

[Bolton Bailey]

In particular, I think that longest pole/longest file(s)/longest proof(s) would be a good candidate for addition to the stats page rather than a feed, since those ones are less of a "here are new updates you might want to be made aware of" and more of a "long-running performance metrics we would like to track and optimize"

[Yaël Dillies]

Yaël Dillies said:

I can't seem to add options to the pole? I meant to add Slowest proofs and Slowest files

Now I can! Please move your reacts from my message to the poll :smile:

[Yaël Dillies]

I believe we should differentiate between:

• sexy statistics to boast mathlib
• gory statistics for people like Matthew or I trying to get mathlib faster/more organised

[Bolton Bailey]

Another option that I think has been suggested for longest pole is to include it in the speed center report somehow

[Damiano Testa]

In terms of differentiating, my initial idea was to have a (weekly according to the poll) feed that would report on one or two statistics on Zulip. I like the idea of advertising elsewhere, and I think that we should do it. I also agree that I would likely post different statistics on the two places.

[Damiano Testa]

I hope that this is how people voted above -- those are statistics that a bot would post weekly in a dedicated stream on Zulip. Feel free to change your answer, if this is not what you had intended!

[Damiano Testa]

I think that a little bit of testing of this model before we make another poll for a "public" posting is probably advisable.

[Jon Eugster]

You could also add links from the statistics page above to the speed center and to wherever stats are posted, so that it's easier to randomly stumble across them

[Bolton Bailey]

Also, while I take the point that the longest pole is not exactly great at being outward-facing, there is something sexy about knowing that "The ring of integers of a number field generated by a 5th-root of unity cyclotomic extension of the rationals is a principal ideal ring" is the deepest theorem we have been able to prove in the library.

[Kim Morrison]

Except that people who like theorem X should be trying to make sure that X is not the longest pole. :-)

[Kim Morrison]

And where "deepest" here could instead mean "least effort has been put into streamlining the dependencies"!

[Eric Wieser]

Or it could mean "streamlining is at the expense of this theorem because the fewest people care about it". I think a fair bit of streamlining is subjective and optimizes the bits current contributors care about at the expense of bits they don't (which is good, but not necessarily stable)

[Yaël Dillies]

Eric Wieser said:

I think a fair bit of streamlining is subjective and optimizes the bits current contributors care about at the expense of bits they don't

I doubt that's actually true in practice. The library is currently so underoptimised that any streamlining is good. Maybe in a few months once I've reasonably straightened out the imports the situation will be different, but right now I can't see any streamlining being bad to some files.

[Kevin Buzzard]

The fact that the integers of $\mathbb{Q}(\zeta_5)$ are a PID is a nontrivial result, needing inputs from both algebra and analysis, so maybe it deserves to be the longest pole

[Riccardo Brasca]

Note that the proof is very close to the math proof (it is indeed quite short, and fast). To be honest I don't see anything wrong with it (for example we can avoid the Minkowski bound and make the proof more direct, but I don't see the point in doing it).

[Ruben Van de Velde]

I think the point is that we're seeing that this proof depends on a lot of prior work, and the question is whether this complexity is inherent or accidental - and it seems like it's inherent

[Ruben Van de Velde]

But it's worth asking the question

[Kim Morrison]

I was referring more to the 4/5th of the longest pole leading up to the result that you wouldn't immediately notice have anything to do with it

[Kim Morrison]

The proof itself can be inherently complex, and still have way too much stuff transitively imported into it.

[Ruben Van de Velde]

(Speaking of splitting, maybe someone should split this thread)

[Damiano Testa]

I have started looking into preparing a summary of the weekly increase. Below is a first draft: please, feel free to comment on what you like, dislike, would like to add!

[Damiano Testa]

---

Weekly stats (2024-05-09 2024-05-16)

615 files changed, 13859 insertions(+), 5864 deletions(-), 7995 total(insertions-deletions)

---

%	Folder
4.3%	Mathlib/Algebra/CharP/
4.3%	Mathlib/Algebra/Group/
11.8%	Mathlib/Algebra/
3.1%	Mathlib/Analysis/
11.1%	Mathlib/CategoryTheory/
5.3%	Mathlib/Data/
3.0%	Mathlib/MeasureTheory/Measure/
3.6%	Mathlib/NumberTheory/LSeries/
3.4%	Mathlib/NumberTheory/
8.7%	Mathlib/RingTheory/Ideal/
6.8%	Mathlib/RingTheory/
10.1%	Mathlib/Tactic/CC/
3.5%	Mathlib/Topology/
16.9%	Mathlib/

commits: old fa33d89fc6, current 71f93293db.

Take also a look at the Mathlib stats page.

[Rémy Degenne]

What does the number in the % column mean?

[Damiano Testa]

I'm not sure, but I think that it is the percentage of change, according to git? The "% graph" is the output of git diff --dirstat "${commit}"...HEAD.

[Damiano Testa]

I found out about this by scavenging the git invocations, looking for "insertions and deletions". Someone on the internet mentioned --dirstat and it looked cool! :smile:

[Damiano Testa]

From the git manual:
--dirstat[=<param1,param2,…​>]

Output the distribution of relative amount of changes for each sub-directory. The behavior of --dirstat can be customized...

[Damiano Testa]

I guess that it is saying that 1617% of mathlib changed in the last week? :shrug:

[Rémy Degenne]

So most likely those 17% reflect some large refactors of low level stuff, or changes of the names of lemmas used everywhere, rather than new things added to mathlib?
I am trying to see if that stat is actually meaningful.

[Luigi Massacci]

Damiano Testa said:

Take also a look at the Mathlib stats page.

Is the recent part of the mathlib3 graph still relevant? Presumably the points after July 16, 2023 could be dropped?

[Damiano Testa]

Yeah, I am also trying to figure out what it means. Mathlib has 1,477,829 lines...

[Damiano Testa]

...and 13,859 is not really close to 17%.

[Damiano Testa]

Luigi Massacci said:

Damiano Testa said:

Take also a look at the Mathlib stats page.

Is the recent part of the mathlib3 graph still relevant? Presumably the stuff after July 16, 2023 could be dropped?

Yes, as the graph shows, mathlib3 became essentially obsolete as soon as the port was finished. I do not maintain that web-page though.

[Damiano Testa]

Back to the percentages: since it is a default option that git gives, I imagine that it has its reason of being, however I do not really know what it is. Unless someone is in favour of keeping it, I may as well drop it.

[Damiano Testa]

(Note that I am also planning to add the number of declarations to the first actual implementation, I just began with what did not require interacting simultaneously with the shell and lean in CI as a first attempt.)

[Damiano Testa]

The sum of all the percentages is 95.9, which may mean that this is explaining how the 13859 addition are spread across folders, where Mathlib presumably means "everything that was not accounted before".

[Yaël Dillies]

Damiano Testa said:

...and 13,859 is not really close to 17%.

Is it not 17% of the files?

[Yaël Dillies]

Damiano Testa said:

commits: old fa33d89fc6, current 71f93293db.

Can you make the commit hashes be links to the commits on github?

[Damiano Testa]

Yaël Dillies said:

Damiano Testa said:

...and 13,859 is not really close to 17%.

Is it not 17% of the files?

This could be.

Yaël Dillies said:

Damiano Testa said:

commits: old fa33d89fc6, current 71f93293db.

Can you make the commit hashes be links to the commits on github?

This should be easy, yes!

[Edward van de Meent]

i'm curious if a "top n merged PRs by diff size" might be informative?

[Edward van de Meent]

i imagine this might highlight important changes/additions

[Ruben Van de Velde]

Depending on how you count, they might all be Yaël moving things

[Damiano Testa]

Here is another proposal: what do you think of this report?

[Damiano Testa]

---

Weekly stats (2024-05-11 2024-05-18)

Reference commits: old 3d4137543f, new 712ef83de5.

987 files changed, 19810 insertions(+), 11144 deletions(-), 8666 total(insertions-deletions)

Declarations:

Type	New	Old	Change
Definitions	73624	73161	463
Theorems	231138	230101	1037
Inductives	2451	2430	21
Other	6148	6080	68

Take also a look at the Mathlib stats page.

[Johan Commelin]

For an internal report, I think that's nice. For an external report, I guess many people will be confused about why "Inductives" is an entry.

[Damiano Testa]

Yes, I was aiming to produce a report for Zulip, test it a little and then upgrade it to an "external" report.

[Eric Wieser]

I'm not sure counting inductives is interesting; def MulOpposite X := X is not really any different to structure MulOpposite where val : X

[Eric Wieser]

I think the interesting counts are maybe:

• Things in Sort _ (types / predicates)
• Things in P where P : Prop (theorems)
• Everything else (data)

[Damiano Testa]

@Eric Wieser, is this the distinction that you had in mind? The ConstantInfo:

• does not have a value;
• has a value whose type is Prop;
• has a value whose type is Type _.

[Eric Wieser]

I don't think the "has a value" is interesting, even things without a value (opaque, axiom) still have a type?

[Damiano Testa]

defnInfo and thmInfo have a value, all other ConstantInfos do not.

[Damiano Testa]

(Though they still have a type.)

[Damiano Testa]

To be precise, I was thinking of docs#Lean.ConstantInfo.value?

[Eric Wieser]

I think just look at type?

[Matthew Ballard]

New contributors, total?

[Damiano Testa]

So,

• inferType type = Prop => Theorem
• inferType type = Type _ => types/predicates
• everything else => data?

[Eric Wieser]

To detect types/ predicates you need to first introduce all the binders

[Eric Wieser]

Your first bullet is correct

[Damiano Testa]

Oh, let me try once more!

• inferType type = Prop => Theorem
• inferType (whatever MetaTelescope type gives) = Sort _ => types/predicates
• everything else => data?

[Eric Wieser]

I think bullet two should not have an infertype

[Damiano Testa]

updated the above. I'll try to implement it!

[Eric Wieser]

Should be = Sort _ too, but otherwise looks good!

[Damiano Testa]

Ok, updated the above!

[Damiano Testa]

Here is the current iteration, with the tally as suggested by Eric:

[Damiano Testa]

---

Weekly stats (2024-05-11 2024-05-18)

Reference commits: old 82af17d1e5, new 964b14278e.

843 files changed, 19601 insertions(+), 11029 deletions(-), 8572 total(insertions-deletions)

Declarations:

Type	New	Old	Change
Theorems	246865	245737	1128
Types/predicates	7649	7589	60
Other	58879	58486	393

Take also a look at the Mathlib stats page.

[Yaël Dillies]

So what does "Other" actually contain?

[Damiano Testa]

Do you want to see some example? If I did not mess up, I implemented the suggestion that Eric proposed.

[Damiano Testa]

It seems mostly garbage.
This is a random sample from the middle of other in Mathlib.Data.Nat.Defs or below:

Set.«term{_|_}_1»
Lean.Expr.isExplicitNumber
Preorder.toLT
Mathlib.getMathlibDir
Simps.zsmulArgs
ToAdditive.proceedFields
Simps.elabSimpsRule
Lean.Parser.Command.simpsRule
Mathlib.Util.«commandCompile_def%_»
instTransGeGt_mathlib
Function.«term↿_»
Simps.ParsedProjectionData.isPrefix
ToAdditive.addToAdditiveAttr
Function.extend
Nat.leRecOn
Lean.Meta.simpType
to_additive_relevant_arg
Mathlib.Prelude.Rename.align.precheck
Classical.decRel
ToAdditive.relevantArgAttr
Lean.MVarId.gcongr
Mathlib.Tactic.PushNeg.elabPushNegConv
Parser.Attr.qify_simps_proc
Trans.simple
Mathlib.Notation.unexpandExistsUnique
Nat.decidableLoHiLe
Lean.Parser.Attr.attrSimps?_
Mathlib.Tactic.tacticTransitivity___
Set.instSDiff
Classical.decPred
Mathlib.Tactic.tacticAssumption'
One.toOfNat1
ToAdditive.warnParametricAttr
Simps.instInhabitedAutomaticProjectionData
Simps.findAutomaticProjections
Mathlib.Tactic.variables
Simps.ProjectionRule.rename
Nat.strongRec'
Mathlib.Prelude.Rename.RenameMap.insert
Mathlib.ProjectionNotation.mkExtendedFieldNotationUnexpander
ToAdditive.applyReplacementFun.aux

[Yaël Dillies]

They are all definitions, right?

[Damiano Testa]

It seems like it. I wonder whether my code is not discriminating correctly.

[Damiano Testa]

This is what I am using, with hopefully clear names:

  if (← isProp type) then
    return {s with thms := s.thms + 1}
  else
    if ← forallTelescopeReducing type fun _ e => return e.isSort then
      return {s with typesPreds := s.typesPreds + 1}
    else
      return {s with other := s.other + 1}

[Damiano Testa]

I wonder whether the other field

• should be dropped, as it is junk;
• has interesting first difference, in that there is a lot of junk at the beginning, but (almost) everything that gets added week by week is interesting.

[Eric Wieser]

Yes, I think "other" is "data"

[Eric Wieser]

And "predicate" should probably have been "propositions"

[Damiano Testa]

So, should I simply label it by data and be happy with it?

[Eric Wieser]

Or "definitions"

[Damiano Testa]

propositions has a possibly ambiguous meaning for mathematicians, as in "lemma, theorem, proposition".

[Yaël Dillies]

Data is junk! You've heard it here first :stuck_out_tongue_closed_eyes:

[Damiano Testa]

So, it may be good for this Zulip to say proposition, but for the external tally, I would not use propositions where theorems is also used.

[Eric Wieser]

You could also split propositions (Sort 0) and types (everything else), though maybe those counts are too small

[Damiano Testa]

Ok, I'll produce the finer splitting.

[Eric Wieser]

Some possible reasons that the stats page disagrees about theorems:

• It might be omitting internal theorems, like equation lemmas
• It might be counting all instances as definitions

[Damiano Testa]

The commits are possibly also different.

[Eric Wieser]

Not 100k theorems different I would hope

[Damiano Testa]

I also filter out non-mathlib files and I screen for

  if c.isUnsafe || (← n.isBlackListed) then return s else

[Eric Wieser]

I think including core and std is probably interesting; most mathlib users don't care whether a lemma is in mathlib/batteries/core, just that it's available with import Mathlib

[Damiano Testa]

I think that a reasonable count should contain results that have either an actual syntax or "should" (such as to_additive generated stuff).

[Eric Wieser]

Yes, to_additive and simps lemmas are worth counting

[Damiano Testa]

Ok, should I then include all declarations, not just the ones in mathlib? (The difference will hardly notice the difference, I imagine).

[Damiano Testa]

The refined count with Mathlib only:

Theorems 157759
Types 1492
Predicates 3731
Other 37490

and with all declarations in the environment:

Theorems 167953
Types 3325
Predicates 4148
Other 60099

[Damiano Testa]

Oh, I forgot to rename Other to Data!

[Damiano Testa]

... and finally, screening out only unsafe, but keeping all blacklisted declarations, in std, core or mathlib:

Theorems 262537
Types 3431
Predicates 8053
Data 106992

[Damiano Testa]

Here is what it seems that the discussion is converging to:

[Damiano Testa]

---

Weekly stats (2024-05-11 2024-05-18)

Reference commits: old 311c57e763, new 53364710b4.

844 files changed, 19661 insertions(+), 11032 deletions(-), 8629 total(insertions-deletions)

Declarations:

Type	New	Old	Change
Theorems	168051	167286	765
Types	3325	3317	8
Predicates	4150	4117	33
Data	60106	59820	286

Take also a look at the Mathlib stats page.

[Damiano Testa]

Any further comments/additions? Would having a total for each column of the table be better? Worse?

[Patrick Massot]

All those numbers are rather difficult to read because there is no separation between groups of three digits.

[Damiano Testa]

Patrick Massot said:

All those numbers are rather difficult to read because there is no separation between groups of three digits.

Ah, let me take care of that!

[Yaël Dillies]

Also I think you should emphasize that theorems are to predicates what data is to types. What about ordering the rows as "Theorems, Data, Predicates, Types"?

[Yaël Dillies]

Damiano Testa said:

Would having a total for each column of the table be better?

I think it does not really matter since the different quantities are not really commensurable

[Richard Osborn]

Perhaps it would be better to have Type | New | Change | Percentage. It's not particularly meaningful to compare a number like 168051 to 167286.

[Damiano Testa]

With thousands separator and Yaël reordered:

[Damiano Testa]

---

Weekly stats (2024-05-11 2024-05-18)

Reference commits: old 311c57e763, new 53364710b4.

844 files changed, 19661 insertions(+), 11032 deletions(-), 8629 total(insertions-deletions)

Declarations:

Type	New	Old	Change
Theorems	168,051	167,286	765
Data	60,106	59,820	286
Predicates	4,150	4,117	33
Types	3,325	3,317	8

Take also a look at the Mathlib stats page.

[Yaël Dillies]

That's very pretty as the bigger numbers are now on the top

[Damiano Testa]

Ok, the latest request is to have a percentage instead of/in addition to the Change column: any strong opinions?

[Eric Wieser]

Regarding the first line, I think you should link to https://github.com/leanprover-community/mathlib4/compare/311c57e763368176a19af895c8a4a6ec1bcab3cc...53364710b45b6e223ccb0a720e59c422a05dff1a

[Damiano Testa]

(If not, I will simply add another column with the percentage.)

[Yaël Dillies]

I think Richard wanted to remove the Old column instead. Personally, I think you should just add a new column

[Damiano Testa]

Oh, I misunderstood. I'll definitely add a percentage column. As to removing the Old one... don't particularly care, but maybe would keep it and try this format for a bit?

[Richard Osborn]

I don't mind keeping the old column either.

[Eric Wieser]

It would be cool to represent the change column as +X -Y; even if the matching is just by name

[Patrick Massot]

I also think the Old column is not very useful.

[Richard Osborn]

Does this track when declarations move files? Or are those considered new declarations?

[Damiano Testa]

Eric Wieser said:

It would be cool to represent the change column as +X -Y; even if the matching is just by name

For this, I would have to restructure the code a bit, since currently I am just tallying the numbers, not recording the declaration names.

[Damiano Testa]

Richard Osborn said:

Does this track when declarations move files? Or are those considered new declarations?

No, this is just tracking numbers of declarations, it is not doing anything with file names, nor even with declaration names. I loop over the declarations, classify them and maintain a tally of the types.

[Richard Osborn]

This could still be useful to track the "largest" PRs that aren't primarily organizational in nature (which touch many lines of code, but do not change the total number of declarations).

[Damiano Testa]

There is already some automation for that with the move-decls label.

[Damiano Testa]

Once the comments settle, I can look into storing HashSets of names of declarations, so that the +X -Y column could exist.

[Damiano Testa]

In the meantime:

[Damiano Testa]

---

Weekly stats (2024-05-11 2024-05-18)

Reference commits: old 4dffa6dc6e, new f9e2c51760.

842 files changed, 19359 insertions(+), 11033 deletions(-), 8326 total(insertions-deletions)

Declarations:

Type	New	Change	%
Theorems	168,051	730	0.43%
Data	60,106	283	0.47%
Predicates	4,150	32	0.77%
Types	3,325	8	0.24%

Take also a look at the Mathlib stats page.

[Mario Carneiro]

I think you could collapse the new and change columns to just "168 051 (+730)"

[Ruben Van de Velde]

And then also the % column?

[Damiano Testa]

I got this to work

[Damiano Testa]

---

Weekly stats (2024-05-11...2024-05-18)

Reference commits: old 0e70892cf2, new 57e4f13b3a.

882 files changed, 19159 insertions(+), 11425 deletions(-), 7734 total(insertions-deletions)

Declarations:

Type	New	+-	Change	%
Theorems	168,040	+745 -80	167,375	0.40%
Data	60,303	+307 -20	60,016	0.48%
Predicates	4,150	+31 -2	4,121	0.70%
Types	6,652	+16 -0	6,636	0.24%

Take also a look at the Mathlib stats page.

[Michael Stoll]

Change = Old?

[Damiano Testa]

Yes, sorry, I had added Change back for testing, this is closer taking into account some of the previous comments:

[Damiano Testa]

---

Weekly stats (2024-05-11...2024-05-18)

Reference commits: old 0e70892cf2, new 57e4f13b3a.

882 files changed, 19159 insertions(+), 11425 deletions(-), 7734 total(insertions-deletions)

Declarations:

Type	New	+-	%
Theorems	168,040	+745 -80	0.40%
Data	60,303	+307 -20	0.48%
Predicates	4,150	+31 -2	0.70%
Types	6,652	+16 -0	0.24%

Take also a look at the Mathlib stats page.

[Damiano Testa]

As suggested by Mario and Ruben, there could just be two or three columns. I do not have a preference.

[Damiano Testa]

Btw, the cache for 0e70892cf2 is corrupted.

[Patrick Massot]

The name new without old is hard to understand

[Patrick Massot]

Maybe total is better

[Eric Wieser]

Eric Wieser said:

Regarding the first line, I think you should link to https://github.com/leanprover-community/mathlib4/compare/311c57e763368176a19af895c8a4a6ec1bcab3cc...53364710b45b6e223ccb0a720e59c422a05dff1a

Damiano, it looks like you might have missed this comment

[Damiano Testa]

Patrick: I renamed Change to Total-- I agree that it is much better!
Mario: I merged Total and +-.
Eric: I totally missed your suggestion to link to compare!

[Damiano Testa]

---

Weekly stats (2024-05-12...2024-05-19)

Type	Total	%
Theorems	168,072 (+772 -86)	0.41%
Data	60,129 (+320 -19)	0.50%
Predicates	4,150 (+31 -2)	0.70%
Types	3,325 (+8 -0)	0.24%

892 files changed, 20516 insertions(+), 12696 deletions(-), 7820 total(insertions-deletions)

Reference commits: old 11471621f4, new 3015868dac.

Take also a look at the Mathlib stats page.

[Enrico Borba]

Excuse me for messaging here but what is a "Longest pole"? I've seen it mentioned a handful of times.

[Bolton Bailey]

Enrico Borba said:

Excuse me for messaging here but what is a "Longest pole"? I've seen it mentioned a handful of times.

See this topic. The longest pole is the sequence of files, each of which imports the previous, which has the longest total compile time, and which is therefore the bottleneck for project build time in the limit as the building computer becomes more parallel.

[Utensil Song]

Maybe

- 892 files changed, 20516 insertions(+), 12696 deletions(-), 7820 total(insertions-deletions)
+ 892 files changed, 7820 lines changed (+20516 -12696)

is less verbose and still clear?

[Yaël Dillies]

+ 892 files changed (+892 -0), 7820 lines changed (+20516 -12696) even?

[Damiano Testa]

Yaël, what does your (+892 -0) represent?

[Yaël Dillies]

The number of added files and the number of removed files

[Damiano Testa]

Oh, I see, so a piece of information that was not actually present in the output that I wrote, right?

[Mario Carneiro]

I think the usual git algorithm for the +- numbers would make the + number be added+changed and - is removed+changed

[Damiano Testa]

Ok, I can work with that!

[Damiano Testa]

Although, does git diff <some annotation> give me that directly?

[Damiano Testa]

(git diff --name-status gives the information with filenames, but not the tally already)

[Mario Carneiro]

I found --compact-summary but --name-status indeed looks easier to parse

[Mario Carneiro]

renames are interesting:

R087    Mathlib/Algebra/BigOperators/List/Basic.lean    Mathlib/Algebra/BigOperators/Group/List.lean

I'm not sure what the 087 means

[Damiano Testa]

Ok, for simplicity, I am going to produce counts of A+M (added and modified) and D+M (deleted and modified) and will not worry about renames and copies.

[Damiano Testa]

So, ultimately, report A-D files changed (+(A+M) -(D+M)).

[Mario Carneiro]

maybe A+D+M files changed?

[Mario Carneiro]

it's a bit weird for that number to be negative because it doesn't sound like a net value

[Damiano Testa]

Actually, git already has its own heuristic for which numbers of files changed to give: maybe I'll just use that and report (+(A+M) -(D+M)) as +-?

[Damiano Testa]

(I have a feeling that + will be very often equal to what git considers to be the number of files changed, but - may be somewhat different.)

[Damiano Testa]

E.g. for the two commits that I was using as a test, I get these numbers:

92 files changed, 1711 insertions(+), 544 deletions(-)
(+92 -85)

I suspect that the coincidence of 92 is very stable, but we'll see!

[Mario Carneiro]

hm, it seems hard to see when a deletion happens though, it would be nice to see that... sorry for waffling but maybe (+A -D ~M) would be better

[Mario Carneiro]

where a rename counts as A+D

[Damiano Testa]

Sure, this is very easy to do.

[Damiano Testa]

In the previous example, I get these numbers:

(+7 -0 ~85)

which indeed is probably a more faithful description of what happened.

[Mario Carneiro]

Is it possible to collect up this information to get a graph over time, or is the mathlib stats page already doing this?

[Damiano Testa]

The mathlib stats page has graphs plotted against time, but the information that I am extracting now is not in that page.

[Mario Carneiro]

I guess one cheap thing you could do is make sure that the weekly reports are distinctive enough that they can be harvested later via some zulip API

[Damiano Testa]

How does this look like?

[Damiano Testa]

---

Weekly stats (2024-05-12...2024-05-19)

Type	Total	%
Theorems	168,073 (+772 -90)	0.41%
Data	60,131 (+320 -19)	0.50%
Predicates	4,150 (+31 -2)	0.70%
Types	3,325 (+8 -0)	0.24%

895 files changed (+42 -11 ~839), 7725 lines changed (+20466 -12741)

Reference commits: old 3f8be61e1c, new d874bdffd1.

Take also a look at the Mathlib stats page.

[Damiano Testa]

Now that we have the + - ~, I wish git had something similar for the lines as well...

[Mario Carneiro]

I suppose you could just interpret the 7725 as ~

[Mario Carneiro]

although it seems to be just 20466-12741

[Kevin Buzzard]

I think "Data" is confusing? Well, it's confusing me right now. What's the difference between "Data" and "Types"? Is Data = terms?

[Damiano Testa]

The 7725 was computed by me and it is indeed just the difference of the (absolute values of the) + and -.

[Mario Carneiro]

Maybe they should be categorized by definition kind: theorem, def, opaque, axiom

[Mario Carneiro]

and then separate between data, predicates, types for the relevant definition kind

[Damiano Testa]

I had the names of the constructors initially, but it was suggested that this other splitting was better... :smile:

[Kevin Buzzard]

I just don't know what people are going to think about the statement "mathlib has 168073 theorems and 60131 datas"

[Mario Carneiro]

I think someone said above this is not for external consumption

[Damiano Testa]

For the moment, I was thinking that this report would be just in Zulip.

[Mario Carneiro]

Other stats which would be useful:

• number of instances
• number of simp lemmas
• number of classes

[Damiano Testa]

It is certainly good to think about what to make public, but I was hoping to get a prototype up and running.

[Damiano Testa]

Yes, these are good suggestions. I focused on producing 1 git-based report and 1 lean-based report.

[Mario Carneiro]

Are there any other metrics people can think of which correlate with overall performance?

[Damiano Testa]

Once this works, I can definitely add more statistics.

[Mario Carneiro]

• number of linters
• number of environment extensions

[Damiano Testa]

Ok, I'll look into how to make a bot post on Zulip the statistics above once per week and I'll make a PR.

[Damiano Testa]

After that, we can see what else to add and what would be good "external" statistics.

[Damiano Testa]

Should the bot post on this thread/topic?

[Damiano Testa]

For testing, I may make it post a few times, just to get a feeling for how these things work.

[Mario Carneiro]

It should be in #mathlib4 stream, with a title like "Mathlib weekly change report"

[Yaël Dillies]

Kevin Buzzard said:

I think "Data" is confusing? Well, it's confusing me right now. What's the difference between "Data" and "Types"? Is Data = terms?

"Definitions", maybe?

[Eric Wieser]

"types" is things like Nat, "data" is things like Nat.factorial.

[Mario Carneiro]

another possible subdivision of the "data def" category is noncomputable/computable

[Mario Carneiro]

lemma/theorem would also be a great split, although I think we don't have the metadata needed to differentiate

[Mario Carneiro]

maybe documented/undocumented theorem

[Mario Carneiro]

actually % documented would be useful on every category

[Damiano Testa]

Mario Carneiro said:

lemma/theorem would also be a great split, although I think we don't have the metadata needed to differentiate

I was planning on doing that later. My plan was to run lake build on a prepped version of mathlib that would log things like this.

[Damiano Testa]

Mario Carneiro said:

actually % documented would be useful on every category

This was one of the suggestions above, I think.

[Eric Wieser]

The reason I suggested we avoid counting theorem is that the choice of what's a theorem and what's part of the definition (ie a projection) is arbitrary, and not interesting mathematically

[Mario Carneiro]

I don't think we should just restrict to mathematically interesting distinctions

[Damiano Testa]

(Note that in the doc-strings for the report, I am also putting in all the suggestions that came up.)

[Mario Carneiro]

I think the main things we want to get out of this relate to proof engineering/maintenance aspects, which is why my suggestions relate to either performance or other code quality indicators

[Damiano Testa]

#13038

[Damiano Testa]

Mario Carneiro said:

I think the main things we want to get out of this relate to proof engineering/maintenance aspects, which is why my suggestions relate to either performance or other code quality indicators

I really like your suggestions!

I am hoping that this current version will help setting up some infrastructure with some easy statistics, before we expand and actually use it for structural reports.

[Utensil Song]

Maybe "Data" is better renamed to "Definition"? It's easier to comprehend, and would it be inaccurate?

[Damiano Testa]

I wonder whether calling it Definition would suggest that it is a count of defs, rather than what it is actually counting.

[Mario Carneiro]

I think it should be a count of defs, subdivided accordingly

[Mario Carneiro]

theorems can't be Data anyway

[Damiano Testa]

Mario Carneiro said:

I think it should be a count of defs, subdivided accordingly

"subdivided accordingly" means that if the ConstantInfo is a defnInfo, then you want so split further into Def Type, Def Predicate and Def Data? What should be the labelling for defs that are in Prop? With the current scheme, everything in Prop is a Theorem.

[Damiano Testa]

(The initial split was precisely by classifying declarations based on their ConstantInfo constructor, so it seems that we are going back to that.)

[Damiano Testa]

What about

• thmInfo counts as Theorem
• defnInfo whose type is Prop counts as Definition (Prop)
• defnInfo whose type-after-binders is Type counts as Definition (Type)
• defnInfo whose type-after-binders is Sort counts as Definition (Predicate)
• defnInfo whose type-after-binders is something else counts as Definition (Data)

I suspect that this is close to what Mario was suggesting. This would ignore other types of ConstantInfo, but maybe this is ok?

[Yaël Dillies]

Damiano Testa said:

With the current scheme, everything in Prop is a Theorem.

That's wrong, right? Everything whose type has type Prop is a Theorem.

[Damiano Testa]

Yaël, yes, this is the usual isProp vs is*A*Prop slip! :man_facepalming:

[Damiano Testa]

(However, I think that the code is doing it right, since I access the type of a declaration, not the value.)

[Damiano Testa]

I am testing the split suggested above: there may be a post in the other stream soon with the new format... hopefully!

[Mario Carneiro]

I think you can throw all other constantinfo into "other"

[Mario Carneiro]

well, inductives should be a category

[Eric Wieser]

Mario, what's your argument for why we care about the type of Constant info? My argument for why we don't is that those are counting implementation details, and what we actually want to measure is API surface. The API surface of a one-field structure is the same as a type synonym, but the constantinfos are very different.

[Eric Wieser]

Mario Carneiro said:

theorems can't be Data anyway

Regarding the converse: are Prop instances still defs, or is that fixed in Lean 4.8.0?

[Mario Carneiro]

The API surface of a one-field structure is the same as a type synonym

I disagree about this, a one-field structure adds to/from functions and several generated declarations

[Mario Carneiro]

but also, in line with my point about gathering better data up-front, I think it's better to have the information than not, if we can easily collect it, and if the more coarse metrics are also there then you can ignore the fine-grained metrics

[Mario Carneiro]

It's difficult to guess in advance which metrics are going to be important until we start collecting the data

[Mario Carneiro]

Eric Wieser said:

Mario Carneiro said:

theorems can't be Data anyway

Regarding the converse: are Prop instances still defs, or is that fixed in Lean 4.8.0?

No, proofs can be def but data can't be theorem