This allows users to much more easily test the behavior of mathport on small examples without having to go through the whole PR pipeline first or recompiling many things. The idea is that you can directly modify Oneshot/lean3-in/main.lean with some test code you would like to have mathported, and Oneshot/lean4-in/Oneshot.lean can contain additional #align directives not included in mathlib4. Running make oneshot will produce output in Outputs/src/oneshot/Oneshot/Main.lean.
This allows users to much more easily test the behavior of mathport on small examples without having to go through the whole PR pipeline first or recompiling many things. The idea is that you can directly modify
Oneshot/lean3-in/main.leanwith some test code you would like to have mathported, andOneshot/lean4-in/Oneshot.leancan contain additional#aligndirectives not included in mathlib4. Runningmake oneshotwill produce output inOutputs/src/oneshot/Oneshot/Main.lean.