aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 2 Packages Projects Releases Wiki Activity
775 Commits 4 Branches 27 Tags 2 MiB
Commit Graph

775 Commits

Author SHA1 Message Date
Leni Aniva c013e66144
doc: Wording 2025-07-11 20:17:27 -07:00
Leni Aniva 40bf3b2100
doc: Remove stale repl documentation 2025-07-11 20:15:14 -07:00
Leni Aniva e8fdd906aa
doc: Remove stale documentation 2025-07-11 20:09:54 -07:00
Leni Aniva b5cb4bfa57 Merge pull request 'fix(frontend): Tomograph compilation' (#235) from frontend/tomograph into dev 
Reviewed-on: #235
 2025-07-11 19:44:24 -07:00
Leni Aniva 8ede816781
Merge branch 'dev' into frontend/tomograph 2025-07-11 16:31:11 -07:00
Leni Aniva 672b2a11f9
build: Update flake 2025-07-11 16:30:28 -07:00
Leni Aniva 147d3cc87e
chore: Remove tomograph as default target 2025-07-11 16:27:14 -07:00
Leni Aniva 752d13182d
fix(frontend): Tomograph fix 2025-07-11 16:24:30 -07:00
Leni Aniva cb44b65f1e Merge pull request 'feat(frontend): Command-level `frontend.process`' (#229) from frontend/command into dev 
Reviewed-on: #229
 2025-07-11 16:05:56 -07:00
Leni Aniva 387a6c2f08 Merge pull request 'refactor: Use consistent error handling' (#233) from goal/message into dev 
Reviewed-on: #233
 2025-07-11 15:01:43 -07:00
Leni Aniva 58b52359e1
doc: Wording 2025-07-11 15:01:00 -07:00
Leni Aniva 18edccd4d0
doc: Move repl documentation to `doc/repl.md` 2025-07-11 15:00:23 -07:00
Leni Aniva a261a4099a
feat(frontend): Cancel token in frontend 2025-07-11 14:55:40 -07:00
Leni Aniva 9fdaefe539
doc: Cleanup tactic documentation 2025-07-10 15:30:46 -07:00
Leni Aniva bd7dde8235
chore: Code cleanup 2025-07-10 15:29:13 -07:00
Leni Aniva 1fcc24283b
refactor: Use consistent error handling 2025-07-10 13:18:35 -07:00
Leni Aniva ce41832081 Merge pull request 'feat: Display `Message` metadata' (#232) from frontend/message into dev 
Reviewed-on: #232
 2025-07-10 11:45:44 -07:00
Leni Aniva ac8dcc4130
feat: Display `Message` metadata 2025-07-10 11:42:25 -07:00
Leni Aniva d85c804133 Merge pull request 'feat(repl): Replace StdIO when executing IO-based monads' (#231) from repl/replace-io into dev 
Reviewed-on: #231
 2025-07-08 14:30:50 -07:00
Leni Aniva 855a882f7b
fix(repl): Extra newline in stdout bypass 2025-07-08 14:29:37 -07:00
Leni Aniva 2593c5bf60
feat(repl): Isolate stdout 2025-07-08 14:16:37 -07:00
Leni Aniva 60dc07e559 Merge pull request 'fix(tactic): Erase finished calc goal' (#228) from fix/calc-erase-goal into dev 
Reviewed-on: #228
 2025-07-07 14:49:10 -07:00
Leni Aniva 92befda2ff
test(tactic): Check fragments have been erased 2025-07-07 14:47:50 -07:00
Leni Aniva 2dbbe2509e
fix(tactic): Erase finished calc goal 2025-07-02 15:46:29 -07:00
Leni Aniva aef8276c99 Merge pull request 'feat(frontend): Tomogram' (#220) from frontend/tomogram into dev 
Reviewed-on: #220
 2025-07-02 15:18:18 -07:00
Leni Aniva c1c7848bca
chore: Format code 2025-07-02 15:18:02 -07:00
Leni Aniva 48046b8b5a
fix(tomograph): Import search directory 2025-07-02 15:14:11 -07:00
Leni Aniva 80fb7f30c3
Merge branch 'dev' into frontend/tomogram 2025-07-02 15:03:24 -07:00
Leni Aniva 8ee1607b45 Merge pull request 'test(repl): MVar name mismatch fix' (#227) from chore/toolchain into dev 
Reviewed-on: #227
 2025-07-02 15:03:09 -07:00
Leni Aniva 726c2ed145
test(repl): MVar name mismatch fix 2025-07-02 15:02:35 -07:00
Leni Aniva e5a7b30f51
Merge branch 'dev' into frontend/tomogram 2025-07-02 14:59:39 -07:00
Leni Aniva d1998b129a Merge pull request 'chore: Update Lean to v4.21.0' (#223) from chore/toolchain into dev 
Reviewed-on: #223
 2025-07-02 14:59:29 -07:00
Leni Aniva 737fd607e8
refactor: Add heuristic case to `isAuxLemma` 2025-07-02 14:54:13 -07:00
Leni Aniva 1f35820e1d
test: Fix unit test failures 2025-07-02 14:40:47 -07:00
Leni Aniva ec78324f9f
feat(repl): Improve tomograph's info 2025-07-02 14:32:24 -07:00
Leni Aniva 2cec5bc881
Merge branch 'dev' into frontend/tomogram 2025-07-02 13:20:00 -07:00
Leni Aniva 7a18fb1f9c
chore: Update version to v0.3.4 2025-07-01 15:43:21 -07:00
Leni Aniva 4c7f77b7ca Merge pull request 'doc: Remove constraint on pick_goal' (#224) from doc/rationale into dev 
Reviewed-on: #224
 2025-07-01 15:41:55 -07:00
Leni Aniva 50bb48f2ed
doc: Remove constraint on pick_goal 2025-06-30 15:56:48 -07:00
Leni Aniva f26b7fc177 Merge pull request 'fix(goal): Unknown metavariable problem during fragment initialization' (#222) from bug/unknown-metavariable-fragment into dev 
Reviewed-on: #222
 2025-06-30 15:28:28 -07:00
Leni Aniva 16474b2ce8
test(repl): Add test for conv and calc 2025-06-30 15:27:51 -07:00
Leni Aniva 3fab7e7818
fix(repl): Allow .none in parentExpr 2025-06-30 15:08:46 -07:00
Leni Aniva 7b96652c87
chore: Update Lean to v4.21.0 2025-06-30 15:05:07 -07:00
Leni Aniva dd7c6c36c8
fix(goal): Allow parent expr to be fragments 2025-06-30 15:00:30 -07:00
Leni Aniva 8857b88d9a
fix(goal): Restore elaboration monad 2025-06-30 14:52:38 -07:00
Leni Aniva 2a87ed2e46 Merge pull request 'feat(serial): Pickle environment delta's' (#221) from serial/delta into dev 
Reviewed-on: #221
 2025-06-27 16:02:21 -07:00
Leni Aniva f4b6996f9e
test: Ignore branch unification test 
We'll handle this in Lean v4.21.0
 2025-06-27 16:01:13 -07:00
Leni Aniva 349cff6f05
test(goal): Collision of aux lemma names 2025-06-26 16:41:49 -07:00
Leni Aniva f914e161e8
fix(goal): Reset messages in replay 2025-06-26 16:23:10 -07:00
Leni Aniva 4df8fcda97
Merge branch 'dev' into serial/delta 2025-06-26 15:52:36 -07:00