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

aniva commented

2024-09-09 17:26:02 -07:00

We should probably assign the root variable when there's just one goal to avoid surprises for our users.

aniva added 1 commit 2024-09-09 17:35:24 -07:00

f729a357b9

Merge branch 'dev' into frontend/collect-holes

aniva added 1 commit 2024-09-09 17:38:22 -07:00

fe8b259e4f

feat: Set root when there's just one mvar

aniva added 1 commit 2024-09-09 18:43:54 -07:00

bec84f857b

fix: repl build failure

aniva commented

2024-09-09 19:32:41 -07:00

https://github.com/lenianiva/PyPantograph/pull/13

Seems fine. Testing has passed.

https://github.com/lenianiva/PyPantograph/pull/13 Seems fine. Testing has passed.

aniva added 1 commit 2024-10-02 22:22:45 -07:00

18cd1d0388

fix: Extracting sorrys from sketches

aniva added 1 commit 2024-10-03 01:30:12 -07:00

143cd289bb

fix: Extraction of sorry's from nested tactics

aniva commented

2024-10-03 01:31:02 -07:00

Fixed #103

aniva added 1 commit 2024-10-03 11:36:19 -07:00

530a1a1a97

fix: Extracting `sorry`s from coupled goals

aniva commented

2024-10-03 11:38:21 -07:00

Currently there's a variable duplication issue in coupled goals; It seems like every binder gets duplicated in the w goal.

def test_sorry_in_coupled: TestT MetaM Unit := do
  let sketch := "
example : ∀ (y: Nat), ∃ (x: Nat), y + 1 = x := by
  intro y
  apply Exists.intro
  case h => sorry
  case w => sorry
  "
  let goalStates ← (collectSorrysFromSource sketch).run' {}
  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
  addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
    {
      target := { pp? := "y + 1 = ?w" },
      vars := #[{
           userName := "y",
           type? := .some { pp? := "Nat" },
        }
      ],
    },
    {
      userName? := .some "w",
      target := { pp? := "Nat" },
      vars := #[{
           userName := "y✝",
           isInaccessible := true,
           type? := .some { pp? := "Nat" },
        }, {
           userName := "y",
           type? := .some { pp? := "Nat" },
        }
      ],
    }
  ])

Currently there's a variable duplication issue in coupled goals; It seems like every binder gets duplicated in the `w` goal. ```lean def test_sorry_in_coupled: TestT MetaM Unit := do let sketch := " example : ∀ (y: Nat), ∃ (x: Nat), y + 1 = x := by intro y apply Exists.intro case h => sorry case w => sorry " let goalStates ← (collectSorrysFromSource sketch).run' {} let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}" addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[ { target := { pp? := "y + 1 = ?w" }, vars := #[{ userName := "y", type? := .some { pp? := "Nat" }, } ], }, { userName? := .some "w", target := { pp? := "Nat" }, vars := #[{ userName := "y✝", isInaccessible := true, type? := .some { pp? := "Nat" }, }, { userName := "y", type? := .some { pp? := "Nat" }, } ], } ]) ```

aniva added 1 commit 2024-10-03 11:46:28 -07:00

a03eeddc9b

fix: Variable duplication in nested translation

aniva added 1 commit 2024-10-03 11:47:43 -07:00

10cb32e03f

Merge branch 'dev' into frontend/collect-holes

aniva merged commit 452c390711 into dev

2024-10-03 15:43:01 -07:00

aniva deleted branch frontend/collect-holes

2024-10-03 15:43:01 -07:00

aniva referenced this issue from a commit

2024-10-03 15:43:02 -07:00