Def main
Modification history
2024-12-11 21:35
MathlibTest/MathlibTestExecutable.lean
feat: test that an executable with `import Mathlib` can be built and run (#19755)
Added mainView on Github →2024-10-25 00:50
scripts/test.lean
chore: use `Batteries` test driver directly in the lake file (#15897) …
Deleted mainView on Github →2024-08-09 00:58
scripts/lint-style.lean
refactor: polish `lint_style` and rename to lint-style (#14757) …
Modified mainView on Github →2024-06-24 11:40
Mathlib/Tactic/Linter/TextBased.lean
chore: move `lint_style` executable to the `scripts` directory (#14057) …
Modified mainView on Github →2024-06-23 07:52
Mathlib/Tactic/Linter/TextBased.lean
feat(lint-style): fix `update-style-exceptions.py`; produce human-readable output by default (#14012) …
Modified mainView on Github →2024-06-21 07:01
Mathlib/Tactic/Linter/TextBased.lean
feat: rewrite file length check in Lean (#13620) …
Added mainView on Github →2024-05-29 17:17
scripts/mk_all.lean
feat: `lake exe mk_all` as a Lean executable (#11853) …
Added mainView on Github →2024-05-20 07:13
scripts/test.lean
chore: switch from `make test` to `lake test` (#12943) …
Added mainView on Github →2024-04-28 22:28
LongestPole/Main.lean
feat: 'lake exe pole' computes the longest pole (#8361) …
Added mainView on Github →2024-02-02 17:38
Shake/Main.lean
feat: add `lake exe shake` to CI (#9751) …
Modified mainView on Github →2024-01-15 00:29
Shake/Main.lean
feat: add `lake exe shake` tree shaking tool (#9346) …
Added mainView on Github →2024-01-10 11:53
ImportGraph/Main.lean
refactor: split `ImportGraph` into its own package. (#9169) …
Deleted mainView on Github →2023-07-12 04:07
Util/ImportGraph/Main.lean
chore: revert move utilities into Util directory (#5787) (#5825) …
Deleted mainView on Github →2023-07-11 10:52
Util/ImportGraph/Main.lean
chore: move utilities into Util directory (#5787) …
Added mainView on Github →