feat: Automatic Mode #92

aniva · 2024-09-06T17:53:00-07:00

aniva commented

2024-09-06 17:53:00 -07:00

For the people who don't want to manage their own resumption code.

Enable options.set { "automaticMode": true } to get the LeanDojo experience.

Disclaimer: Don't complain that MCTS doesn't work if you enable this. You asked for it.

refactor: Pull Repl out of main library.
refactor: All goal functions now take MVarId as parameters instead of goalId: Nat
refactor: IndexError is now no longer a part of TacticResult.

For the people who don't want to manage their own resumption code. Enable `options.set { "automaticMode": true }` to get the LeanDojo experience. Disclaimer: Don't complain that MCTS doesn't work if you enable this. You asked for it. * refactor: Pull Repl out of main library. * refactor: All goal functions now take `MVarId` as parameters instead of `goalId: Nat` * refactor: `IndexError` is now no longer a part of `TacticResult`.

aniva added this to the 0.3 milestone 2024-09-06 17:53:00 -07:00

aniva added the

part/Goal

category

feature

labels 2024-09-06 17:53:00 -07:00

aniva self-assigned this 2024-09-06 17:53:00 -07:00

aniva added 1 commit 2024-09-06 21:07:42 -07:00

82d99ccf9b

refactor: Use `MVarId` across the board

aniva added 2 commits 2024-09-06 21:32:13 -07:00

37473b3efb

feat: Automatic mode (auto resume)

e2ad6ce6b3

doc: Documentation for automatic mode

aniva added 1 commit 2024-09-06 22:02:03 -07:00

a7b30af36b

refactor: Refactor REPL out of main library

fix: Calc previous rhs not found bug

aniva added 1 commit 2024-09-06 22:22:45 -07:00

9b3eef35ec

fix: Forgot to include the current goals in resume

aniva commented

2024-09-06 23:20:10 -07:00

There's not a single unit test for this. Maybe I should write one, but I'm tired.

aniva added 2 commits 2024-09-07 14:03:45 -07:00

68dac4c951

chore: Version bump to 0.2.18

e4d53733d0

feat: Simplify repl

aniva added the

part/FFI

label 2024-09-07 14:05:27 -07:00

aniva added

part/REPL

and removed

part/FFI

labels 2024-09-07 14:06:35 -07:00

aniva added 1 commit 2024-09-08 11:57:58 -07:00

25bb964604

test: Automatic mode testing

refactor: Simplified integration test structure

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

b645d79fda

Merge branch 'dev' into goal/automatic

aniva merged commit 27e4e45418 into dev

2024-09-08 12:25:07 -07:00

aniva deleted branch goal/automatic

2024-09-08 12:25:07 -07:00

aniva referenced this issue from a commit

2024-09-08 12:25:08 -07:00

Merge pull request 'feat: Automatic Mode' (#92) from goal/automatic into dev

aniva referenced this pull request

2024-09-08 13:40:12 -07:00

Refactor out the Pantograph executable and lib into different targets #93

aniva modified the milestone from 0.3 to TACAS '25

2024-09-08 14:26:45 -07:00

Sign in to join this conversation.

No reviewers

No Label

No Milestone

No project

No Assignees

1 Participants

Notifications

Due Date

The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: aniva/Pantograph#92