lean2md v0.2.1

lean2md v0.2.1 - Release Notes

Command-Line Interface Improvements

This release adds more flexible file processing options to the lean2md CLI:

• Single file processing: Process individual files with automatic output naming
  lean2md file.lean → Outputs file.md

• Specific file paths: Convert single files with custom target paths
  lean2md src/module.lean docs/output.md

Documentation

• Updated README with enhanced usage examples
• Added more comprehensive examples for all supported command patterns

Testing

• Added integration tests for all CLI operations
• Ensured consistent behavior across single-file and directory operations

This release makes lean2md more convenient for quick conversions of individual files and standalone modules in addition to the previously supported directory processing.

lean2md v0.2.0

lean2md v0.2.0 - Release Notes

Breaking Changes

• Consistent Marker Processing: All markers now work identically across all contexts
  • The --+ marker now works properly inside code blocks within comments (previously ignored)
  • This ensures predictable behavior regardless of where markers appear

Improvements

• Enhanced Marker Precedence: Clarified and documented marker precedence rules
• Test Coverage: Added tests for markers in nested code blocks
• Documentation
• Updated README to clearly explain the consistent marker behavior
• Added examples demonstrating marker usage in different contexts

This release primarily focuses on making marker behavior more consistent and predictable, particularly enhancing the --+ marker to work inside code blocks within comments.

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.