Seasawhermk-exercise

Simple and intuitive tool to manage exercises in textbooks written in Lean.

mk-exercise

This tool erases parts of Lean code and replaces them with sorry. I developed this to make it easier to manage exercises in textbooks written in Lean.

This is inspired by a script in a glimpse of lean.

How to use

Basic usage

Add this repository to your lakefile:

require «mk-exercise» from git
  "https://github.com/Seasawher/mk-exercise" @ "main"

Don't forget to run lake update mk-exercise after editing the lakefile. And simply run lake exe mk_exercise <input_dir> <output_dir>.

Setup GitHub Action

GitHub Action allows you to run this every time a particular branch is updated, automatically updating the exercises to the latest state. You may wish to look at yuma-mizuno/lean-math-workshop, where exercises are managed using this tool.

Features

  • Replace the code enclosed by -- sorry with sorry, preserving indentation.
  • Replace the inline code enclosed by /-+-/ with sorry.
  • Replace the code after /- sorry -/ with sorry.
  • Lines ending with --## are ignored.
  • Blocks enclosed with --##-- are ignored.

Check the test code for more information.