aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity
426 Commits 6 Branches 17 Tags 1.3 MiB
Commit Graph

426 Commits

Author SHA1 Message Date
Leni Aniva 1a99a2e7b2 fix: Sanitize name in universe levels 2023-10-29 13:03:48 -07:00
Leni Aniva 60854525b9 feat: Simplify printing of function applications 2023-10-29 12:50:36 -07:00
Leni Aniva e523e8bcc6 chore: Version bump (breaking change) 2023-10-29 11:57:24 -07:00
Leni Aniva de250eafd0 feat: Print names in one segment separated with . 2023-10-29 11:56:56 -07:00
Leni Aniva c0dfa04b18 feat: Simplify name printing 2023-10-29 11:18:35 -07:00
Leni Aniva 4ce932eb3b Merge pull request 'Enable handling of m-Coupled goals' (#20) from goal/dependency into dev 
Reviewed-on: #20
 2023-10-27 19:30:20 -07:00
Leni Aniva 045181356c feat: Add REPL function for root expression 2023-10-27 15:41:12 -07:00
Leni Aniva 41e1f64d44 Merge branch 'dev' into goal/dependency 2023-10-27 15:33:47 -07:00
Leni Aniva 3b1746490d feat: Add REPL command for assigning an expression 2023-10-27 15:32:59 -07:00
Leni Aniva f064bb21a4 feat: Assigning a goal with an expression 2023-10-27 15:15:22 -07:00
Leni Aniva 269e5c707c refactor: Separate goal printing and processing 
Added a test for delta proof variables
 2023-10-26 22:47:42 -07:00
Leni Aniva c852db2f46 test: m-coupled goals 2023-10-26 11:22:02 -07:00
Leni Aniva 8029298db7 feat: Display user name in Goal structure 
1. Modify `serialize_expression_ast` so its no longer a monad
2. Test existence of root expression
 2023-10-25 22:18:59 -07:00
Leni Aniva d991533170 feat: Add proof continue and root extraction 2023-10-25 16:03:45 -07:00
Leni Aniva a9294e0338 Add documentation about flake 2023-10-20 12:54:35 -07:00
Leni Aniva 3d7d5d6b4d feat: Add nix flake 2023-10-20 12:41:56 -07:00
Leni Aniva 538ba6e7d7 Store states instead of goals 
1. Rename {Commands, Protocol}, and {Symbols, Symbol}
2. Store the root mvarId in the proof state along with goal indices
3. Add diagnostics function which prints out the state
4. Bump version to 0.2.6 (breaking change)

Documentations pending
 2023-10-15 17:15:23 -07:00
Leni Aniva 41db295ff5 Rename tactic to goal and restructure 2023-10-15 12:31:22 -07:00
Leni Aniva 7a5fe554ba Add holes test stub 
Move tests into their own namespaces
 2023-10-06 17:31:36 -07:00
Leni Aniva 13f3460e9a Fix test failures 2023-10-05 17:51:41 -07:00
Leni Aniva a8cf94ccb1 Bump Lean version to 4.1.0 2023-10-05 17:49:43 -07:00
Leni Aniva 0948e71d60 Add dependency for lakefile and lean-toolchain 2023-10-02 10:30:58 -07:00
Leni Aniva 6d15d1e670 Use makefile instead of ad-hoc script 2023-10-02 10:26:19 -07:00
Leni Aniva 35b391881e Add ready message to indicate the main loop is up 2023-10-02 10:14:03 -07:00
Leni Aniva d7077ce854 Bump lean version to 4.0.0 2023-09-13 21:02:26 -07:00
Leni Aniva 75f43786fb Merge pull request 'Simplify goal bookkeeping mechanism' (#10) from tactic/book into dev 
Reviewed-on: #10
 2023-08-30 19:18:36 -07:00
Leni Aniva f538f580bd Merge branch 'dev' into tactic/book 2023-08-30 19:17:25 -07:00
Leni Aniva f1f1c20ff9 Add SemihashMap interface, rename proof commands to goal commands, allow deletion 2023-08-30 19:16:33 -07:00
Leni Aniva 6b96f7893f Separate max and imax in sort level 2023-08-27 22:50:18 -07:00
Leni Aniva b98304f78a Version bump to 0.2.4 due to breaking change 2023-08-27 19:59:31 -07:00
Leni Aniva a6e337a89e Rename proof commands to goal commands 2023-08-27 19:58:52 -07:00
Leni Aniva a86af1bc57 Add SemihashMap structure for goal bookkeeping 2023-08-27 19:53:09 -07:00
Leni Aniva b74119e378 Merge pull request 'Remove the obsolete name field from proof tree structure' (#11) from misc/cleanup into dev 
Reviewed-on: #11
 2023-08-26 18:50:40 -07:00
Leni Aniva 9c4c43a9f1 Remove the obsolete name field from proof tree structure 2023-08-26 18:50:15 -07:00
Leni Aniva bd4fbcc369 Add test cases for command error categories 2023-08-24 23:12:18 -07:00
Leni Aniva ff8fed8741 Classify JSON error as command error 
Also add documentation for this
 2023-08-24 22:51:40 -07:00
Leni Aniva 98edaa3297 Merge pull request 'Add more serialisation options' (#2) from io/serial into dev 
Reviewed-on: #2
 2023-08-23 13:29:00 -07:00
Leni Aniva 1f27532769 Merge branch 'dev' into io/serial 2023-08-23 13:25:08 -07:00
Leni Aniva 0c330c8778 Unify json and unknown error into command error 2023-08-23 13:00:11 -07:00
Leni Aniva 59c046efc6 Add proper printing of sorts 2023-08-23 12:51:06 -07:00
Leni Aniva a8cbb3be4f Move all json-string functions to Main.lean 2023-08-22 09:54:37 -07:00
Leni Aniva 96cbbf2551 Add compressed json print option; Rearrange commands into hierarchy 2023-08-16 19:25:32 -07:00
Leni Aniva b2ba26528d Add proof variable delta; Bump version to 0.2.1 2023-08-15 15:40:54 -07:00
Leni Aniva 7771408de1 Add expression sexp printing (2/2) 2023-08-14 21:43:40 -07:00
Leni Aniva 9eadd1d4d4 Add expression sexp printing (1/2, tests pending) 2023-08-14 17:07:53 -07:00
Leni Aniva 5cedb9d88c version bump, restructure 2023-08-13 21:19:06 -07:00
Leni Aniva 622aa7f969 Add documentation; Remove mathlib dependency 2023-06-09 14:45:45 -07:00
Leni Aniva 4613777607 Add json goal printing 2023-05-27 23:10:39 -07:00
Leni Aniva 3e05722d1e Add back the clear command to reset state 2023-05-26 16:55:33 -07:00
Leni Aniva 068a188fea Add expr.type 2023-05-25 13:40:03 -07:00