aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity
505 Commits 11 Branches 20 Tags 1.8 MiB
Commit Graph

505 Commits

Author SHA1 Message Date
Leni Aniva 22ddfaaf21 Merge pull request 'feat: Error reporting in frontend' (#107) from frontend/error into dev 
Reviewed-on: #107
 2024-10-05 22:39:23 -07:00
Leni Aniva d0321e72dd
feat: Add message diagnostics to frontend.process 2024-10-05 14:49:17 -07:00
Leni Aniva 452c390711 Merge pull request 'feat: Collect holes in Lean file and put them into a `GoalState`' (#99) from frontend/collect-holes into dev 
Reviewed-on: #99
 2024-10-03 15:43:00 -07:00
Leni Aniva 10cb32e03f
Merge branch 'dev' into frontend/collect-holes 2024-10-03 11:47:38 -07:00
Leni Aniva a03eeddc9b
fix: Variable duplication in nested translation 2024-10-03 11:46:09 -07:00
Leni Aniva 530a1a1a97
fix: Extracting `sorry`s from coupled goals 2024-10-03 11:35:54 -07:00
Leni Aniva b174b4ea79 Merge pull request 'fix: Tactics should produce `.syntheticOpaque` goals' (#100) from goal/tactic into dev 
Reviewed-on: #100
 2024-10-03 08:47:30 -07:00
Leni Aniva ed1f96d7f7
Merge branch 'dev' into goal/tactic 2024-10-03 01:38:10 -07:00
Leni Aniva 143cd289bb
fix: Extraction of sorry's from nested tactics 2024-10-03 01:29:46 -07:00
Leni Aniva 18cd1d0388
fix: Extracting sorrys from sketches 2024-10-02 22:22:20 -07:00
Leni Aniva bec84f857b
fix: repl build failure 2024-09-09 18:43:34 -07:00
Leni Aniva fe8b259e4f
feat: Set root when there's just one mvar 2024-09-09 17:37:59 -07:00
Leni Aniva f729a357b9
Merge branch 'dev' into frontend/collect-holes 2024-09-09 17:35:10 -07:00
Leni Aniva 9075ded885
feat: Set `automaticMode` to true by default 2024-09-09 17:29:43 -07:00
Leni Aniva 9f0de0957e
doc: Update documentation for frontend command 2024-09-09 12:39:32 -07:00
Leni Aniva 762a139e78
feat: Export frontend functions 2024-09-09 12:30:32 -07:00
Leni Aniva 4f5950ed78
feat: Convert holes to goals 2024-09-09 12:26:46 -07:00
Leni Aniva 08fb53c020
test: Frontend process testing 2024-09-09 10:18:20 -07:00
Leni Aniva 8e3241c02a
refactor: Move all frontend functions to `Frontend` 2024-09-08 15:02:43 -07:00
Leni Aniva 5e99237e09
fix: Tactics should produce `.syntheticOpaque` goals 2024-09-08 14:13:39 -07:00
Leni Aniva 860344f9c5
refactor: Factor out `FrontendM` driver 2024-09-08 13:44:46 -07:00
Leni Aniva 27e4e45418 Merge pull request 'feat: Automatic Mode' (#92) from goal/automatic into dev 
Reviewed-on: #92
 2024-09-08 12:25:06 -07:00
Leni Aniva b645d79fda
Merge branch 'dev' into goal/automatic 2024-09-08 12:13:42 -07:00
Leni Aniva e36954a589 Merge pull request 'feat: Expose `GoalState` functions' (#94) from lib/export into dev 
Reviewed-on: #94
 2024-09-08 12:10:46 -07:00
Leni Aniva 414f1c70fd
Merge branch 'dev' into lib/export 2024-09-08 12:01:02 -07:00
Leni Aniva 25bb964604
test: Automatic mode testing 
refactor: Simplified integration test structure
 2024-09-08 11:57:39 -07:00
Leni Aniva 7c49fcff27
refactor: Un-export two field accessor functions 
User should use `lean_ctor_get`
 2024-09-08 11:53:54 -07:00
Leni Aniva f11c5ebaa3
doc: Add GPL License 2024-09-07 14:11:04 -07:00
Leni Aniva e4d53733d0
feat: Simplify repl 2024-09-07 14:03:29 -07:00
Leni Aniva 68dac4c951
chore: Version bump to 0.2.18 2024-09-07 13:55:41 -07:00
Leni Aniva 4042ec707e
refactor: Use `Meta.mapMetaM` 2024-09-07 13:54:52 -07:00
Leni Aniva 8394e1b468
feat: Expose `conv` and `calc` tactics 2024-09-07 13:47:55 -07:00
Leni Aniva 9b3eef35ec
fix: Forgot to include the current goals in resume 2024-09-06 22:22:19 -07:00
Leni Aniva a7b30af36b
refactor: Refactor REPL out of main library 
fix: Calc previous rhs not found bug
 2024-09-06 22:01:36 -07:00
Leni Aniva e2ad6ce6b3
doc: Documentation for automatic mode 2024-09-06 21:32:02 -07:00
Leni Aniva 37473b3efb
feat: Automatic mode (auto resume) 2024-09-06 21:30:11 -07:00
Leni Aniva 82d99ccf9b
refactor: Use `MVarId` across the board 2024-09-06 21:07:12 -07:00
Leni Aniva 02556f3c79
feat: Expose `GoalState` functions 2024-09-05 11:56:06 -07:00
Leni Aniva 9c40a83956
fix: Instantiate type when detecting `eq` 2024-09-03 19:05:16 -07:00
Leni Aniva f8df2599f9
fix: Use `replaceMainGoal` instead of `setGoals` 2024-09-03 14:18:47 -07:00
Leni Aniva 8d2cd6dfc7
fix: Bindings in prograde tactics 2024-09-03 14:15:52 -07:00
Leni Aniva 948b535b5d Merge pull request 'feat: Prograde tactics' (#83) from tactic/eval into dev 
Reviewed-on: #83
 2024-08-31 20:04:38 -07:00
Leni Aniva edec0f5733
feat: Use CoreM for diag monad 2024-08-26 13:42:14 -04:00
Leni Aniva 0c529c5cd9
Merge branch 'misc/test-driver' into tactic/eval 2024-08-18 12:24:26 -07:00
Leni Aniva 76765c913c
test: Use `lake test`. Retired `Makefile` 2024-08-18 12:22:59 -07:00
Leni Aniva 3733c10a4e
refactor: Unify call convention 
Induction like tactics should return `Array InductionSubgoal`. Branching
tactics should return their branch first.
 2024-08-17 16:47:21 -07:00
Leni Aniva 5d43068ec3
fix: Flake check failure 2024-08-17 02:07:17 -07:00
Leni Aniva f87eed817f
build: Move non-package output to legacyPackages 2024-08-17 01:59:48 -07:00
Leni Aniva 43e11f1ba3
refactor: Always display isInaccessible 2024-08-17 00:53:38 -07:00
Leni Aniva 0c469027c6
fix: Refactor mvar collection in assign tactic 2024-08-17 00:50:02 -07:00