aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity
551 Commits 10 Branches 21 Tags 50 MiB
Commit Graph

353 Commits

Author SHA1 Message Date
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 06fdf7e678
chore: Update Lean to v4.15.0 2025-01-13 11:09:55 -08:00
Leni Aniva 9d2a999a4f
merge: branch 'dev' into misc/version 2025-01-13 10:29:50 -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 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 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 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 524314721b
feat: Gate type error collection behind flag 2025-01-07 19:40:03 +09:00
Leni Aniva 48b924fae2
fix(frontend): Incorrect capture of binder term 2024-12-20 19:12:12 +09:00
Leni Aniva b42d917aa7
fix: Unnecessary instantiation call 2024-12-17 08:18:27 +09:00
Leni Aniva 53bad1c4c9
refactor: Remove obsolete sanitize option 2024-12-15 12:52:08 -08:00
Leni Aniva 7a3b89cc0e
feat: Simplify sexp binder 2024-12-15 12:49:02 -08:00
Leni Aniva c0090dec97
fix: Quote string literal in sexp 2024-12-15 12:40:47 -08:00
Leni Aniva 13e01b9e62
Merge branch 'dev' into misc/version 2024-12-11 20:53:32 -08:00
Leni Aniva 0fa57a5a15
Merge branch 'dev' into goal/print 2024-12-11 16:51:58 -08:00
Leni Aniva 2f732a7f20
feat: Print goals in `goal.print` 2024-12-11 16:49:52 -08:00
Leni Aniva eeb336c944
Merge branch 'dev' into goal/print 2024-12-11 16:40:01 -08:00
Leni Aniva bb445f4d73
chore: Update version 2024-12-11 16:38:59 -08:00
Leni Aniva ab77418e24
fix: Drop previous message lists 2024-12-11 09:05:47 -08:00
Leni Aniva f2f71a6028
fix: Reset core message log 2024-12-11 09:01:57 -08:00
Leni Aniva 7cba8efd54
Merge branch 'dev' into frontend/infotree 2024-12-11 01:14:15 -08:00
Leni Aniva 4217dbcf80
Merge branch 'dev' into bug/tactic-failure-placeholder 2024-12-11 01:08:44 -08:00
Leni Aniva cb87fcd9dd
fix: Insert `mvarDeps` 2024-12-11 00:16:52 -08:00
Leni Aniva e0e5c9ec68
chore: Code cleanup 2024-12-10 23:51:47 -08:00
Leni Aniva 755ba13c1b
fix: Set `synthesizeSyntheticMVarsNoPostponing` 2024-12-10 23:48:46 -08:00
Leni Aniva 1d10cd2b20
fix: Collect errored mvars by iterating errorInfo 2024-12-10 23:16:33 -08:00
Leni Aniva 0725d865de
feat: Print value of arbitrary mvar in goal state 2024-12-10 14:14:59 -08:00
Leni Aniva 681c3fb78d
fix: Disallow indeterminant type `sorry` 2024-12-10 12:21:56 -08:00
Leni Aniva 37a5884be4
fix: Use `ppSyntax` instead of `ppTactic` 2024-12-09 21:39:33 -08:00
Leni Aniva 1527743900
refactor: Optionalize CompilationUnit 2024-12-09 21:00:33 -08:00
Leni Aniva eb0374dfb3
feat: Collect new constants in repl 2024-12-09 20:57:25 -08:00
Leni Aniva dd00d803d1
feat: Collect sorry/elab failure boundaries 2024-12-09 20:38:27 -08:00
Leni Aniva e9cbc6eab3
chore: Update version 2024-12-09 20:17:55 -08:00
Leni Aniva 0b4ded1049
fix: Collect sorrys and type mismatches 2024-12-09 20:15:53 -08:00
Leni Aniva 5ef2b5c118
feat: Collect newly defined constants 2024-12-09 19:40:00 -08:00
Leni Aniva d040d2006c
fix: Do not guard mvar errors in other tactics 2024-12-09 17:58:08 -08:00
Leni Aniva 47d26badc8
feat: Capture mvar errors 2024-12-09 17:30:33 -08:00
Leni Aniva 2d068ecd50
fix: Use guarded `isDefEq` 2024-12-09 00:06:20 -08:00
Leni Aniva 17ab2eafd8
fix: Halt on match guard 2024-12-09 00:03:53 -08:00
Leni Aniva ea813e5bc5
feat: Monadic info collection 2024-12-08 23:21:36 -08:00
Leni Aniva b950dc9b1a
fix: Verbose printing of infotree 2024-12-08 22:51:55 -08:00
Leni Aniva 9ede3cf717
feat: InfoTree printing 2024-12-08 15:38:03 -08:00