lean4-htt/tests/lean/leanpkg/build_error/src
..
err.lean