openai / miniF2F - Source Code Overview

Analysis scope, overview of main, test, generated, deployment, build, and other code.

Source Code Analysis Scope

Files includes and excluded from analyses

thy

lean

txt

11 extensions are included in analyses: mm, thy, ml, lean, sh, txt, gitignore, md, py, json, toml
4 criteria are used to exclude files from analysis:

exclude files with path like ".*/sokrates_.*?[.]json" (Sokrates conventions and configurations) (1 file).
exclude files with path like ".*/[.][a-zA-Z0-9_]+.*" (Hidden files and folders) (1 file).
exclude files with path like ".*/git[-]history[.]txt" (Git history) (1 file).
exclude files with path like ".*/git[-][a-zA-Z0-9_]+[.]txt" (Git data exports for sokrates analyses) (0 files).

The source code folder contains 1,317 files:

1,310 files are included in analyses.
7 files are excluded from analyses:

Explore all files....

Overview of Analyzed Files

Basic stats on analyzed files

Intro

For analysis purposes we separate files in scope into several categories: main, test, generated, deployment and build, and other.

The main category contains all manually created source code files that are being used in the production.
Files in the main category are used as input for other analyses: logical decomposition, concerns, duplication, file size, unit size, and conditional complexity.
Test source code files are used only for testing of the product. These files are normally not deployed to production.
Build and deployment source code files are used to configure or support build and deployment process.
Generated source code files are automatically generated files that have not been manually changed after generation.
While a source code folder may contain a number of files, we are primarily interested in the source code files that are being written and maintained by developers.
Files containing binaries, documentation, or third-party libraries, for instance, are excluded from analysis. The exception are third-party libraries that have been changed by developers.

655 files

652 files

2 files

1 file

Main Code

All manually created or maintained source code that defines logic of the product that is run in a production environment.

thy

lean

Explore: circles | sunburst

The following criteria are used to filter files:

files with paths like ".*".

655 files match defined criteria (9,979 LOC, 100.0% vs. main code):

244 *.thy files (3,505 LOC)
244 *.mm files (3,262 LOC)
2 *.lean files (2,219 LOC)
163 *.ml files (752 LOC)
1 *.py files (234 LOC)
1 *.toml files (7 LOC)

" *.thy" is biggest, containing 35.12% of LOC.
" *.toml" is smallest, containing 0.07% of LOC.

Test Code

Used only for testing of the product. Normally not deployed in a production environment.

thy

lean

Explore: circles | sunburst

The following criteria are used to filter files:

files with paths like ".*/test[.].*".
files with paths like ".*/[Tt]est/.*".

652 files match defined criteria (8,632 LOC, 86.5% vs. main code):

244 *.thy files (3,312 LOC)
244 *.mm files (2,447 LOC)
1 *.lean files (2,283 LOC)
163 *.ml files (590 LOC)

" *.thy" is biggest, containing 38.37% of LOC.
" *.ml" is smallest, containing 6.84% of LOC.

Build and Deployment Code

Source code used to configure or support build and deployment process.

Explore: circles | sunburst

The following criteria are used to filter files:

files with paths like ".*[.]sh".
files with paths like ".*[.]git[a-z]+".
files with paths like ".*/[.]gitignore".

2 files match defined criteria (17 LOC, 0.2% vs. main code). All matches are in *.sh files.

Other Code

Explore: circles | sunburst

The following criteria are used to filter files:

files with paths like ".*[.]json".
files with paths like ".*[.]md".
files with paths like ".*/README[.][a-z0-9]+".
files with paths like ".*/[.]gitignore".
files with paths like ".*[.]txt".

1 file matches defined criteria (93 LOC, 0.9% vs. main code). All matches are in *.md files.

Analyzers

Info about analyzers used for source code examinations.

*.thy files are analyzed with DefaultLanguageAnalyzer:

All basic standard analyses supported (source code overview, duplication, file size, concerns, findings, metrics, controls)

Basic code cleaning (empty lines removed for LOC calculations and duplication calculations)

No unit size analysis

No conditional complexity analysis

No dependency analysis

*.mm files are analyzed with CppAnalyzer:

All basic standard analyses supported (source code overview, duplication, file size, concerns, findings, metrics, controls)

Advanced code cleaning (empty lines and comments removed for LOC calculations, additional cleaning for duplication calculations)

Unit size analysis

Conditional complexity analysis

Advanced heuristic dependency analysis

*.lean files are analyzed with DefaultLanguageAnalyzer:

All basic standard analyses supported (source code overview, duplication, file size, concerns, findings, metrics, controls)

Basic code cleaning (empty lines removed for LOC calculations and duplication calculations)

No unit size analysis

No conditional complexity analysis

No dependency analysis

*.ml files are analyzed with DefaultLanguageAnalyzer:

All basic standard analyses supported (source code overview, duplication, file size, concerns, findings, metrics, controls)

Basic code cleaning (empty lines removed for LOC calculations and duplication calculations)

No unit size analysis

No conditional complexity analysis

No dependency analysis

*.py files are analyzed with PythonAnalyzer:

All basic standard analyses supported (source code overview, duplication, file size, concerns, findings, metrics, controls)

Advanced code cleaning (empty lines and comments removed for LOC calculations, additional cleaning for duplication calculations)

Unit size analysis

Conditional complexity analysis

Basic heuristic dependency analysis

*.toml files are analyzed with DefaultLanguageAnalyzer:

All basic standard analyses supported (source code overview, duplication, file size, concerns, findings, metrics, controls)

Basic code cleaning (empty lines removed for LOC calculations and duplication calculations)

No unit size analysis

No conditional complexity analysis

No dependency analysis

2025-04-14 12:05