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

aniva commented

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

Owner

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

refactor: Factor out FrontendM driver 860344f9c5

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

refactor: Move all frontend functions to Frontend 8e3241c02a

aniva commented

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

Author

Owner

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

test: Frontend process testing 08fb53c020

aniva added 1 commit

2024-09-09 12:27:01 -07:00

feat: Convert holes to goals 4f5950ed78

aniva added 1 commit

2024-09-09 12:30:48 -07:00

feat: Export frontend functions 762a139e78

aniva added 1 commit

2024-09-09 12:39:50 -07:00

doc: Update documentation for frontend command 9f0de0957e

aniva commented

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

Author

Owner

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

Merge branch 'dev' into frontend/collect-holes f729a357b9

aniva added 1 commit

2024-09-09 17:38:22 -07:00

feat: Set root when there's just one mvar fe8b259e4f

aniva added 1 commit

2024-09-09 18:43:54 -07:00

fix: repl build failure bec84f857b

aniva commented

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

Author

Owner

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

fix: Extracting sorrys from sketches 18cd1d0388

aniva added 1 commit

2024-10-03 01:30:12 -07:00

fix: Extraction of sorry's from nested tactics 143cd289bb

aniva commented

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

Author

Owner

Fixed #103

aniva added 1 commit

2024-10-03 11:36:19 -07:00

fix: Extracting sorrys from coupled goals 530a1a1a97

aniva commented

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

Author

Owner

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

fix: Variable duplication in nested translation a03eeddc9b

aniva added 1 commit

2024-10-03 11:47:43 -07:00

Merge branch 'dev' into frontend/collect-holes 10cb32e03f