5Developer Tools

28 entries

Verso SlidesVerso genre for reveal.js slide decks with checked Lean code.leanprover/verso-slides
SubVersoExtracts highlighted Lean code for use in Verso and other tools.leanprover/subverso
mdgenGenerates Markdown files from Lean sources.Seasawher/mdgen
LiterateLeanFiles that are valid Markdown and valid Lean at the same time, with no preprocessor.tani/literate-lean
lean-slidesRenders reveal.js slides from Markdown comments inside the infoview.0art0/lean-slides
LeanTeXDSL for writing LaTeX Beamer presentations in Lean.kiranandcode/LeanTeX
versotreedocGenerates a Verso document skeleton that mirrors a source tree.richardlford/versotreedoc
doc-verification-bridgeDocumentation tool that extracts verification relationships from Lean code.NicolasRouquette/doc-verification-bridge
lean-i18nTranslate Lean projects with PO files.hhu-adam/lean-i18n

leanfmtStructure-preserving code formatter.duckki/leanfmt
lean-fmtCode formatter and linter with editor and CI integration.jcreinhold/lean-fmt
leanerLinter, formatter and whole-program dead-code eliminator.SrGaabriel/leaner
lint-llm-proofsLinters for patterns common in LLM-generated proofs.jessealama/lint-llm-proofs

import-graphAnalyze and visualize a package's import structure (lake exe graph).leanprover-community/import-graph
jixiaStatic analysis tool that extracts declarations, dependency graphs and tactic states.frenzymath/jixia
FlameTCFlame graphs for debugging type class synthesis performance.hargoniX/Flame
leaffDiff tool for Lean environments.alexjbest/leaff
lean4exportPlain-text export of declarations for external checkers and tools.leanprover/lean4export
ast_exportExports Lean 4 ASTs.digama0/ast_export
lean2sexpConverts .olean files to s-expressions.andrejbauer/lean2sexp
NodeGraphGenerates dependency graphs between declarations.adamtopaz/NodeGraph
lean4-dep-auditTraces a constant's transitive dependencies down to axioms, externs and their C sources.levzlotnik/lean4-dep-audit
Lean FuzzGrammar-based fuzzing for Lean DSLs, using parser tables extracted from the compiler.kiranandcode/lean-fuzz

lean4checkerReplays an environment to check that the kernel accepts every declaration (archived).leanprover/lean4checker
ComparatorChecks that a solution proves exactly the stated challenge theorem, using only allowed axioms.leanprover/comparator
Lean Kernel ArenaTest suite and leaderboard for independent Lean kernel implementations (source).
SafeVerifyRobustly checks submitted proofs and implementations against a reference.GasStationManager/SafeVerify
axiom-auditAxiom allowlist check that fails CI on sorry, native_decide or custom axioms.leanprover-community/axiom-audit