Skip to content

This script can check and auto-generate `import` statements in a lean4 repository.

License

Notifications You must be signed in to change notification settings

Seasawher/import-all

Repository files navigation

import-all

This is not my original. see yatima

how to use this

Add this repository to your lakefile:

require «import-all» from git
  "https://github.com/Seasawher/import-all" @ "main"

Don't forget to run lake update import-all after editing the lakefile.

Now you can run lake exe import_all <input_dir> and lake exe import_check <input_dir>.

  • import_all auto generate import statements for lean files in <input_dir>

  • import_check is mainly for CI. This command checks to see if the lean files in <input_dir> have been imported correctly.

You may not need to use this repository

What are you going to use this script for? If you want to ensure that all files are built every time you run lake build, this repository is not necessary. Instead, add the following settings to your lakefile. (replace YourProject with your project directory name 😃)

@[default_target]
lean_lib «YourProject» where
  globs := #[.submodules `YourProject]

About

This script can check and auto-generate `import` statements in a lean4 repository.

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages