In the talk from Jonathan Blow the treemap application has a dropdown for metrics and borders:
Metrics:
'if' density
maximum 'if' depth
Maximum loop depth
assignments
global reads
global writes
heap allocations
heap frees
call locality (module) (when calling code, is it within module or to other modules?)
call locality (file) (when calling code, it is within file or to other files?)
call constancy (Is the function we're calling known at compile time, or is it a function pointer?)
Blend (a linear blend of all the above)
Borders
Modules + files. He says every leaf square is a procedure or function, then the white borders are files, and the black borders are modules. The size is proportional to how big the procedure is, size metric is "expression count" which is the # of nodes in the AST of the program.
So here we have a number of questions for how to visualize mathlib.
Firstly, what metrics to use?
Proof length
number of tactic calls
Distribution of tactic uses
LOC
Comment ratio, comment density
Figuring out uses of unfold in a file that is not where that definition was created
Speed of tactic calls
Highly nested have-blocks
stuff in nolint.json?
Secondly, what borders?
White borders can still be files. I don't know what Lean has in terms of modules, or what leaf squares should be. Right away I see alias, theorem, lemma, section and end, variable, import, module, namespace, open, universe as being top level statements.
We would really prefer to get information from lean compiler, instead of relying on regex and textual search. This implies that the input should be a static file, instead of something dynamically updating
In the talk from Jonathan Blow the treemap application has a dropdown for metrics and borders:
Metrics:
'if' density
maximum 'if' depth
Maximum loop depth
assignments
global reads
global writes
heap allocations
heap frees
call locality (module) (when calling code, is it within module or to other modules?)
call locality (file) (when calling code, it is within file or to other files?)
call constancy (Is the function we're calling known at compile time, or is it a function pointer?)
Blend (a linear blend of all the above)
Borders
Modules + files. He says every leaf square is a procedure or function, then the white borders are files, and the black borders are modules. The size is proportional to how big the procedure is, size metric is "expression count" which is the # of nodes in the AST of the program.
So here we have a number of questions for how to visualize mathlib.
Firstly, what metrics to use?
Proof length
number of tactic calls
Distribution of tactic uses
LOC
Comment ratio, comment density
Figuring out uses of unfold in a file that is not where that definition was created
Speed of tactic calls
Highly nested have-blocks
stuff in nolint.json?
Secondly, what borders?
White borders can still be files. I don't know what Lean has in terms of modules, or what leaf squares should be. Right away I see
alias,theorem,lemma,sectionandend,variable,import,module,namespace,open,universeas being top level statements.We would really prefer to get information from lean compiler, instead of relying on regex and textual search. This implies that the input should be a static file, instead of something dynamically updating