I have a recent interest in formalizing mathematics in Lean4. But I thought it would be useful to try to do relatively ordinary computer programming tasks in Lean, as a learning experience. (I should point out that I come to this already as a bit of functional programming fan.)

MLML

So: I built a tokenizer-parser-decoder for a small configuration language that I called MLML (“my little markup language”). (I used to use dhall for tasks like this, but don’t need all its features and thought it would be educational and interesting to roll my own.)

The README at the repository has a bit of an overview of the specifications.

course-planner

One frequent task when teaching is to produce semester schedule(s) for aspects of a course.

I used the MLML configuration language to provide course-planning tools for this requirement: see the repository here: course-planner

This tool uses an MLML semester specification – see e.g. this example – together with an MLML course specification – see e.g. this example – to produce markdown descriptions of the schedule – see e.g. the lecture schedule for this sample class and the org-mode schedule info for this sample class.

publications

I wrote a tool to use MLML to keep track of publication information, as well; see the repository here: pubs

Using an MLML specification, this tool actually produces the publication-list part of my CV and the publication-list part of this web-site.

Here is an example of an MLML specification of a few manuscripts.

And here are the two forms of output from this data:

• manuscript details
• cv style output

grade-keeper

While I’m at it, I should also mention this tool, though it is not written in Lean nor does it use MLML. It is written in Idris2.

It produced (markdown) reports of grade for my class. From the README of the gradekeeper repo:

A grade computation and reporting pipeline for university courses. The core engine is an Idris 2 program that reads a course specification and student score data, computes final grades, and produces a Markdown report. Supporting Guile Scheme scripts and a Makefile handle data wrangling and glue the pipeline together.

Overview

The pipeline takes three inputs for a given course:

1. A course specification (.scm s-expression file) describing score items, grade formulas, grade cutoffs, and any per-student exceptions.
2. A Canvas grade export (CSV) downloaded from the Canvas LMS.
3. A SIS enrollment export (.xlsx) from the university’s student information system.

It produces:

• A Markdown grade report (<course>--<term>--grade-report.md)
• HTML and PDF renderings of that report (via pandoc)