Migrating alpha file import to lean + adding testing - #1552

Merged

jstoobysmith merged 11 commits into

leanprover-community:masterfrom

FergusMunro:migratingAlphaFileImportToLean

Aug 21, 2026

Commits on Aug 19, 2026

created alphaFileImports.lean
FergusMunro
committed
c138503
updated lakefile and agents.md to include alphaFileImports as build target
FergusMunro
committed
b9d4cc9
included alphaFileImports and noAlphaImports in lint_all.lean
FergusMunro
committed
fe22c84
changed alphaBuild workflow to use new lean script
FergusMunro
committed
a2388a6
modified lean checkers to allow for command line arguments
FergusMunro
committed
5fbd936
created Meta/test directory, populated with dummy project violating linter rules, and created testing lean script2
FergusMunro
committed
023eae0
added testImportScript to lakefile
FergusMunro
committed
a9645bf

Commits on Aug 20, 2026

added text for new checks in lint_all
FergusMunro
committed
cf27671
temporarily removed Meta file
FergusMunro
committed
ee1390e
Removed newlines and accidental test case.
FergusMunro
committed
2671e17
removed a few extra newlines
FergusMunro
committed
953494f