Convert Lean 4 .olean files to s-expressions

This utility converts compiled Lean 4 files to files to the S-expression format. These can be used for further processing, e.g., for machine-learning purposes.

Installation

In order to use lean2sexp in a Lean project, add the following line to lakefile.lean:

require lean2sexp from git
  "https://github.com/andrejbauer/lean2sexp.git" @ "main"

Usage

By default, lean2sexp converts all files found in the project subdirectory build/lib and stores them in the folder sexp. (This means you should build the project before running lean2sexp, and possibly remove sexp folder to get rid of stale files.)

To generate the files with s-expressions, run

lake exe lean2sexp

Optionally, you may provide the input and output folders (or just the input folder):

lake exe lean2sexp 〈oleanDir〉 〈sexpDir〉

Background

The utility is fashioned after a similar Agda backend, implemented in the ast-dump branch of this Agda fork, see src/full/Agda/Interaction/Highlighting/Sexp therein.