lean2md v0.1.0 - Initial Release

The first release of lean2md, a command-line tool that converts Lean files to Markdown documents, preserving code structure and comments.

Features

• Converts Lean comments (/- ... -/) to Markdown text
• Maintains Lean code blocks inside Markdown code fences
• Special handling for docstrings and custom markers
• Built-in quiz generation for mdbook-quiz integration
• Directory structure preservation from source to target

Special Markers

• --# at the end of a line: Ignores the entire line
• --#--: Lines between two --#-- markers are completely ignored
• --+ at the end of a docstring: The docstring is formatted as an admonish block
• --! at the end of a line: Forces the line to be included in the output
• Quiz support with --@quiz:name and --@quiz-end markers

Installation

# Clone the repository
git clone https://github.com/fosterfarrell9/lean2md.git
cd lean2md
# Build the project
cargo build --release
# The executable will be in target/release/lean2md

Usage

lean2md <lean_src_dir> <md_tgt_dir>

For more details, see the README.