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.