feat: Collect holes in Lean file and put them into a GoalState #99

aniva · 2024-09-08T13:47:29-07:00

aniva commented

2024-09-08 13:47:29 -07:00

refactor: Moved all FrontendM functions into Frontend/.
feat: Export frontend functions
feat: Add frontend.process (refactored from compile.unit) command, which runs the frontend on a file.
doc: Updated documentation
chore: Version bump to 0.2.19 (major command modification)

* refactor: Moved all `FrontendM` functions into `Frontend/`. * feat: Export frontend functions * feat: Add `frontend.process` (refactored from `compile.unit`) command, which runs the frontend on a file. * doc: Updated documentation * chore: Version bump to 0.2.19 (major command modification)

aniva added the

labels 2024-09-08 13:47:29 -07:00

aniva self-assigned this 2024-09-08 13:47:29 -07:00

aniva added 1 commit 2024-09-08 13:47:30 -07:00

860344f9c5

refactor: Factor out `FrontendM` driver

aniva added this to the TACAS '25 milestone 2024-09-08 13:48:41 -07:00

aniva added 1 commit 2024-09-08 15:03:05 -07:00

8e3241c02a

refactor: Move all frontend functions to `Frontend`

aniva commented

2024-09-08 15:06:40 -07:00

We need to think about what the interface should look like. IMO the user should input a theorem name or line number, and the repl generates a goal state for the theorem/example/etc. on that line number. This requires traversing the entire file every time.

The current best solution is to write all the tests into one file, compile it, and load it as the environment.

I don't think there's a very nice meet in the middle solution given Lean's convoluted type system and possible theorem inter-dependencies.

The simplest solution is to extract data from only the first compilation unit that has holes. This avoids the problematic inter-dependency issue.

We need to think about what the interface should look like. IMO the user should input a theorem name or line number, and the repl generates a goal state for the theorem/example/etc. on that line number. This requires traversing the entire file every time. The current best solution is to write all the tests into one file, compile it, and load it as the environment. I don't think there's a very nice meet in the middle solution given Lean's convoluted type system and possible theorem inter-dependencies. The simplest solution is to extract data from only the first compilation unit that has holes. This avoids the problematic inter-dependency issue.

aniva added 1 commit 2024-09-09 10:19:41 -07:00

08fb53c020

test: Frontend process testing

aniva added 1 commit 2024-09-09 12:27:01 -07:00

4f5950ed78

feat: Convert holes to goals

aniva added 1 commit 2024-09-09 12:30:48 -07:00

762a139e78

feat: Export frontend functions

aniva added 1 commit 2024-09-09 12:39:50 -07:00

9f0de0957e

doc: Update documentation for frontend command