 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 |
|
Leni Aniva
|
e0c5f76451
|
Rename tactic failure mode to avoid confusion
Clean up README
|
2023-05-24 23:11:17 -07:00 |
|
Leni Aniva
|
da1cdf3d16
|
Update gitignore to exclude hidden files
|
2023-05-24 09:32:19 -07:00 |
|
Leni Aniva
|
1ed1aff7c9
|
Add documentation about options
|
2023-05-24 00:55:54 -07:00 |
|
Leni Aniva
|
95ed7d115c
|
Add expression binding printing and import Lean
|
2023-05-24 00:54:48 -07:00 |
|
Leni Aniva
|
1fed222f56
|
Use TermElabM as the main monad stack instead of IO
|
2023-05-23 05:12:46 -07:00 |
|
Leni Aniva
|
94bc3355a2
|
Save core state in proofs
|
2023-05-22 22:48:48 -07:00 |
|
Leni Aniva
|
ba779766c0
|
Rename ids so they are consistent
|
2023-05-22 19:51:16 -07:00 |
|
Leni Aniva
|
1ad45f650f
|
Remove testing stub in README.md
|
2023-05-22 19:12:07 -07:00 |
|
Leni Aniva
|
0f8df08dd5
|
Add module name for symbol
|
2023-05-22 16:00:41 -07:00 |
|
Leni Aniva
|
116c7ff4c6
|
Add option id handling with ?
|
2023-05-22 14:56:43 -07:00 |
|
Leni Aniva
|
6a71dad389
|
Add option format for proof output and test cases
|
2023-05-22 14:49:56 -07:00 |
|
Leni Aniva
|
1bf929b1e4
|
Add testing stub
|
2023-05-22 11:47:46 -07:00 |
|
Leni Aniva
|
46ccad1669
|
Add default arguments for Json
|
2023-05-22 00:49:37 -07:00 |
|
Leni Aniva
|
76d76630ee
|
Add manifest file
|
2023-05-21 23:30:41 -07:00 |
|
Leni Aniva
|
083ec8beec
|
Add REPL tactics
|
2023-05-21 17:41:39 -07:00 |
|
Leni Aniva
|
15aab3d31f
|
Remove ExceptT from main monad
Allow pretty printing of expr
|
2023-05-20 15:58:38 -07:00 |
|
Leni Aniva
|
2a4d348aab
|
Add expression IO stub for constant types
|
2023-05-20 14:04:09 -07:00 |
|
Leni Aniva
|
8127e9ba06
|
Add alternative command input format and IO stub
|
2023-05-20 13:03:12 -07:00 |
|
Leni Aniva
|
e246fd961f
|
Add tactic state manipulation
|
2023-05-17 21:58:03 -07:00 |