lakefile.toml

name = "HepLean"
defaultTargets = ["HepLean"]
# -- Optional inclusion for LeanCopilot
#moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.14.0"

[[require]]
name = "«doc-gen4»"
git = "https://github.com/leanprover/doc-gen4"
rev = "v4.14.0"

[[lean_lib]]
name = "HepLean"

# -- Optional inclusion of llm. Needed for `openAI_doc_check`
#[[require]]
#name = "llm"
#git = "https://github.com/leanprover-community/llm"
#rev = "main"

# -- Optional inclusion of tryAtEachStep
#[[require]]
#name = "tryAtEachStep"
#git = "https://github.com/dwrensha/tryAtEachStep"
#rev = "main"

# -- Optional inclusion of LeanCopilot
#[[require]]
#name = "LeanCopilot"
#git = "https://github.com/lean-dojo/LeanCopilot.git"
#rev = "v1.4.1"

# lean_exe commands defined specifically for HepLean.

[[lean_exe]]
name = "check_file_imports"
srcDir = "scripts"

[[lean_exe]]
name = "type_former_lint"
srcDir = "scripts"

[[lean_exe]]
name = "hepLean_style_lint"
srcDir = "scripts"

[[lean_exe]]
name = "find_TODOs"
srcDir = "scripts"

[[lean_exe]]
name = "mathlib_textLint_on_hepLean"
srcDir = "scripts"

[[lean_exe]]
name = "stats"
supportInterpreter = true
srcDir = "scripts"

[[lean_exe]]
name = "notes"
supportInterpreter = true
srcDir = "scripts/MetaPrograms"

[[lean_exe]]
name = "lint_all"
supportInterpreter = true
srcDir = "scripts"

[[lean_exe]]
name = "free_simps"
srcDir = "scripts/MetaPrograms"

[[lean_exe]]
name = "check_rfl"
srcDir = "scripts/MetaPrograms"

[[lean_exe]]
name = "no_docs"
srcDir = "scripts/MetaPrograms"

[[lean_exe]]
name = "informal"
supportInterpreter = true
srcDir = "scripts/MetaPrograms"

[[lean_exe]]
name = "redundent_imports"
supportInterpreter = true
srcDir = "scripts/MetaPrograms"


# -- Optional inclusion of openAI_doc_check. Needs `llm` above.
#[[lean_exe]]
#name = "openAI_doc_check"
#srcDir = "scripts"