LeanTeX v2.5 is the new recommended release on main.
Highlights:
- Native minted Lean blocks can be labeled and followed by \leantexoutput{name} for matching Lean diagnostics and infoview-style output.
- Hidden snippets can use \leantex[infoview=lines:N]{...} to render output without duplicating source code.
- Native minted and macro outputs render plainly, without an extra LeanTeX heading or tcolorbox.
- Legacy v2 \begin{lean} blocks remain supported with the existing boxed display.
- Output-only snippets avoid writing duplicate generated code files, keeping generated artifacts lighter.
- README now documents the three maintained branches: main for v2.5, version2 for the earlier minted v2 line, and version1 for the original listings implementation.
Validation:
- python3 -m unittest discover -s tests -v: 50 tests passing
- python3 -m py_compile leantex/*.py: passing