openai / lean-gym
File Size

The distribution of size of files (measured in lines of code).

Intro
Learn more...
File Size Overall
0% | 36% | 0% | 43% | 20%
Legend:
1001+
501-1000
201-500
101-200
1-100


explore: grouped by folders | grouped by size | sunburst | 3D view
File Size per Extension
1001+
501-1000
201-500
101-200
1-100
lean0% | 36% | 0% | 44% | 18%
toml0% | 0% | 0% | 0% | 100%
File Size per Logical Decomposition
primary
1001+
501-1000
201-500
101-200
1-100
src0% | 36% | 0% | 44% | 18%
ROOT0% | 0% | 0% | 0% | 100%
Longest Files (Top 13)
File# lines# units
lean
repl.lean
in src
 502 -
lean
table.lean
in src/basic
 198 -
lean
list.lean
in src/basic
 139 -
lean
control.lean
in src/basic
 132 -
lean
tactic.lean
in src/util
 130 -
lean
shrink_proof.lean
in src/tools
 86 -
lean
filter_decls.lean
in src/tools
 52 -
lean
io.lean
in src/util
 51 -
lean
util.lean
in src/util
 41 -
lean
try_finish.lean
in src/tools
 28 -
8 -
8 -
7 -
Files With Most Units (Top 0)
File# lines# units
Files With Long Lines (Top 6)

There are 6 files with lines longer than 120 characters. In total, there are 43 long lines.

File# lines# units# long lines
lean
table.lean
in src/basic
 198 - 23
lean
repl.lean
in src
 502 - 8
lean
shrink_proof.lean
in src/tools
 86 - 6
lean
tactic.lean
in src/util
 130 - 2
lean
list.lean
in src/basic
 139 - 2
lean
control.lean
in src/basic
 132 - 2
Correlations

File Size vs. Commits (all time): 13 points

src/repl.lean x: 70 commits (all time) y: 502 lines of code src/tools/try_finish.lean x: 5 commits (all time) y: 28 lines of code src/util/io.lean x: 19 commits (all time) y: 51 lines of code leanpkg.toml x: 20 commits (all time) y: 8 lines of code leanpkg_mathlib.toml x: 10 commits (all time) y: 7 lines of code leanpkg_miniF2F.toml x: 33 commits (all time) y: 8 lines of code src/tools/filter_decls.lean x: 6 commits (all time) y: 52 lines of code src/tools/shrink_proof.lean x: 6 commits (all time) y: 86 lines of code src/util/tactic.lean x: 32 commits (all time) y: 130 lines of code src/basic/control.lean x: 3 commits (all time) y: 132 lines of code src/util/util.lean x: 2 commits (all time) y: 41 lines of code src/basic/table.lean x: 3 commits (all time) y: 198 lines of code src/basic/list.lean x: 2 commits (all time) y: 139 lines of code
502.0
lines of code
  min: 7.0
  average: 106.31
  25th percentile: 18.0
  median: 52.0
  75th percentile: 135.5
  max: 502.0
0 70.0
commits (all time)
min: 2.0 | average: 16.23 | 25th percentile: 3.0 | median: 6.0 | 75th percentile: 26.0 | max: 70.0

File Size vs. Contributors (all time): 13 points

src/repl.lean x: 8 contributors (all time) y: 502 lines of code src/tools/try_finish.lean x: 2 contributors (all time) y: 28 lines of code src/util/io.lean x: 4 contributors (all time) y: 51 lines of code leanpkg.toml x: 3 contributors (all time) y: 8 lines of code leanpkg_mathlib.toml x: 2 contributors (all time) y: 7 lines of code leanpkg_miniF2F.toml x: 5 contributors (all time) y: 8 lines of code src/tools/filter_decls.lean x: 2 contributors (all time) y: 52 lines of code src/tools/shrink_proof.lean x: 2 contributors (all time) y: 86 lines of code src/util/tactic.lean x: 5 contributors (all time) y: 130 lines of code src/basic/control.lean x: 1 contributors (all time) y: 132 lines of code src/util/util.lean x: 1 contributors (all time) y: 41 lines of code src/basic/table.lean x: 2 contributors (all time) y: 198 lines of code src/basic/list.lean x: 1 contributors (all time) y: 139 lines of code
502.0
lines of code
  min: 7.0
  average: 106.31
  25th percentile: 18.0
  median: 52.0
  75th percentile: 135.5
  max: 502.0
0 8.0
contributors (all time)
min: 1.0 | average: 2.92 | 25th percentile: 1.5 | median: 2.0 | 75th percentile: 4.5 | max: 8.0

File Size vs. Commits (30 days): 0 points

No data for "commits (30d)" vs. "lines of code".

File Size vs. Contributors (30 days): 0 points

No data for "contributors (30d)" vs. "lines of code".

File Size vs. Commits (90 days): 0 points

No data for "commits (90d)" vs. "lines of code".

File Size vs. Contributors (90 days): 0 points

No data for "contributors (90d)" vs. "lines of code".