Leni Aniva aniva
0 Followers · 1 Following
  • Stanford University Centaur Lab
  • https://leni.sh

  • Director of NorCal Hakkero Factory No. 1

  • Joined on 2023-08-21
Repositories
13
 Projects Packages Public Activity Starred Repositories
9
aniva pushed to goal/tactic at aniva/Pantograph 2024-09-08 14:14:10 -07:00
5e99237e09 fix: Tactics should produce `.syntheticOpaque` goals
aniva created branch goal/tactic in aniva/Pantograph 2024-09-08 14:14:10 -07:00
aniva created pull request aniva/Pantograph#99 2024-09-08 13:47:30 -07:00
feat: Collect holes in Lean file and put them into a GoalState
aniva created branch frontend/collect-holes in aniva/Pantograph 2024-09-08 13:45:21 -07:00
aniva pushed to frontend/collect-holes at aniva/Pantograph 2024-09-08 13:45:21 -07:00
860344f9c5 refactor: Factor out `FrontendM` driver
aniva closed issue aniva/Pantograph#93 2024-09-08 13:40:12 -07:00
Refactor out the Pantograph executable and lib into different targets
aniva commented on issue aniva/Pantograph#93 2024-09-08 13:40:12 -07:00
Refactor out the Pantograph executable and lib into different targets

Done #92

aniva opened issue aniva/Pantograph#98 2024-09-08 13:39:37 -07:00
Use MLList from Batteries
aniva pushed tag v0.2.18 to aniva/Pantograph 2024-09-08 12:27:33 -07:00
aniva deleted branch goal/automatic from aniva/Pantograph 2024-09-08 12:25:08 -07:00
aniva pushed to dev at aniva/Pantograph 2024-09-08 12:25:08 -07:00
27e4e45418 Merge pull request 'feat: Automatic Mode' (#92) from goal/automatic into dev
b645d79fda Merge branch 'dev' into goal/automatic
25bb964604 test: Automatic mode testing
e4d53733d0 feat: Simplify repl
68dac4c951 chore: Version bump to 0.2.18
Compare 10 commits »
aniva merged pull request aniva/Pantograph#92 2024-09-08 12:25:07 -07:00
feat: Automatic Mode
aniva pushed to goal/automatic at aniva/Pantograph 2024-09-08 12:13:49 -07:00
b645d79fda Merge branch 'dev' into goal/automatic
e36954a589 Merge pull request 'feat: Expose `GoalState` functions' (#94) from lib/export into dev
414f1c70fd Merge branch 'dev' into lib/export
7c49fcff27 refactor: Un-export two field accessor functions
f11c5ebaa3 doc: Add GPL License
Compare 8 commits »
aniva pushed to dev at aniva/Pantograph 2024-09-08 12:10:48 -07:00
e36954a589 Merge pull request 'feat: Expose `GoalState` functions' (#94) from lib/export into dev
414f1c70fd Merge branch 'dev' into lib/export
7c49fcff27 refactor: Un-export two field accessor functions
4042ec707e refactor: Use `Meta.mapMetaM`
8394e1b468 feat: Expose `conv` and `calc` tactics
Compare 6 commits »
aniva deleted branch lib/export from aniva/Pantograph 2024-09-08 12:10:48 -07:00
aniva merged pull request aniva/Pantograph#94 2024-09-08 12:10:47 -07:00
feat: Expose `GoalState` functions
aniva pushed to lib/export at aniva/Pantograph 2024-09-08 12:01:17 -07:00
414f1c70fd Merge branch 'dev' into lib/export
f11c5ebaa3 doc: Add GPL License
Compare 2 commits »
aniva pushed to goal/automatic at aniva/Pantograph 2024-09-08 11:57:57 -07:00
25bb964604 test: Automatic mode testing
aniva pushed to lib/export at aniva/Pantograph 2024-09-08 11:54:06 -07:00
7c49fcff27 refactor: Un-export two field accessor functions
aniva commented on issue aniva/Pantograph#23 2024-09-08 01:10:47 -07:00
Printing fine-grained delaboration structure

Alignment heuristics are not needed in Trillium anymore. This could still be useful to just provide training data, but I don't see a way to inject code into the Delab monad.