aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 11 Pull Requests 2 Packages Projects Releases Wiki Activity
575 Commits 8 Branches 21 Tags 50 MiB
Commit Graph

575 Commits

Author SHA1 Message Date
Leni Aniva 4d295bd9ff Merge pull request 'doc: Manual about `env.{describe,module_read}`' (#165) from env/module into dev 
Reviewed-on: #165
 2025-01-26 22:04:28 -08:00
Leni Aniva 7d6ad1ebb9 Merge pull request 'chore: Code cleanup' (#164) from chore/cleanup into dev 
Reviewed-on: #164
 2025-01-26 22:04:12 -08:00
Leni Aniva 003a63bd13
doc: Manual about `env.{describe,module_read}` 2025-01-24 20:21:31 -08:00
Leni Aniva 970c16a0a4
chore: Use `StateRefT` in `Repl.lean` 2025-01-24 20:19:07 -08:00
Leni Aniva 6a7830cb71
fix: Remove spurious print 2025-01-24 19:24:54 -08:00
Leni Aniva 787c9e606d
chore: Cleanup REPL loop 2025-01-24 19:22:58 -08:00
Leni Aniva 976646fb67
chore: Use repeat-break structure 2025-01-24 19:11:05 -08:00
Leni Aniva 418d630255
fix: Remove unused variable 2025-01-24 19:06:07 -08:00
Leni Aniva b67d3eccc4 Merge pull request 'fix: Panic in `exprProjToApp`' (#161) from bug/expr-proj-to-app-panic into dev 
Reviewed-on: #161
 2025-01-24 15:05:04 -08:00
Leni Aniva 6f792b0657
Merge branch 'dev' into bug/expr-proj-to-app-panic 2025-01-24 15:03:13 -08:00
Leni Aniva ed1d5d7b58 Merge pull request 'feat: Module reading functions' (#159) from env/module into dev 
Reviewed-on: #159
 2025-01-24 15:01:16 -08:00
Leni Aniva f7f1272145
Merge branch 'dev' into env/module 2025-01-24 15:01:00 -08:00
Leni Aniva be8dee6731
test: Add test for module read 2025-01-24 15:00:35 -08:00
Leni Aniva 549be79cbf Merge pull request 'feat: Pickle constants in goal state' (#157) from serial/pickle into dev 
Reviewed-on: #157
 2025-01-24 14:52:52 -08:00
Leni Aniva 5c1e7599c0
feat: Projection export function 2025-01-24 14:44:09 -08:00
Leni Aniva 8ce4cbdcf5
feat: Printing field projection in sexp 2025-01-22 13:01:47 -08:00
Leni Aniva 3a26bb1924
fix: Analyze projection application 2025-01-22 12:49:33 -08:00
Leni Aniva 5994f0ddf0
fix: Conditional handling of `.proj` 2025-01-17 23:10:03 -08:00
Leni Aniva 59935e386b Merge pull request 'feat: Draft tactic REPL interface' (#158) from tactic/draft into dev 
Reviewed-on: #158
 2025-01-16 10:32:47 -08:00
Leni Aniva bc4bf47c8b
feat: Implement repl interfaces 2025-01-15 21:23:37 -08:00
Leni Aniva c9f524b9ae
feat: Implement `env.describe` and `env.module_read` 2025-01-15 21:20:05 -08:00
Leni Aniva 4f5ffc1ffb
feat: Protocol for module access 2025-01-15 21:02:04 -08:00
Leni Aniva 62363cb943
fix: Over-eager assertion of fvarId validity 2025-01-14 13:21:38 -08:00
Leni Aniva 9d445783c2
feat: Draft tactic REPL interface 2025-01-13 12:50:25 -08:00
Leni Aniva fef7f1e2f3
feat: Pickle constants in goal state 2025-01-13 12:43:42 -08:00
Leni Aniva c1f63af019 chore: Update version to 0.2.25 2025-01-13 12:29:11 -08:00
Leni Aniva b8b46c4a9c Merge pull request 'chore: Update Lean to v4.15.0' (#134) from misc/version into dev 
Reviewed-on: #134
 2025-01-13 12:28:49 -08:00
Leni Aniva 60e78b322e
fix: Test failures 2025-01-13 12:28:16 -08:00
Leni Aniva 06fdf7e678
chore: Update Lean to v4.15.0 2025-01-13 11:09:55 -08:00
Leni Aniva 5e61282660
test: Source location extraction 2025-01-13 10:30:26 -08:00
Leni Aniva 9d2a999a4f
merge: branch 'dev' into misc/version 2025-01-13 10:29:50 -08:00
Leni Aniva db24650aec Merge pull request 'feat: Draft tactic' (#153) from goal/tactic-draft into dev 
Reviewed-on: #153
 2025-01-13 10:22:35 -08:00
Leni Aniva 6a9ba4bb15
Merge branch 'dev' into goal/tactic-draft 2025-01-13 10:22:05 -08:00
Leni Aniva ebde7c9eed
feat: Prohibit coupling in drafting 2025-01-13 10:20:36 -08:00
Leni Aniva ef4e5ecbf8
chore: Update version 2025-01-10 12:55:26 -08:00
Leni Aniva a374af3a5f Merge pull request 'fix: Incorrect binder capture' (#152) from bug/incorrect-binder-capture into dev 
Reviewed-on: #152
 2025-01-10 12:49:14 -08:00
Leni Aniva 9eec14503a
Merge branch 'dev' into bug/incorrect-binder-capture 2025-01-10 12:48:18 -08:00
Leni Aniva 814f36eb63 Merge pull request 'feat: Add source location extraction' (#154) from env/inspect into dev 
Reviewed-on: #154
 2025-01-10 12:47:35 -08:00
Leni Aniva 4a4b02d7b0
test: Source location extraction 2025-01-10 12:47:13 -08:00
Leni Aniva 97eaadc93c
feat: Add source location extraction 2025-01-10 12:16:23 -08:00
Leni Aniva aa066b8634
fix: Add test 2025-01-08 22:53:10 -08:00
Leni Aniva 072d351f04
fix: Delete extraneous test 2025-01-08 22:47:08 -08:00
Leni Aniva cb46b47a60
test: Draft tactic test 2025-01-08 22:23:30 -08:00
Leni Aniva 5ce6123de7
feat: Draft tactic 2025-01-08 19:56:14 -08:00
Leni Aniva f891960362
fix: Volatile test 2025-01-07 17:52:28 -08:00
Leni Aniva 6302b747b8
feat: Improve error message clarity 2025-01-07 17:51:32 -08:00
Leni Aniva 07e737eb81 Merge pull request 'feat: Simplify sexp printing' (#149) from delate/sexp into dev 
Reviewed-on: #149
 2025-01-07 17:31:29 -08:00
Leni Aniva 56f40462ae Merge pull request 'fix: Unnecessary instantiation call' (#148) from goal/tactic into dev 
Reviewed-on: #148
 2025-01-07 17:31:08 -08:00
Leni Aniva 524314721b
feat: Gate type error collection behind flag 2025-01-07 19:40:03 +09:00
Leni Aniva 5a05e9e8d4
test: Add binder capturing test 2024-12-22 08:47:38 +09:00