Compare commits

...

183 Commits

Author SHA1 Message Date
Leni Aniva 431bdab236
doc: Reason why not to follow nixpkgs 2024-03-30 00:03:37 -07:00
Leni Aniva a4a1dfabef
Merge branch 'dev' into misc/toolchain 2024-03-30 00:01:24 -07:00
Leni Aniva 08874d433f
fix: Update flake so lean builds on Darwin 2024-03-29 23:59:14 -07:00
Leni Aniva 5c970bfeed
fix: Lean build failure on macOS 2024-03-29 23:50:30 -07:00
Leni Aniva c701210f53 Merge pull request 'feat: Query arbitrary assignment in goal' (#47) from goal/relation into dev
Reviewed-on: #47
2024-03-29 23:48:20 -07:00
Leni Aniva 113e65e193
Merge branch 'dev' into goal/relation 2024-03-29 23:47:09 -07:00
Leni Aniva aeed233846 Merge pull request 'chore: Version bump and toolchain cleanup' (#51) from misc/toolchain into dev
Reviewed-on: #51
2024-03-28 22:36:25 -07:00
Leni Aniva 3e1a14222c
Merge branch 'dev' into misc/toolchain 2024-03-28 22:35:48 -07:00
Leni Aniva 0ade3d1637 Merge pull request 'feat: Remove display of implementation details' (#50) from io/serial into dev
Reviewed-on: #50
2024-03-28 22:35:37 -07:00
Leni Aniva bdb060b79f
build: Dev shell 2024-03-28 22:26:46 -07:00
Leni Aniva c5404b8210
build: Ignore test files when building target 2024-03-28 22:23:19 -07:00
Leni Aniva 1d1a151a4b
doc: Main README.md 2024-03-28 22:12:11 -07:00
Leni Aniva d853cb8cc2
chore: Version bump 2024-03-28 22:08:22 -07:00
Leni Aniva 78a3b240ba
test: Catalog has no numeric symbols 2024-03-28 20:44:09 -07:00
Leni Aniva 35c4ea693d
feat: Stop cataloging internal/detail dependencies 2024-03-28 19:49:44 -07:00
Leni Aniva d9af064888
test: Elimination of aux lemmas 2024-03-28 19:27:45 -07:00
Leni Aniva 01a23b338a
feat: Unfold aux lemmas when printing root expr 2024-03-28 18:56:42 -07:00
Leni Aniva 91e55245fa
doc: Update README.md 2024-03-28 11:37:07 -07:00
Leni Aniva 22fdb7bea9
build: Nix build targets and checks 2024-03-28 11:33:15 -07:00
Leni Aniva 60903bf31f
feat: Bump toolchain version 2024-03-28 00:06:35 -07:00
Leni Aniva a3a244159b
chore: Version bump to 0.2.13 2024-03-16 19:00:28 -07:00
Leni Aniva bb09d1e964
chore: Version bump to 4.8.0 prerelease 2024-03-15 18:44:28 -07:00
Leni Aniva b7542b4749
chore: Lean version bump to 4.7.0-rc2
Multithreading in ABI was not stabilized in 4.1.0
2024-03-15 06:01:25 -07:00
Leni Aniva 689112d973
fix: Use Arrays only in the ABI 2024-03-14 22:40:14 -07:00
Leni Aniva b64adf31cf
feat(lib): Export goal.print function 2024-03-14 16:34:01 -07:00
Leni Aniva c83af044b4
fix: Pass options by reference 2024-03-11 21:31:59 -07:00
Leni Aniva 285cf0416a
feat(lib): Option creation function 2024-03-10 15:33:32 -07:00
Leni Aniva 5db727e30b
fix: Execute expr parsing within goal.start 2024-03-10 15:09:38 -07:00
Leni Aniva f42a27e036
feat(lib): Expose goal state interface 2024-03-10 08:13:10 -07:00
Leni Aniva d958dbed9d
feat(lib): CoreM execution function 2024-03-10 06:41:35 -07:00
Leni Aniva ca89d671cc
refactor: Move some functions to `Library.lean` 2024-03-09 20:37:48 -08:00
Leni Aniva 4706df2217
feat(lib): Search path function 2024-03-09 19:36:25 -08:00
Leni Aniva 863c6d9e7d
feat(lib): Catalog command FFI 2024-03-09 16:50:36 -08:00
Leni Aniva 021d0b5b7d
feat: Add exported version function 2024-03-08 23:50:44 -08:00
Leni Aniva ecacf2107c
feat(build): Add shared facet for lean_lib 2024-03-06 15:27:22 -08:00
Leni Aniva 075bec6da2
feat: Output shared library in flake 2024-03-06 15:26:35 -08:00
Leni Aniva 8853b17fee
test: More diagnostics for tests 2024-03-06 15:14:08 -08:00
Leni Aniva 3292b34070 Merge pull request 'feat: Print parent expression assignment' (#45) from goal/relation into dev
Reviewed-on: #45
2024-02-15 14:55:02 -08:00
Leni Aniva d57612ec71
test: Delayed metavariable assignment 2024-02-15 14:47:09 -08:00
Leni Aniva 9ac84b3fd1
Merge branch 'dev' into goal/relation 2024-02-15 14:39:30 -08:00
Leni Aniva a748900ad6 Merge pull request 'feat: Add leanpkgs to the flake output' (#46) from nix/toolchain into dev
Reviewed-on: #46
2024-02-15 14:30:30 -08:00
Leni Aniva 3e321516f7
chore: Expose `leanPkgs` in flake 2024-02-13 15:30:56 -05:00
Leni Aniva 8b67e7006a
feat: Add lake and lean to the package output 2024-02-05 11:50:22 -08:00
Leni Aniva 4a98b90289
chore: Version bump to 0.2.12-alpha 2024-01-30 17:45:32 -08:00
Leni Aniva 5720c72515
feat: Prevent crash during rootExpr call 2024-01-30 17:22:20 -08:00
Leni Aniva 6d22841a27
doc: Correct comment about parent filling expr 2024-01-30 16:37:35 -08:00
Leni Aniva 9a5ee49778
feat: Print parent expression assignment 2024-01-24 18:19:04 -08:00
Leni Aniva a811decf84 Merge pull request 'test: Option controlled mvar instantiation' (#44) from goal/diag into dev
Reviewed-on: #44
2024-01-17 22:27:44 -08:00
Leni Aniva 79b6974172
Merge branch 'dev' into goal/diag 2024-01-17 14:03:19 -08:00
Leni Aniva 42c3da4a67 Merge pull request 'feat: Print inductives, constructors, and recursors in env.inspect' (#43) from env/inspect into dev
Reviewed-on: #43
2024-01-17 14:02:55 -08:00
Leni Aniva efa956464d
test: Option controlled mvar instantiation 2024-01-16 16:44:54 -08:00
Leni Aniva 93a34f9fda
feat: Print constructor and recursor info 2024-01-16 14:11:52 -08:00
Leni Aniva a1421439f8
feat: Print inductives in env.inspect 2024-01-16 13:29:30 -08:00
Leni Aniva b29f7cb180
test: Simplify monad execution 2024-01-07 14:14:20 -08:00
Leni Aniva 6e39b5ef8b Merge pull request 'feat: Add definitions and theorems to the environment' (#41) from env/add-decl into dev
Reviewed-on: #41
2023-12-26 12:41:01 -08:00
Leni Aniva 77232d5a1e
refactor: Rename Test/{Catalog,Environment} 2023-12-26 12:22:57 -05:00
Leni Aniva 22789436bd
chore: Move environment functions to its own file
Symbol.lean is now subsumed
2023-12-15 13:40:36 -05:00
Leni Aniva aca7dc9811
refactor: env. operations into its own file 2023-12-15 13:37:55 -05:00
Leni Aniva 3b83c81540
fix: Force instantiate all mvars in env.add 2023-12-15 13:07:59 -05:00
Leni Aniva 6c25cca46a
test: env.add 2023-12-14 11:11:24 -08:00
Leni Aniva 2f3a91562a
fix: env_add monads 2023-12-14 05:52:12 -08:00
Leni Aniva 09f5792d4a
Merge branch 'dev' into env/add-decl 2023-12-14 05:48:49 -08:00
Leni Aniva 4076d8a7dd Merge pull request 'feat: Change the main interaction monad' (#40) from core/loop into dev
Reviewed-on: #40
2023-12-14 05:46:39 -08:00
Leni Aniva 02889510b2
feat: env_add command 2023-12-13 19:35:32 -08:00
Leni Aniva 12544b81ee
chore: Rename lib. commands to env.
This is done to improve clarity and align with Lean's terminology
2023-12-12 18:56:25 -08:00
Leni Aniva ab1b309c72
feat: Use CoreM as the main interaction monad 2023-12-12 18:39:02 -08:00
Leni Aniva 45beca0bc4
doc: TermElabM metavariable generation 2023-12-08 17:32:30 -08:00
Leni Aniva 1fb189a38f
fix: Consolidate TermElabM blocks 2023-12-08 17:31:25 -08:00
Leni Aniva c76751861a
fix: Change the main interaction monad to MetaM 2023-12-08 16:17:16 -08:00
Leni Aniva de2688ccfa
chore: Version downgrade to 0.2.10-alpha
There is a currently known bug
2023-12-07 12:38:02 -08:00
Leni Aniva 4871133027 Merge pull request 'fix: Printing projection leads to crash' (#37) from io/sexp into dev
Reviewed-on: #37
2023-12-07 12:33:01 -08:00
Leni Aniva 2dc7657e2a
doc: getUsedConstants bug about projections 2023-12-06 15:05:04 -08:00
Leni Aniva ccf5a03647
fix: Printing projection leads to crash 2023-12-05 22:45:59 -08:00
Leni Aniva 56966b27cf Merge pull request 'feat: Handling of private names' (#36) from library/catalog into dev
Reviewed-on: #36
2023-12-05 20:22:38 -08:00
Leni Aniva 9276d47e0d
Merge branch 'dev' into library/catalog 2023-12-05 20:21:22 -08:00
Leni Aniva cf856d2880
chore: Version bump 2023-12-05 20:21:07 -08:00
Leni Aniva beb837ccab Merge pull request 'feat: Print structural projection as application' (#35) from io/serial into dev
Reviewed-on: #35
2023-12-05 20:20:51 -08:00
Leni Aniva da74258dd1
feat!: Display public name only if name is private 2023-12-05 20:20:08 -08:00
Leni Aniva 9f2b07757f
feat: Display whether a symbol is private 2023-12-05 19:07:00 -08:00
Leni Aniva 07ade4c822
feat: Expose _private names 2023-12-04 23:36:09 -08:00
Leni Aniva a454aaf1d4
feat: Remove stem deduce
Some private subproofs are not shown in the catalog and this breaks
dependencies
2023-12-04 16:40:15 -08:00
Leni Aniva ec09304e02
feat: Remove printing projections 2023-12-04 16:21:02 -08:00
Leni Aniva 967e3dfb4f
feat: Remove | in symbol output 2023-11-27 09:54:41 -08:00
Leni Aniva 0a5a96275f
chore: Version bump to 0.2.9 2023-11-26 23:48:47 -08:00
Leni Aniva 7690272bfa
feat: Shorter symbol category 2023-11-26 22:14:58 -08:00
Leni Aniva 7b59937853
feat: Read dependencies of library symbols 2023-11-25 15:07:56 -08:00
Leni Aniva 2a9931c134
fix: Rectify error format 2023-11-09 22:24:17 -08:00
Leni Aniva c99125c4a6 Merge pull request 'feat: Allow selective continuation of goals' (#27) from goal/continuation into dev
Reviewed-on: #27
2023-11-07 16:49:55 -08:00
Leni Aniva 8218d3f004
fix: Do not show parent state in continue 2023-11-07 13:10:14 -08:00
Leni Aniva 736e68639f
fix: New goal state not inserted correctly 2023-11-07 13:07:50 -08:00
Leni Aniva cfd1cfd107
Merge branch 'dev' into goal/continuation 2023-11-07 12:11:14 -08:00
Leni Aniva 764be6d14b
fix: Remove the error prone SemihashMap 2023-11-07 12:09:54 -08:00
Leni Aniva 5ac5198f51
fix: Remove the error prone SemihashMap 2023-11-07 12:04:17 -08:00
Leni Aniva 7076669c3d
chore: Code formatting 2023-11-06 12:20:08 -08:00
Leni Aniva 245e76b2f1
feat: Print the root mvar name 2023-11-06 11:51:31 -08:00
Leni Aniva 7c28cf4ed0
Merge branch 'dev' into goal/continuation 2023-11-06 11:45:24 -08:00
Leni Aniva c5f563598d
chore: Remove unnecessary unsafe's 2023-11-06 11:43:57 -08:00
Leni Aniva a7aeb03b43
chore: Update documentation 2023-11-06 11:04:28 -08:00
Leni Aniva dbace9f2d5
fix: Use Lean's built in name parser
The `str_to_name` parser cannot handle numerical names and escapes.
2023-11-06 10:45:11 -08:00
Leni Aniva 782ce38c87
chore: Version bump to 0.2.8 2023-11-04 15:54:28 -07:00
Leni Aniva d809a960f9
feat: Goal continuation fails if target has goals 2023-11-04 15:53:57 -07:00
Leni Aniva db706070ad
feat: Add goal.continue command 2023-11-04 15:51:09 -07:00
Leni Aniva 754fb69cff
feat: Partial state continuation 2023-11-04 15:33:53 -07:00
Leni Aniva dc2cc5be77
test: Separate mvar coupling tests 2023-11-04 15:01:41 -07:00
Leni Aniva f5ed87f740 Merge pull request 'feat: Minor updates to serialization' (#26) from io/serial into dev
Reviewed-on: #26
2023-10-30 14:47:41 -07:00
Leni Aniva 8dd994d1ca
bug: Fix quote escape problem 2023-10-30 14:45:43 -07:00
Leni Aniva d87217c6bb
feat: Print metavariable name in goal 2023-10-30 14:44:06 -07:00
Leni Aniva 796f0d8336 Merge pull request 'feat: Simplify printing of names and expressions' (#25) from io/serial into dev
Reviewed-on: #25
2023-10-29 13:08:05 -07:00
Leni Aniva e5acd4b26c
fix: Sanitize name in universe levels 2023-10-29 13:03:48 -07:00
Leni Aniva 454a5bc6b9
feat: Simplify printing of function applications 2023-10-29 12:50:36 -07:00
Leni Aniva afed5bbc8d
chore: Version bump (breaking change) 2023-10-29 11:57:24 -07:00
Leni Aniva e2526f11b1
feat: Print names in one segment separated with . 2023-10-29 11:56:56 -07:00
Leni Aniva c2d606b9d9
feat: Simplify name printing 2023-10-29 11:18:35 -07:00
Leni Aniva c19fd1bcfb 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 427d819349
feat: Add REPL function for root expression 2023-10-27 15:41:12 -07:00
Leni Aniva ca7a081cac
Merge branch 'dev' into goal/dependency 2023-10-27 15:33:47 -07:00
Leni Aniva 82f5494718
feat: Add REPL command for assigning an expression 2023-10-27 15:32:59 -07:00
Leni Aniva b381d89ff9
feat: Assigning a goal with an expression 2023-10-27 15:15:22 -07:00
Leni Aniva e98fb77f33
refactor: Separate goal printing and processing
Added a test for delta proof variables
2023-10-26 22:47:42 -07:00
Leni Aniva 4ffd226cac
test: m-coupled goals 2023-10-26 11:22:02 -07:00
Leni Aniva 0ecfa9fc26
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 0a0f0304a8
feat: Add proof continue and root extraction 2023-10-25 16:03:45 -07:00
Leni Aniva 7dc6e4e549
Add documentation about flake 2023-10-20 12:54:35 -07:00
Leni Aniva ba53e9087b
feat: Add nix flake 2023-10-20 12:41:56 -07:00
Leni Aniva 9447d29e37
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 8c93d30ab7
Rename tactic to goal and restructure 2023-10-15 12:31:22 -07:00
Leni Aniva 42133f9b74
Add holes test stub
Move tests into their own namespaces
2023-10-06 17:31:36 -07:00
Leni Aniva 5b002a9ceb
Fix test failures 2023-10-05 17:51:41 -07:00
Leni Aniva 836a14fa63
Bump Lean version to 4.1.0 2023-10-05 17:49:43 -07:00
Leni Aniva 5f2b394471
Add dependency for lakefile and lean-toolchain 2023-10-02 10:30:58 -07:00
Leni Aniva 2c3a7adb61
Use makefile instead of ad-hoc script 2023-10-02 10:26:19 -07:00
Leni Aniva 8e02e6e7cc Add ready message to indicate the main loop is up 2023-10-02 10:14:03 -07:00
Leni Aniva 1e637dabaa
Bump lean version to 4.0.0 2023-09-13 21:02:26 -07:00
Leni Aniva c4a97d8a76 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 acfd4e8288
Merge branch 'dev' into tactic/book 2023-08-30 19:17:25 -07:00
Leni Aniva 46347d8244
Add SemihashMap interface, rename proof commands to goal commands, allow deletion 2023-08-30 19:16:33 -07:00
Leni Aniva 71327d2d55
Separate max and imax in sort level 2023-08-27 22:50:18 -07:00
Leni Aniva 8d5d7b6e3e
Version bump to 0.2.4 due to breaking change 2023-08-27 19:59:31 -07:00
Leni Aniva 80ad7a2bd0
Rename proof commands to goal commands 2023-08-27 19:58:52 -07:00
Leni Aniva 0c5f439067
Add SemihashMap structure for goal bookkeeping 2023-08-27 19:53:09 -07:00
Leni Aniva dea63ac5ea 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 81702d12ef Remove the obsolete name field from proof tree structure 2023-08-26 18:50:15 -07:00
Leni Aniva 51edc701fe
Add test cases for command error categories 2023-08-24 23:12:18 -07:00
Leni Aniva 95d26a2f50
Classify JSON error as command error
Also add documentation for this
2023-08-24 22:51:40 -07:00
Leni Aniva 5978e5f4f3 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 7160f8aa61
Merge branch 'dev' into io/serial 2023-08-23 13:25:08 -07:00
Leni Aniva 85440e0278
Unify json and unknown error into command error 2023-08-23 13:00:11 -07:00
Leni Aniva e63f7c9afa
Add proper printing of sorts 2023-08-23 12:51:06 -07:00
Leni Aniva 1d1fa60175
Move all json-string functions to Main.lean 2023-08-22 09:54:37 -07:00
Leni Aniva ddf7ec21c8 Add compressed json print option; Rearrange commands into hierarchy 2023-08-16 19:25:32 -07:00
Leni Aniva 0e61093f47 Add proof variable delta; Bump version to 0.2.1 2023-08-15 15:40:54 -07:00
Leni Aniva d476354a4a Add expression sexp printing (2/2) 2023-08-14 21:43:40 -07:00
Leni Aniva 19c57ada1e Add expression sexp printing (1/2, tests pending) 2023-08-14 17:07:53 -07:00
Leni Aniva d705cdf0e5 version bump, restructure 2023-08-13 21:19:06 -07:00
Leni Aniva a00a2b4a42 Add documentation; Remove mathlib dependency 2023-06-09 14:45:45 -07:00
Leni Aniva 572548c1bd Add json goal printing 2023-05-27 23:10:39 -07:00
Leni Aniva 9fe3f62371 Add back the clear command to reset state 2023-05-26 16:55:33 -07:00
Leni Aniva 989130ecd2 Add expr.type 2023-05-25 13:40:03 -07:00
Leni Aniva 5beb911db5 Rename tactic failure mode to avoid confusion
Clean up README
2023-05-24 23:11:17 -07:00
Leni Aniva 9b8aff95e5 Update gitignore to exclude hidden files 2023-05-24 09:32:19 -07:00
Leni Aniva 4033722596 Add documentation about options 2023-05-24 00:55:54 -07:00
Leni Aniva fd536da55c Add expression binding printing and import Lean 2023-05-24 00:54:48 -07:00
Leni Aniva 58367cef6c Use TermElabM as the main monad stack instead of IO 2023-05-23 05:12:46 -07:00
Leni Aniva c781797898 Save core state in proofs 2023-05-22 22:48:48 -07:00
Leni Aniva 44d470d63e Rename ids so they are consistent 2023-05-22 19:51:16 -07:00
Leni Aniva 51477a4806 Remove testing stub in README.md 2023-05-22 19:12:07 -07:00
Leni Aniva 56b967ee7a Add module name for symbol 2023-05-22 16:00:41 -07:00
Leni Aniva 22202af24e Add option id handling with ? 2023-05-22 14:56:43 -07:00
Leni Aniva 111dea2093 Add option format for proof output and test cases 2023-05-22 14:49:56 -07:00
Leni Aniva 8a448fb114 Add testing stub 2023-05-22 11:47:46 -07:00
Leni Aniva 2772a394cc Add default arguments for Json 2023-05-22 00:49:37 -07:00
Leni Aniva 147079816d Add manifest file 2023-05-21 23:30:41 -07:00
Leni Aniva 41241bfa40 Add REPL tactics 2023-05-21 17:41:39 -07:00
Leni Aniva ed70875837 Remove ExceptT from main monad
Allow pretty printing of expr
2023-05-20 15:58:38 -07:00
Leni Aniva c4a1ccad13 Add expression IO stub for constant types 2023-05-20 14:04:09 -07:00
Leni Aniva 65da39440d Add alternative command input format and IO stub 2023-05-20 13:03:12 -07:00
Leni Ven 14a6eb1f59 Add tactic state manipulation 2023-05-17 21:58:03 -07:00
Leni Ven 2ec4efde55 Add stack size troubleshooting 2023-05-14 15:22:41 -07:00
Leni Ven 3cb0795bb6 Add unsafe filtering in catalog 2023-05-12 16:12:21 -07:00
Leni Aniva 9f53781ffe Add working catalog code and example 2023-05-12 01:08:36 -07:00
Leni Ven 5a297e8fef Add README and catalog functions 2023-05-09 22:51:19 -07:00
Leni Aniva 0b2db92b4a Separate commands into its own file 2023-05-09 18:01:09 -07:00
Leni Ven 9a957bce35 Add REPL 2023-05-09 16:39:24 -07:00
24 changed files with 2980 additions and 12 deletions

4
.gitignore vendored
View File

@ -1,2 +1,6 @@
.*
!.gitignore
*.olean
/build /build
/lake-packages /lake-packages

View File

@ -1,4 +1,66 @@
import Lean.Data.Json
import Lean.Environment
import Pantograph.Version
import Pantograph.Library
import Pantograph import Pantograph
def main : IO Unit := -- Main IO functions
IO.println s!"Hello, {hello}!" open Pantograph
/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
def parseCommand (s: String): Except String Protocol.Command := do
let s := s.trim
match s.get? 0 with
| .some '{' => -- Parse in Json mode
Lean.fromJson? (← Lean.Json.parse s)
| .some _ => -- Parse in line mode
let offset := s.posOf ' ' |> s.offsetOfPos
if offset = s.length then
return { cmd := s.take offset, payload := Lean.Json.null }
else
let payload ← s.drop offset |> Lean.Json.parse
return { cmd := s.take offset, payload := payload }
| .none => throw "Command is empty"
partial def loop : MainM Unit := do
let state ← get
let command ← (← IO.getStdin).getLine
if command.trim.length = 0 then return ()
match parseCommand command with
| .error error =>
let error := Lean.toJson ({ error := "command", desc := error }: Protocol.InteractionError)
-- Using `Lean.Json.compress` here to prevent newline
IO.println error.compress
| .ok command =>
let ret ← execute command
let str := match state.options.printJsonPretty with
| true => ret.pretty
| false => ret.compress
IO.println str
loop
unsafe def main (args: List String): IO Unit := do
-- NOTE: A more sophisticated scheme of command line argument handling is needed.
-- Separate imports and options
if args == ["--version"] then do
println! s!"{version}"
return
initSearch ""
let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
|>.toArray |> createCoreContext
let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
let coreState ← createCoreState imports.toArray
let context: Context := {
imports
}
try
let coreM := loop.run context |>.run' {}
IO.println "ready."
discard <| coreM.toIO coreContext coreState
catch ex =>
IO.println "Uncaught IO exception"
IO.println ex.toString

20
Makefile Normal file
View File

@ -0,0 +1,20 @@
LIB := ./.lake/build/lib/Pantograph.olean
EXE := ./.lake/build/bin/pantograph
SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain
TEST_EXE := ./.lake/build/bin/test
TEST_SOURCE := $(wildcard Test/*.lean)
$(LIB) $(EXE): $(SOURCE)
lake build pantograph
$(TEST_EXE): $(LIB) $(TEST_SOURCE)
lake build test
test: $(TEST_EXE)
$(TEST_EXE)
clean:
lake clean
.PHONY: test clean

View File

@ -1 +1,184 @@
def hello := "world" import Pantograph.Goal
import Pantograph.Protocol
import Pantograph.Serial
import Pantograph.Environment
import Pantograph.Library
import Lean.Data.HashMap
namespace Pantograph
structure Context where
imports: List String
/-- Stores state of the REPL -/
structure State where
options: Protocol.Options := {}
nextId: Nat := 0
goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
/-- Main state monad for executing commands -/
abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
-- certain monadic features in `MainM`
abbrev CR α := Except Protocol.InteractionError α
def execute (command: Protocol.Command): MainM Lean.Json := do
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
match Lean.fromJson? command.payload with
| .ok args => do
match (← comm args) with
| .ok result => return Lean.toJson result
| .error ierror => return Lean.toJson ierror
| .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
match command.cmd with
| "reset" => run reset
| "stat" => run stat
| "expr.echo" => run expr_echo
| "env.catalog" => run env_catalog
| "env.inspect" => run env_inspect
| "env.add" => run env_add
| "options.set" => run options_set
| "options.print" => run options_print
| "goal.start" => run goal_start
| "goal.tactic" => run goal_tactic
| "goal.continue" => run goal_continue
| "goal.delete" => run goal_delete
| "goal.print" => run goal_print
| cmd =>
let error: Protocol.InteractionError :=
errorCommand s!"Unknown command {cmd}"
return Lean.toJson error
where
errorCommand := errorI "command"
errorIndex := errorI "index"
-- Command Functions
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
let state ← get
let nGoals := state.goalStates.size
set { state with nextId := 0, goalStates := Lean.HashMap.empty }
return .ok { nGoals }
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
let state ← get
let nGoals := state.goalStates.size
return .ok { nGoals }
env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
let result ← Environment.catalog args
return .ok result
env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
let state ← get
Environment.inspect args state.options
env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
Environment.addDecl args
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
let state ← get
exprEcho args.expr state.options
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
let state ← get
let options := state.options
set { state with
options := {
-- FIXME: This should be replaced with something more elegant
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
printExprPretty := args.printExprPretty?.getD options.printExprPretty,
printExprAST := args.printExprAST?.getD options.printExprAST,
noRepeat := args.noRepeat?.getD options.noRepeat,
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
}
}
return .ok { }
options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.OptionsPrintResult) := do
return .ok (← get).options
goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
let state ← get
let env ← Lean.MonadEnv.getEnv
let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
| .some expr, .none => do
let expr ← match ← exprParse expr with
| .error e => return .error e
| .ok expr => pure $ expr
return .ok $ ← GoalState.create expr
| .none, .some copyFrom =>
(match env.find? <| copyFrom.toName with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
| .some cInfo => return .ok (← GoalState.create cInfo.type))
| _, _ =>
return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
match expr? with
| .error error => return .error error
| .ok goalState =>
let stateId := state.nextId
set { state with
goalStates := state.goalStates.insert stateId goalState,
nextId := state.nextId + 1
}
return .ok { stateId, root := goalState.root.name.toString }
goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
let state ← get
match state.goalStates.find? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => do
let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
| .some tactic, .none => do
pure ( Except.ok (← goalTactic goalState args.goalId tactic))
| .none, .some expr => do
pure ( Except.ok (← goalTryAssign goalState args.goalId expr))
| _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
match nextGoalState? with
| .error error => return .error error
| .ok (.success nextGoalState) =>
let nextStateId := state.nextId
set { state with
goalStates := state.goalStates.insert state.nextId nextGoalState,
nextId := state.nextId + 1,
}
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
return .ok {
nextStateId? := .some nextStateId,
goals? := .some goals,
}
| .ok (.parseError message) =>
return .ok { parseError? := .some message }
| .ok (.indexError goalId) =>
return .error $ errorIndex s!"Invalid goal id index {goalId}"
| .ok (.failure messages) =>
return .ok { tacticErrors? := .some messages }
goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
let state ← get
match state.goalStates.find? args.target with
| .none => return .error $ errorIndex s!"Invalid state index {args.target}"
| .some target => do
let nextState? ← match args.branch?, args.goals? with
| .some branchId, .none => do
match state.goalStates.find? branchId with
| .none => return .error $ errorIndex s!"Invalid state index {branchId}"
| .some branch => pure $ target.continue branch
| .none, .some goals =>
pure $ goalResume target goals
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
match nextState? with
| .error error => return .error <| errorI "structure" error
| .ok nextGoalState =>
let nextStateId := state.nextId
set { state with
goalStates := state.goalStates.insert nextStateId nextGoalState,
nextId := state.nextId + 1
}
let goals ← goalSerialize nextGoalState (options := state.options)
return .ok {
nextStateId,
goals,
}
goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
let state ← get
let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates
set { state with goalStates }
return .ok {}
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
let state ← get
match state.goalStates.find? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => runMetaM <| do
return .ok (← goalPrint goalState state.options)
end Pantograph

137
Pantograph/Environment.lean Normal file
View File

@ -0,0 +1,137 @@
import Pantograph.Protocol
import Pantograph.Serial
import Lean
open Lean
open Pantograph
namespace Pantograph.Environment
def isNameInternal (n: Lean.Name): Bool :=
-- Returns true if the name is an implementation detail which should not be shown to the user.
isLeanSymbol n (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) n.isAuxLemma n.hasMacroScopes
where
isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
| .str _ name => name == "Lean"
| _ => true
def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String :=
let pref := match info with
| .axiomInfo _ => "a"
| .defnInfo _ => "d"
| .thmInfo _ => "t"
| .opaqueInfo _ => "o"
| .quotInfo _ => "q"
| .inductInfo _ => "i"
| .ctorInfo _ => "c"
| .recInfo _ => "r"
s!"{pref}{toString n}"
def toFilteredSymbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
if isNameInternal n || info.isUnsafe
then Option.none
else Option.some <| toCompactSymbolName n info
def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
let env ← Lean.MonadEnv.getEnv
let names := env.constants.fold (init := #[]) (λ acc name info =>
match toFilteredSymbol name info with
| .some x => acc.push x
| .none => acc)
return { symbols := names }
def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
let env ← Lean.MonadEnv.getEnv
let name := args.name.toName
let info? := env.find? name
let info ← match info? with
| none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
| some info => pure info
let module? := env.getModuleIdxFor? name >>=
(λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
let value? := match args.value?, info with
| .some true, _ => info.value?
| .some false, _ => .none
| .none, .defnInfo _ => info.value?
| .none, _ => .none
-- Information common to all symbols
let core := {
type := ← (serialize_expression options info.type).run',
isUnsafe := info.isUnsafe,
value? := ← value?.mapM (λ v => serialize_expression options v |>.run'),
publicName? := Lean.privateToUserName? name |>.map (·.toString),
-- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
typeDependency? := if args.dependency?.getD false
then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n)
else .none,
valueDependency? := ← if args.dependency?.getD false
then info.value?.mapM (λ e => do
let e ← (unfoldAuxLemmas e).run'
pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => name_to_ast n) )
else pure (.none),
module? := module?
}
let result := match info with
| .inductInfo induct => { core with inductInfo? := .some {
numParams := induct.numParams,
numIndices := induct.numIndices,
all := induct.all.toArray.map (·.toString),
ctors := induct.ctors.toArray.map (·.toString),
isRec := induct.isRec,
isReflexive := induct.isReflexive,
isNested := induct.isNested,
} }
| .ctorInfo ctor => { core with constructorInfo? := .some {
induct := ctor.induct.toString,
cidx := ctor.cidx,
numParams := ctor.numParams,
numFields := ctor.numFields,
} }
| .recInfo r => { core with recursorInfo? := .some {
all := r.all.toArray.map (·.toString),
numParams := r.numParams,
numIndices := r.numIndices,
numMotives := r.numMotives,
numMinors := r.numMinors,
k := r.k,
} }
| _ => core
return .ok result
def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
let env ← Lean.MonadEnv.getEnv
let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
let type ← match syntax_from_str env args.type with
| .ok syn => do
match ← syntax_to_expr syn with
| .error e => return .error e
| .ok expr => pure expr
| .error e => return .error e
let value ← match syntax_from_str env args.value with
| .ok syn => do
try
let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
let expr ← instantiateMVars expr
pure $ expr
catch ex => return .error (← ex.toMessageData.toString)
| .error e => return .error e
pure $ .ok (type, value)
let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with
| .ok t => pure t
| .error e => return .error $ Protocol.errorExpr e
let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
(name := args.name.toName)
(levelParams := [])
(type := type)
(value := value)
(hints := Lean.mkReducibilityHintsRegularEx 1)
(safety := Lean.DefinitionSafety.safe)
(all := [])
let env' ← match env.addDecl constant with
| .error e => do
let options ← Lean.MonadOptions.getOptions
let desc ← (e.toMessageData options).toString
return .error $ { error := "kernel", desc }
| .ok env' => pure env'
Lean.MonadEnv.modifyEnv (λ _ => env')
return .ok {}
end Pantograph.Environment

234
Pantograph/Goal.lean Normal file
View File

@ -0,0 +1,234 @@
import Pantograph.Protocol
import Lean
def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
{
msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false
}
namespace Pantograph
open Lean
structure GoalState where
savedState : Elab.Tactic.SavedState
-- The root hole which is the search target
root: MVarId
-- New metavariables acquired in this state
newMVars: SSet MVarId
-- The id of the goal in the parent
parentGoalId: Nat := 0
-- Parent state metavariable source
parentMVar: Option MVarId
abbrev M := Elab.TermElabM
protected def GoalState.create (expr: Expr): M GoalState := do
-- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context.
-- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
--Elab.Term.synthesizeSyntheticMVarsNoPostponing
--let expr ← instantiateMVars expr
let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous))
let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
let root := goal.mvarId!
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]}
return {
savedState,
root,
newMVars := SSet.insert .empty root,
parentMVar := .none,
}
protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals
protected def GoalState.runM {α: Type} (state: GoalState) (m: Elab.TermElabM α) : M α := do
state.savedState.term.restore
m
protected def GoalState.mctx (state: GoalState): MetavarContext :=
state.savedState.term.meta.meta.mctx
protected def GoalState.env (state: GoalState): Environment :=
state.savedState.term.meta.core.env
private def GoalState.mvars (state: GoalState): SSet MVarId :=
state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
state.savedState.term.restore
def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
state.savedState.term.meta.restore
/-- Inner function for executing tactic on goal state -/
def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
M (Except (Array String) Elab.Tactic.SavedState):= do
let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := do
state.restore
Elab.Tactic.setGoals [goal]
try
Elab.Tactic.evalTactic stx
if (← getThe Core.State).messages.hasErrors then
let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
let errors ← (messages.map Message.data).mapM fun md => md.toString
return .error errors
else
return .ok (← MonadBacktrack.saveState)
catch exception =>
return .error #[← exception.toMessageData.toString]
tacticM tactic { elaborator := .anonymous } |>.run' state.tactic
/-- Response for executing a tactic -/
inductive TacticResult where
-- Goes to next state
| success (state: GoalState)
-- Tactic failed with messages
| failure (messages: Array String)
-- Could not parse tactic
| parseError (message: String)
-- The goal index is out of bounds
| indexError (goalId: Nat)
/-- Execute tactic on given state -/
protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String):
M TacticResult := do
state.restoreElabM
let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure $ goal
| .none => return .indexError goalId
let tactic ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `tactic)
(input := tactic)
(fileName := "<stdin>") with
| .ok stx => pure $ stx
| .error error => return .parseError error
match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
| .error errors =>
return .failure errors
| .ok nextSavedState =>
-- Assert that the definition of metavariables are the same
let nextMCtx := nextSavedState.term.meta.meta.mctx
let prevMCtx := state.savedState.term.meta.meta.mctx
-- Generate a list of mvarIds that exist in the parent state; Also test the
-- assertion that the types have not changed on any mvars.
let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
assert! prevMVarDecl.type == mvarDecl.type
return acc
else
return acc.insert mvarId
) SSet.empty
return .success {
root := state.root,
savedState := nextSavedState
newMVars,
parentGoalId := goalId,
parentMVar := .some goal,
}
protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
state.restoreElabM
let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure goal
| .none => return .indexError goalId
let expr ← match Parser.runParserCategory
(env := state.env)
(catName := `term)
(input := expr)
(fileName := "<stdin>") with
| .ok syn => pure syn
| .error error => return .parseError error
let tacticM: Elab.Tactic.TacticM TacticResult := do
state.savedState.restore
Elab.Tactic.setGoals [goal]
try
let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
-- Attempt to unify the expression
let goalType ← goal.getType
let exprType ← Meta.inferType expr
if !(← Meta.isDefEq goalType exprType) then
return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)]
goal.checkNotAssigned `GoalState.tryAssign
goal.assign expr
if (← getThe Core.State).messages.hasErrors then
let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
let errors ← (messages.map Message.data).mapM fun md => md.toString
return .failure errors
else
let prevMCtx := state.savedState.term.meta.meta.mctx
let nextMCtx ← getMCtx
-- Generate a list of mvarIds that exist in the parent state; Also test the
-- assertion that the types have not changed on any mvars.
let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
assert! prevMVarDecl.type == mvarDecl.type
return acc
else
return mvarId :: acc
) []
-- The new goals are the newMVars that lack an assignment
Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)))
let nextSavedState ← MonadBacktrack.saveState
return .success {
root := state.root,
savedState := nextSavedState,
newMVars := newMVars.toSSet,
parentGoalId := goalId,
parentMVar := .some goal,
}
catch exception =>
return .failure #[← exception.toMessageData.toString]
tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
/--
Brings into scope a list of goals
-/
protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
.error s!"Goals not in scope"
else
-- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
let unassigned := goals.filter (λ goal =>
let mctx := state.mctx
¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
.ok {
state with
savedState := {
term := state.savedState.term,
tactic := { goals := unassigned },
},
}
/--
Brings into scope all goals from `branch`
-/
protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
if !target.goals.isEmpty then
.error s!"Target state has unresolved goals"
else if target.root != branch.root then
.error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}"
else
target.resume (goals := branch.goals)
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
let expr ← goalState.mctx.eAssignment.find? goalState.root
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
if expr.hasMVar then
-- Must not assert that the goal state is empty here. We could be in a branch goal.
--assert! ¬goalState.goals.isEmpty
.none
else
assert! goalState.goals.isEmpty
return expr
protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
let parent ← goalState.parentMVar
let expr := goalState.mctx.eAssignment.find! parent
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
return expr
protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do
let expr ← goalState.mctx.eAssignment.find? mvar
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
return expr
end Pantograph

181
Pantograph/Library.lean Normal file
View File

@ -0,0 +1,181 @@
import Pantograph.Environment
import Pantograph.Goal
import Pantograph.Protocol
import Pantograph.Serial
import Pantograph.Version
import Lean
namespace Lean
/-- This is better than the default version since it handles `.` and doesn't
crash the program when it fails. -/
def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO Options := do
let ps := (entry.splitOn "=").map String.trim
let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'"
let key := key.toName
let defValue ← getOptionDefaultValue key
match defValue with
| DataValue.ofString _ => pure $ opts.setString key val
| DataValue.ofBool _ =>
match val with
| "true" => pure $ opts.setBool key true
| "false" => pure $ opts.setBool key false
| _ => throw s!"invalid Bool option value '{val}'"
| DataValue.ofName _ => pure $ opts.setName key val.toName
| DataValue.ofNat _ =>
match val.toNat? with
| none => throw s!"invalid Nat option value '{val}'"
| some v => pure $ opts.setNat key v
| DataValue.ofInt _ =>
match val.toInt? with
| none => throw s!"invalid Int option value '{val}'"
| some v => pure $ opts.setInt key v
| DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
end Lean
namespace Pantograph
def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
metaM.run'
def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
termElabM.run' (ctx := {
declName? := .none,
errToSorry := false,
}) |>.run'
def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
/-- Adds the given paths to Lean package search path -/
@[export pantograph_init_search]
unsafe def initSearch (sp: String): IO Unit := do
Lean.enableInitializersExecution
Lean.initSearchPath (← Lean.findSysroot) (sp := System.SearchPath.parse sp)
/-- Creates a Core.Context object needed to run all monads -/
@[export pantograph_create_core_context]
def createCoreContext (options: Array String): IO Lean.Core.Context := do
let options? ← options.foldlM Lean.setOptionFromString' Lean.Options.empty |>.run
let options ← match options? with
| .ok options => pure options
| .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
return {
currNamespace := Lean.Name.str .anonymous "Aniva"
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0] },
options := options
}
/-- Creates a Core.State object needed to run all monads -/
@[export pantograph_create_core_state]
def createCoreState (imports: Array String): IO Lean.Core.State := do
let env ← Lean.importModules
(imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
return { env := env }
@[export pantograph_env_catalog_m]
def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
Environment.catalog ({}: Protocol.EnvCatalog)
@[export pantograph_mk_options]
def mkOptions
(printJsonPretty: Bool)
(printExprPretty: Bool)
(printExprAST: Bool)
(noRepeat: Bool)
(printAuxDecls: Bool)
(printImplementationDetailHyps: Bool)
: Protocol.Options := {
printJsonPretty,
printExprPretty,
printExprAST,
noRepeat,
printAuxDecls,
printImplementationDetailHyps,
}
@[export pantograph_env_inspect_m]
def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) :=
Environment.inspect ({
name, value? := .some value, dependency?:= .some dependency
}: Protocol.EnvInspect) options
@[export pantograph_env_add_m]
def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
Lean.CoreM (Protocol.CR Protocol.EnvAddResult) :=
Environment.addDecl { name, type, value, isTheorem }
/-- This must be a TermElabM since the parsed expr contains extra information -/
def exprParse (s: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
let env ← Lean.MonadEnv.getEnv
let syn ← match syntax_from_str env s with
| .error str => return .error $ errorI "parsing" str
| .ok syn => pure syn
match ← syntax_to_expr syn with
| .error str => return .error $ errorI "elab" str
| .ok expr => return .ok expr
@[export pantograph_expr_echo_m]
def exprEcho (expr: String) (options: @&Protocol.Options):
Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
let termElabM: Lean.Elab.TermElabM _ := do
let expr ← match ← exprParse expr with
| .error e => return .error e
| .ok expr => pure expr
try
let type ← Lean.Meta.inferType expr
return .ok {
type := (← serialize_expression options type),
expr := (← serialize_expression options expr)
}
catch exception =>
return .error $ errorI "typing" (← exception.toMessageData.toString)
runTermElabM termElabM
@[export pantograph_goal_start_expr_m]
def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
let termElabM: Lean.Elab.TermElabM _ := do
let expr ← match ← exprParse expr with
| .error e => return .error e
| .ok expr => pure $ expr
return .ok $ ← GoalState.create expr
runTermElabM termElabM
@[export pantograph_goal_tactic_m]
def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult :=
runTermElabM <| GoalState.execute state goalId tactic
@[export pantograph_goal_try_assign_m]
def goalTryAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult :=
runTermElabM <| GoalState.tryAssign state goalId expr
@[export pantograph_goal_continue]
def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
target.continue branch
@[export pantograph_goal_resume]
def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
@[export pantograph_goal_serialize_m]
def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
runMetaM <| state.serializeGoals (parent := .none) options
@[export pantograph_goal_print_m]
def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do
let metaM := do
state.restoreMetaM
return {
root? := ← state.rootExpr?.mapM (λ expr => do
serialize_expression options (← unfoldAuxLemmas expr)),
parent? := ← state.parentExpr?.mapM (λ expr => do
serialize_expression options (← unfoldAuxLemmas expr)),
}
runMetaM metaM
end Pantograph

260
Pantograph/Protocol.lean Normal file
View File

@ -0,0 +1,260 @@
/-
All the command input/output structures are stored here
Note that no command other than `InteractionError` may have `error` as one of
its field names to avoid confusion with error messages generated by the REPL.
-/
import Lean.Data.Json
namespace Pantograph.Protocol
/-- Main Option structure, placed here to avoid name collision -/
structure Options where
-- When false, suppress newlines in Json objects. Useful for machine-to-machine interaction.
-- This should be false` by default to avoid any surprises with parsing.
printJsonPretty: Bool := false
-- When enabled, pretty print every expression
printExprPretty: Bool := true
-- When enabled, print the raw AST of expressions
printExprAST: Bool := false
-- When enabled, the types and values of persistent variables in a goal
-- are not shown unless they are new to the proof step. Reduces overhead.
-- NOTE: that this assumes the type and assignment of variables can never change.
noRepeat: Bool := false
-- See `pp.auxDecls`
printAuxDecls: Bool := false
-- See `pp.implementationDetailHyps`
printImplementationDetailHyps: Bool := false
deriving Lean.ToJson
abbrev OptionsT := ReaderT Options
--- Expression Objects ---
structure BoundExpression where
binders: Array (String × String)
target: String
deriving Lean.ToJson
structure Expression where
-- Pretty printed expression
pp?: Option String := .none
-- AST structure
sexp?: Option String := .none
deriving Lean.ToJson
structure Variable where
/-- The internal name used in raw expressions -/
name: String := ""
/-- The name displayed to the user -/
userName: String
/-- Does the name contain a dagger -/
isInaccessible?: Option Bool := .none
type?: Option Expression := .none
value?: Option Expression := .none
deriving Lean.ToJson
structure Goal where
name: String := ""
/-- Name of the metavariable -/
userName?: Option String := .none
/-- Is the goal in conversion mode -/
isConversion: Bool := false
/-- target expression type -/
target: Expression
/-- Variables -/
vars: Array Variable := #[]
deriving Lean.ToJson
--- Individual Commands and return types ---
structure Command where
cmd: String
payload: Lean.Json
deriving Lean.FromJson
structure InteractionError where
error: String
desc: String
deriving Lean.ToJson
def errorIndex (desc: String): InteractionError := { error := "index", desc }
def errorExpr (desc: String): InteractionError := { error := "expr", desc }
--- Individual command and return types ---
structure Reset where
deriving Lean.FromJson
structure Stat where
deriving Lean.FromJson
structure StatResult where
-- Number of goals states
nGoals: Nat
deriving Lean.ToJson
-- Return the type of an expression
structure ExprEcho where
expr: String
deriving Lean.FromJson
structure ExprEchoResult where
expr: Expression
type: Expression
deriving Lean.ToJson
-- Print all symbols in environment
structure EnvCatalog where
deriving Lean.FromJson
structure EnvCatalogResult where
symbols: Array String
deriving Lean.ToJson
-- Print the type of a symbol
structure EnvInspect where
name: String
-- If true/false, show/hide the value expressions; By default definitions
-- values are shown and theorem values are hidden.
value?: Option Bool := .some false
-- If true, show the type and value dependencies
dependency?: Option Bool := .some false
deriving Lean.FromJson
-- See `InductiveVal`
structure InductInfo where
numParams: Nat
numIndices: Nat
all: Array String
ctors: Array String
isRec: Bool := false
isReflexive: Bool := false
isNested: Bool := false
deriving Lean.ToJson
-- See `ConstructorVal`
structure ConstructorInfo where
induct: String
cidx: Nat
numParams: Nat
numFields: Nat
deriving Lean.ToJson
structure RecursorInfo where
all: Array String
numParams: Nat
numIndices: Nat
numMotives: Nat
numMinors: Nat
k: Bool
deriving Lean.ToJson
structure EnvInspectResult where
type: Expression
isUnsafe: Bool := false
value?: Option Expression := .none
module?: Option String := .none
-- If the name is private, displays the public facing name
publicName?: Option String := .none
typeDependency?: Option (Array String) := .none
valueDependency?: Option (Array String) := .none
inductInfo?: Option InductInfo := .none
constructorInfo?: Option ConstructorInfo := .none
recursorInfo?: Option RecursorInfo := .none
deriving Lean.ToJson
structure EnvAdd where
name: String
type: String
value: String
isTheorem: Bool
deriving Lean.FromJson
structure EnvAddResult where
deriving Lean.ToJson
/-- Set options; See `Options` struct above for meanings -/
structure OptionsSet where
printJsonPretty?: Option Bool
printExprPretty?: Option Bool
printExprAST?: Option Bool
noRepeat?: Option Bool
printAuxDecls?: Option Bool
printImplementationDetailHyps?: Option Bool
deriving Lean.FromJson
structure OptionsSetResult where
deriving Lean.ToJson
structure OptionsPrint where
deriving Lean.FromJson
abbrev OptionsPrintResult := Options
structure GoalStart where
-- Only one of the fields below may be populated.
expr: Option String -- Directly parse in an expression
copyFrom: Option String -- Copy the type from a theorem in the environment
deriving Lean.FromJson
structure GoalStartResult where
stateId: Nat := 0
-- Name of the root metavariable
root: String
deriving Lean.ToJson
structure GoalTactic where
-- Identifiers for tree, state, and goal
stateId: Nat
goalId: Nat := 0
-- One of the fields here must be filled
tactic?: Option String := .none
expr?: Option String := .none
deriving Lean.FromJson
structure GoalTacticResult where
-- The next goal state id. Existence of this field shows success
nextStateId?: Option Nat := .none
-- If the array is empty, it shows the goals have been fully resolved.
goals?: Option (Array Goal) := .none
-- Existence of this field shows tactic execution failure
tacticErrors?: Option (Array String) := .none
-- Existence of this field shows the tactic parsing has failed
parseError?: Option String := .none
deriving Lean.ToJson
structure GoalContinue where
-- State from which the continuation acquires the context
target: Nat
-- One of the following must be supplied
-- The state which is an ancestor of `target` where goals will be extracted from
branch?: Option Nat := .none
-- Or, the particular goals that should be brought back into scope
goals?: Option (Array String) := .none
deriving Lean.FromJson
structure GoalContinueResult where
nextStateId: Nat
goals: (Array Goal)
deriving Lean.ToJson
-- Remove goal states
structure GoalDelete where
-- This is ok being a List because it doesn't show up in the ABI
stateIds: List Nat
deriving Lean.FromJson
structure GoalDeleteResult where
deriving Lean.ToJson
structure GoalPrint where
stateId: Nat
deriving Lean.FromJson
structure GoalPrintResult where
-- The root expression
root?: Option Expression := .none
-- The filling expression of the parent goal
parent?: Option Expression
deriving Lean.ToJson
-- Diagnostic Options, not available in REPL
structure GoalDiag where
printContext: Bool := true
printValue: Bool := true
printNewMVars: Bool := false
-- Print all mvars
printAll: Bool := false
instantiate: Bool := true
abbrev CR α := Except InteractionError α
end Pantograph.Protocol

315
Pantograph/Serial.lean Normal file
View File

@ -0,0 +1,315 @@
/-
All serialisation functions
-/
import Lean
import Pantograph.Protocol
import Pantograph.Goal
open Lean
-- Symbol processing functions --
def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
namespace Pantograph
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
--- Input Functions ---
/-- Read syntax object from string -/
def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
Parser.runParserCategory
(env := env)
(catName := `term)
(input := s)
(fileName := "<stdin>")
/-- Parse a syntax object. May generate additional metavariables! -/
def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
try
let expr ← Elab.Term.elabType syn
return .ok expr
catch ex => return .error (← ex.toMessageData.toString)
def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
try
let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none)
return .ok expr
catch ex => return .error (← ex.toMessageData.toString)
--- Output Functions ---
def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := do
Meta.forallTelescope expr fun arr body => do
let binders ← arr.mapM fun fvar => do
return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
return { binders, target := toString (← Meta.ppExpr body) }
def name_to_ast (name: Name) (sanitize: Bool := true): String :=
let internal := name.isInaccessibleUserName || name.hasMacroScopes
if sanitize && internal then "_"
else toString name |> enclose_if_escaped
where
enclose_if_escaped (n: String) :=
let quote := "\""
if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
/-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
partial def serialize_sort_level_ast (level: Level) (sanitize: Bool): String :=
let k := level.getOffset
let u := level.getLevelOffset
let u_str := match u with
| .zero => "0"
| .succ _ => panic! "getLevelOffset should not return .succ"
| .max v w =>
let v := serialize_sort_level_ast v sanitize
let w := serialize_sort_level_ast w sanitize
s!"(:max {v} {w})"
| .imax v w =>
let v := serialize_sort_level_ast v sanitize
let w := serialize_sort_level_ast w sanitize
s!"(:imax {v} {w})"
| .param name =>
let name := name_to_ast name sanitize
s!"{name}"
| .mvar id =>
let name := name_to_ast id.name sanitize
s!"(:mv {name})"
match k, u with
| 0, _ => u_str
| _, .zero => s!"{k}"
| _, _ => s!"(+ {u_str} {k})"
/--
Completely serializes an expression tree. Json not used due to compactness
-/
partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do
self expr
where
self (e: Expr): MetaM String :=
match e with
| .bvar deBruijnIndex =>
-- This is very common so the index alone is shown. Literals are handled below.
-- The raw de Bruijn index should never appear in an unbound setting. In
-- Lean these are handled using a `#` prefix.
pure s!"{deBruijnIndex}"
| .fvar fvarId =>
let name := of_name fvarId.name
pure s!"(:fv {name})"
| .mvar mvarId =>
let name := of_name mvarId.name
pure s!"(:mv {name})"
| .sort level =>
let level := serialize_sort_level_ast level sanitize
pure s!"(:sort {level})"
| .const declName _ =>
-- The universe level of the const expression is elided since it should be
-- inferrable from surrounding expression
pure s!"(:c {declName})"
| .app _ _ => do
let fn' ← self e.getAppFn
let args := (← e.getAppArgs.mapM self) |>.toList
let args := " ".intercalate args
pure s!"({fn'} {args})"
| .lam binderName binderType body binderInfo => do
let binderName' := of_name binderName
let binderType' ← self binderType
let body' ← self body
let binderInfo' := binder_info_to_ast binderInfo
pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
| .forallE binderName binderType body binderInfo => do
let binderName' := of_name binderName
let binderType' ← self binderType
let body' ← self body
let binderInfo' := binder_info_to_ast binderInfo
pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
| .letE name type value body _ => do
-- Dependent boolean flag diacarded
let name' := name_to_ast name
let type' ← self type
let value' ← self value
let body' ← self body
pure s!"(:let {name'} {type'} {value'} {body'})"
| .lit v =>
-- To not burden the downstream parser who needs to handle this, the literal
-- is wrapped in a :lit sexp.
let v' := match v with
| .natVal val => toString val
| .strVal val => s!"\"{val}\""
pure s!"(:lit {v'})"
| .mdata _ inner =>
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
-- It may become necessary to incorporate the metadata.
self inner
| .proj typeName idx inner => do
let env ← getEnv
let fieldName := getStructureFields env typeName |>.get! idx
let projectorName := getProjFnForField? env typeName fieldName |>.get!
let e := Expr.app (.const projectorName []) inner
self e
-- Elides all unhygenic names
binder_info_to_ast : Lean.BinderInfo → String
| .default => ""
| .implicit => " :implicit"
| .strictImplicit => " :strictImplicit"
| .instImplicit => " :instImplicit"
of_name (name: Name) := name_to_ast name sanitize
def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
let pp := toString (← Meta.ppExpr e)
let pp?: Option String := match options.printExprPretty with
| true => .some pp
| false => .none
let sexp: String ← serialize_expression_ast e
let sexp?: Option String := match options.printExprAST with
| true => .some sexp
| false => .none
return {
pp?,
sexp?
}
/-- Adapted from ppGoal -/
def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
: MetaM Protocol.Goal := do
-- Options for printing; See Meta.ppGoal for details
let showLetValues := true
let ppAuxDecls := options.printAuxDecls
let ppImplDetailHyps := options.printImplementationDetailHyps
let lctx := mvarDecl.lctx
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
Meta.withLCtx lctx mvarDecl.localInstances do
let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
match localDecl with
| .cdecl _ fvarId userName _ _ _ =>
let userName := userName.simpMacroScopes
return {
name := of_name fvarId.name,
userName:= of_name userName.simpMacroScopes,
}
| .ldecl _ fvarId userName _ _ _ _ => do
return {
name := of_name fvarId.name,
userName := toString userName.simpMacroScopes,
}
let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
match localDecl with
| .cdecl _ fvarId userName type _ _ =>
let userName := userName.simpMacroScopes
let type ← instantiateMVars type
return {
name := of_name fvarId.name,
userName:= of_name userName,
isInaccessible? := .some userName.isInaccessibleUserName
type? := .some (← serialize_expression options type)
}
| .ldecl _ fvarId userName type val _ _ => do
let userName := userName.simpMacroScopes
let type ← instantiateMVars type
let value? ← if showLetValues then
let val ← instantiateMVars val
pure $ .some (← serialize_expression options val)
else
pure $ .none
return {
name := of_name fvarId.name,
userName:= of_name userName,
isInaccessible? := .some userName.isInaccessibleUserName
type? := .some (← serialize_expression options type)
value? := value?
}
let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
let skip := !ppAuxDecls && localDecl.isAuxDecl ||
!ppImplDetailHyps && localDecl.isImplementationDetail
if skip then
return acc
else
let nameOnly := options.noRepeat && (parentDecl?.map
(λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
let var ← match nameOnly with
| true => ppVarNameOnly localDecl
| false => ppVar localDecl
return var::acc
return {
name := of_name goal.name,
userName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName),
isConversion := isLHSGoal? mvarDecl.type |>.isSome,
target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
vars := vars.reverse.toArray
}
where
of_name (n: Name) := name_to_ast n (sanitize := false)
protected def GoalState.serializeGoals
(state: GoalState)
(parent: Option GoalState := .none)
(options: @&Protocol.Options := {}):
MetaM (Array Protocol.Goal):= do
state.restoreMetaM
let goals := state.goals.toArray
let parentDecl? := parent.bind (λ parentState =>
let parentGoal := parentState.goals.get! state.parentGoalId
parentState.mctx.findDecl? parentGoal)
goals.mapM fun goal => do
match state.mctx.findDecl? goal with
| .some mvarDecl =>
let serializedGoal ← serialize_goal options goal mvarDecl (parentDecl? := parentDecl?)
pure serializedGoal
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
/-- Print the metavariables in a readable format -/
protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
goalState.restoreMetaM
let savedState := goalState.savedState
let goals := savedState.tactic.goals
let mctx ← getMCtx
let root := goalState.root
-- Print the root
match mctx.decls.find? root with
| .some decl => printMVar ">" root decl
| .none => IO.println s!">{root.name}: ??"
goals.forM (fun mvarId => do
if mvarId != root then
match mctx.decls.find? mvarId with
| .some decl => printMVar "⊢" mvarId decl
| .none => IO.println s!"⊢{mvarId.name}: ??"
)
let goals := goals.toSSet
mctx.decls.forM (fun mvarId decl => do
if goals.contains mvarId || mvarId == root then
pure ()
-- Print the remainig ones that users don't see in Lean
else if options.printAll then
let pref := if goalState.newMVars.contains mvarId then "~" else " "
printMVar pref mvarId decl
else
pure ()
--IO.println s!" {mvarId.name}{userNameToString decl.userName}"
)
where
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
if options.printContext then
decl.lctx.fvarIdToDecl.forM printFVar
let type ← if options.instantiate
then instantiateMVars decl.type
else pure $ decl.type
let type_sexp ← serialize_expression_ast type (sanitize := false)
IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
if options.printValue then
if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
let value ← if options.instantiate
then instantiateMVars value
else pure $ value
IO.println s!" := {← Meta.ppExpr value}"
printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do
IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
userNameToString : Name → String
| .anonymous => ""
| other => s!"[{other}]"
end Pantograph

6
Pantograph/Version.lean Normal file
View File

@ -0,0 +1,6 @@
namespace Pantograph
@[export pantograph_version]
def version := "0.2.14"
end Pantograph

139
README.md Normal file
View File

@ -0,0 +1,139 @@
# Pantograph
A Machine-to-Machine interaction system for Lean 4.
![Pantograph](doc/icon.svg)
Pantograph provides interfaces to execute proofs, construct expressions, and
examine the symbol list of a Lean project for machine learning.
## Installation
For Nix based workflow, see below.
Install `elan` and `lake`. Execute
``` sh
make build/bin/pantograph
```
setup the `LEAN_PATH` environment variable so it contains the library path of lean libraries. The libraries must be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
``` sh
LIB="../lib"
LIB_MATHLIB="$LIB/mathlib4/lake-packages"
export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
```
The provided `flake.nix` has a develop environment with Lean already setup.
## Executable Usage
``` sh
pantograph MODULES|LEAN_OPTIONS
```
The REPL loop accepts commands as single-line JSON inputs and outputs either an
`Error:` (indicating malformed command) or a JSON return value indicating the
result of a command execution. The command can be passed in one of two formats
```
command { ... }
{ "cmd": command, "payload": ... }
```
The list of available commands can be found in `Pantograph/Protocol.lean` and below. An
empty command aborts the REPL.
The `pantograph` executable must be run with a list of modules to import. It can
also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
Example: (~5k symbols)
```
$ pantograph Init
env.catalog
env.inspect {"name": "Nat.le_add_left"}
```
Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
```
$ pantograph Mathlib.Analysis.Seminorm
env.catalog
```
Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
```
$ pantograph Init
goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
goal.tactic {"stateId": 0, "goalId": 0, "tactic": "intro n m"}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "assumption"}
goal.delete {"stateIds": [0]}
stat {}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"}
stat
```
where the application of `assumption` should lead to a failure.
### Commands
See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
- `reset`: Delete all cached expressions and proof trees
- `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
- `env.catalog`: Display a list of all safe Lean symbols in the current environment
- `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
given symbol; If value flag is set, the value is printed or hidden. By default
only the values of definitions are printed.
- `options.set { key: value, ... }`: Set one or more options (not Lean options; those
have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
- `options.print`: Display the current set of options
- `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr": <expr>]}`: Execute a tactic string on a given goal
- `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`: Continue from a proof state
- `goal.remove {"stateIds": [<id>]}"`: Remove a bunch of stored goals.
- `goal.print {"stateId": <id>}"`: Print a goal state
- `stat`: Display resource usage
### Errors
When an error pertaining to the execution of a command happens, the returning JSON structure is
``` json
{ error: "type", desc: "description" }
```
Common error forms:
* `command`: Indicates malformed command structure which results from either
invalid command or a malformed JSON structure that cannot be fed to an
individual command.
* `index`: Indicates an invariant maintained by the output of one command and
input of another is broken. For example, attempting to query a symbol not
existing in the library or indexing into a non-existent proof state.
### Troubleshooting
If lean encounters stack overflow problems when printing catalog, execute this before running lean:
```sh
ulimit -s unlimited
```
## Library Usage
`Pantograph/Library.lean` exposes a series of interfaces which allow FFI call
with `Pantograph` which mirrors the REPL commands above. It is recommended to
call Pantograph via this FFI since it provides a tremendous speed up.
## Developing
### Testing
The tests are based on `LSpec`. To run tests,
``` sh
make test
```
## Nix based workflow
The included Nix flake provides build targets for `sharedLib` and `executable`.
The executable can be used as-is, but linking against the shared library
requires the presence of `lean-all`.
To run tests:
``` sh
nix build .#checks.${system}.test
```
For example, `${system}` could be `x86_64-linux`. Using `nix develop` drops the
current session into a development shell with fixed Lean version.

60
Test/Common.lean Normal file
View File

@ -0,0 +1,60 @@
import Pantograph.Goal
import Pantograph.Library
import Pantograph.Protocol
import Lean
import LSpec
open Lean
namespace Pantograph
namespace Protocol
/-- Set internal names to "" -/
def Goal.devolatilize (goal: Goal): Goal :=
{
goal with
name := "",
vars := goal.vars.map removeInternalAux,
}
where removeInternalAux (v: Variable): Variable :=
{
v with
name := ""
}
deriving instance DecidableEq, Repr for Expression
deriving instance DecidableEq, Repr for Variable
deriving instance DecidableEq, Repr for Goal
end Protocol
def TacticResult.toString : TacticResult → String
| .success state => s!".success ({state.goals.length} goals)"
| .failure messages =>
let messages := "\n".intercalate messages.toList
s!".failure {messages}"
| .parseError error => s!".parseError {error}"
| .indexError index => s!".indexError {index}"
def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
open Lean
def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq): IO LSpec.TestSeq := do
let coreContext: Core.Context ← createCoreContext #[]
match ← (coreM.run' coreContext { env := env }).toBaseIO with
| .error exception =>
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
| .ok a => return a
def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
runCoreMSeq env metaM.run'
def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
termElabM.run' (ctx := {
declName? := .none,
errToSorry := false,
})
def defaultTermElabMContext: Lean.Elab.Term.Context := {
declName? := some "_pantograph".toName,
errToSorry := false
}
end Pantograph

103
Test/Environment.lean Normal file
View File

@ -0,0 +1,103 @@
import LSpec
import Pantograph.Serial
import Pantograph.Environment
import Test.Common
import Lean
open Lean
namespace Pantograph.Test.Environment
open Pantograph
deriving instance DecidableEq, Repr for Protocol.InductInfo
deriving instance DecidableEq, Repr for Protocol.ConstructorInfo
deriving instance DecidableEq, Repr for Protocol.RecursorInfo
deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
def test_catalog: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
let inner: CoreM LSpec.TestSeq := do
let catalogResult ← Environment.catalog {}
let symbolsWithNum := env.constants.fold (init := #[]) (λ acc name info =>
match (Environment.toFilteredSymbol name info).isSome && (name matches .num _ _) with
| false => acc
| true => acc.push name
)
return LSpec.check "No num symbols" (symbolsWithNum.size == 0)
runCoreMSeq env inner
def test_symbol_visibility: IO LSpec.TestSeq := do
let entries: List (Name × Bool) := [
("Nat.add_comm".toName, false),
("Lean.Name".toName, true),
("Init.Data.Nat.Basic._auxLemma.4".toName, true),
]
let suite := entries.foldl (λ suites (symbol, target) =>
let test := LSpec.check symbol.toString ((Environment.isNameInternal symbol) == target)
LSpec.TestSeq.append suites test) LSpec.TestSeq.done
return suite
inductive ConstantCat where
| induct (info: Protocol.InductInfo)
| ctor (info: Protocol.ConstructorInfo)
| recursor (info: Protocol.RecursorInfo)
def test_inspect: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
let testCases: List (String × ConstantCat) := [
("Or", ConstantCat.induct {
numParams := 2,
numIndices := 0,
all := #["Or"],
ctors := #["Or.inl", "Or.inr"],
}),
("Except.ok", ConstantCat.ctor {
induct := "Except",
cidx := 1,
numParams := 2,
numFields := 1,
}),
("Eq.rec", ConstantCat.recursor {
all := #["Eq"],
numParams := 2,
numIndices := 1,
numMotives := 1,
numMinors := 1,
k := true,
}),
("ForM.rec", ConstantCat.recursor {
all := #["ForM"],
numParams := 3,
numIndices := 0,
numMotives := 1,
numMinors := 1,
k := false,
})
]
let inner: CoreM LSpec.TestSeq := do
testCases.foldlM (λ acc (name, cat) => do
let args: Protocol.EnvInspect := { name := name }
let result ← match ← Environment.inspect args (options := {}) with
| .ok result => pure $ result
| .error e => panic! s!"Error: {e.desc}"
let p := match cat with
| .induct info => LSpec.test name (result.inductInfo? == .some info)
| .ctor info => LSpec.test name (result.constructorInfo? == .some info)
| .recursor info => LSpec.test name (result.recursorInfo? == .some info)
return LSpec.TestSeq.append acc p
) LSpec.TestSeq.done
runCoreMSeq env inner
def suite: IO LSpec.TestSeq := do
return LSpec.group "Environment" $
(LSpec.group "Catalog" (← test_catalog)) ++
(LSpec.group "Symbol visibility" (← test_symbol_visibility)) ++
(LSpec.group "Inspect" (← test_inspect))
end Pantograph.Test.Environment

160
Test/Integration.lean Normal file
View File

@ -0,0 +1,160 @@
/- Integration test for the REPL
-/
import LSpec
import Pantograph
namespace Pantograph.Test.Integration
open Pantograph
def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json))
(expected: Lean.Json): MainM LSpec.TestSeq := do
let result ← execute { cmd := cmd, payload := Lean.Json.mkObj payload }
return LSpec.test name (toString result = toString expected)
def subroutine_step (cmd: String) (payload: List (String × Lean.Json))
(expected: Lean.Json): MainM LSpec.TestSeq := subroutine_named_step cmd cmd payload expected
def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do
-- Setup the environment for execution
let env ← Lean.importModules
(imports := #[{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }])
(opts := {})
(trustLevel := 1)
let context: Context := {
imports := ["Init"]
}
let coreContext: Lean.Core.Context ← createCoreContext #[]
let commands: MainM LSpec.TestSeq :=
steps.foldlM (λ suite step => do
let result ← step
return suite ++ result) LSpec.TestSeq.done
try
let coreM := commands.run context |>.run' {}
return Prod.fst $ (← coreM.toIO coreContext { env := env })
catch ex =>
return LSpec.check s!"Uncaught IO exception: {ex.toString}" false
def test_option_modify : IO LSpec.TestSeq :=
let pp? := Option.some "∀ (n : Nat), n + 1 = n.succ"
let sexp? := Option.some "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"
let module? := Option.some "Init.Data.Nat.Basic"
let options: Protocol.Options := {}
subroutine_runner [
subroutine_step "env.inspect"
[("name", .str "Nat.add_one")]
(Lean.toJson ({
type := { pp? }, module? }:
Protocol.EnvInspectResult)),
subroutine_step "options.set"
[("printExprAST", .bool true)]
(Lean.toJson ({ }:
Protocol.OptionsSetResult)),
subroutine_step "env.inspect"
[("name", .str "Nat.add_one")]
(Lean.toJson ({
type := { pp?, sexp? }, module? }:
Protocol.EnvInspectResult)),
subroutine_step "options.print"
[]
(Lean.toJson ({ options with printExprAST := true }:
Protocol.OptionsPrintResult))
]
def test_malformed_command : IO LSpec.TestSeq :=
let invalid := "invalid"
subroutine_runner [
subroutine_named_step "Invalid command" invalid
[("name", .str "Nat.add_one")]
(Lean.toJson ({
error := "command", desc := s!"Unknown command {invalid}"}:
Protocol.InteractionError)),
subroutine_named_step "JSON Deserialization" "expr.echo"
[(invalid, .str "Random garbage data")]
(Lean.toJson ({
error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}:
Protocol.InteractionError))
]
def test_tactic : IO LSpec.TestSeq :=
let goal1: Protocol.Goal := {
name := "_uniq.10",
target := { pp? := .some "∀ (q : Prop), x q → q x" },
vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
}
let goal2: Protocol.Goal := {
name := "_uniq.13",
target := { pp? := .some "x y → y x" },
vars := #[
{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
{ name := "_uniq.12", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
],
}
subroutine_runner [
subroutine_step "goal.start"
[("expr", .str "∀ (p q: Prop), p q → q p")]
(Lean.toJson ({stateId := 0, root := "_uniq.8"}:
Protocol.GoalStartResult)),
subroutine_step "goal.tactic"
[("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
(Lean.toJson ({
nextStateId? := .some 1,
goals? := #[goal1],
}:
Protocol.GoalTacticResult)),
subroutine_step "goal.print"
[("stateId", .num 1)]
(Lean.toJson ({
parent? := .some { pp? := .some "fun x => ?m.11 x" },
}:
Protocol.GoalPrintResult)),
subroutine_step "goal.tactic"
[("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
(Lean.toJson ({
nextStateId? := .some 2,
goals? := #[goal2],
}:
Protocol.GoalTacticResult))
]
def test_env : IO LSpec.TestSeq :=
let name1 := "Pantograph.mystery"
let name2 := "Pantograph.mystery2"
subroutine_runner [
subroutine_step "env.add"
[
("name", .str name1),
("type", .str "Prop → Prop → Prop"),
("value", .str "λ (a b: Prop) => Or a b"),
("isTheorem", .bool false)
]
(Lean.toJson ({}: Protocol.EnvAddResult)),
subroutine_step "env.inspect"
[("name", .str name1)]
(Lean.toJson ({
value? := .some { pp? := .some "fun a b => a b" },
type := { pp? := .some "Prop → Prop → Prop" },
}:
Protocol.EnvInspectResult)),
subroutine_step "env.add"
[
("name", .str name2),
("type", .str "Nat → Int"),
("value", .str "λ (a: Nat) => a + 1"),
("isTheorem", .bool false)
]
(Lean.toJson ({}: Protocol.EnvAddResult)),
subroutine_step "env.inspect"
[("name", .str name2)]
(Lean.toJson ({
value? := .some { pp? := .some "fun a => ↑a + 1" },
type := { pp? := .some "Nat → Int" },
}:
Protocol.EnvInspectResult))
]
def suite: IO LSpec.TestSeq := do
return LSpec.group "Integration" $
(LSpec.group "Option modify" (← test_option_modify)) ++
(LSpec.group "Malformed command" (← test_malformed_command)) ++
(LSpec.group "Tactic" (← test_tactic)) ++
(LSpec.group "Env" (← test_env))
end Pantograph.Test.Integration

21
Test/Main.lean Normal file
View File

@ -0,0 +1,21 @@
import LSpec
import Test.Environment
import Test.Metavar
import Test.Integration
import Test.Proofs
import Test.Serial
open Pantograph.Test
def main := do
Lean.initSearchPath (← Lean.findSysroot)
let suites := [
Metavar.suite,
Integration.suite,
Proofs.suite,
Serial.suite,
Environment.suite
]
let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
LSpec.lspecIO $ all

267
Test/Metavar.lean Normal file
View File

@ -0,0 +1,267 @@
import LSpec
import Pantograph.Goal
import Pantograph.Serial
import Test.Common
import Lean
namespace Pantograph.Test.Metavar
open Pantograph
open Lean
abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
def addTest (test: LSpec.TestSeq): TestM Unit := do
set $ (← get) ++ test
def startProof (expr: String): TestM (Option GoalState) := do
let env ← Lean.MonadEnv.getEnv
let syn? := syntax_from_str env expr
addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
match syn? with
| .error error =>
IO.println error
return Option.none
| .ok syn =>
let expr? ← syntax_to_expr_type syn
addTest $ LSpec.check s!"Elaborating" expr?.isOk
match expr? with
| .error error =>
IO.println error
return Option.none
| .ok expr =>
let goal ← GoalState.create (expr := expr)
return Option.some goal
def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal :=
{
userName?,
target := { pp? := .some target},
vars := (nameType.map fun x => ({
userName := x.fst,
type? := .some { pp? := .some x.snd },
isInaccessible? := .some false
})).toArray
}
def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
let coreContext: Lean.Core.Context ← createCoreContext #[]
let metaM := termElabM.run' (ctx := defaultTermElabMContext)
let coreM := metaM.run'
match ← (coreM.run' coreContext { env := env }).toBaseIO with
| .error exception =>
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
| .ok (_, a) =>
return a
/-- M-coupled goals -/
def test_m_couple: TestM Unit := do
let state? ← startProof "(2: Nat) ≤ 5"
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
-- Set m to 3
let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
let state1b ← match state2.continue state1 with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ 3", .some "3 ≤ 5"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
def test_m_couple_simp: TestM Unit := do
let state? ← startProof "(2: Nat) ≤ 5"
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 2") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
let state1b ← match state2.continue state1 with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ 2", .some "2 ≤ 5"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
let state3 ← match ← state1b.execute (goalId := 0) (tactic := "simp") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let state4 ← match state3.continue state1b with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
let state5 ← match ← state4.execute (goalId := 0) (tactic := "simp") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
state5.restoreMetaM
let root ← match state5.rootExpr? with
| .some e => pure e
| .none =>
addTest $ assertUnreachable "(5 root)"
return ()
let rootStr: String := toString (← Lean.Meta.ppExpr root)
addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
let rootStr: String := toString (← Lean.Meta.ppExpr (← unfoldAuxLemmas root))
addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
return ()
def test_proposition_generation: TestM Unit := do
let state? ← startProof "Σ' p:Prop, p"
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply PSigma.mk") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[
buildGoal [] "?fst" (userName? := .some "snd"),
buildGoal [] "Prop" (userName? := .some "fst")
])
if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then
addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})")
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"])
addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
#[])
addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
return ()
def test_partial_continuation: TestM Unit := do
let state? ← startProof "(2: Nat) ≤ 5"
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
let state2 ← match ← state1.execute (goalId := 2) (tactic := "apply Nat.succ") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "apply Nat.succ" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "Nat"])
-- Execute a partial continuation
let coupled_goals := state1.goals ++ state2.goals
let state1b ← match state2.resume (goals := coupled_goals) with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
-- Roundtrip
--let coupled_goals := coupled_goals.map (λ g =>
-- { name := str_to_name $ name_to_ast g.name (sanitize := false)})
let coupled_goals := coupled_goals.map (λ g => name_to_ast g.name (sanitize := false))
let coupled_goals := coupled_goals.map (λ g => { name := g.toName })
let state1b ← match state2.resume (goals := coupled_goals) with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
-- Continuation should fail if the state does not exist:
match state0.resume coupled_goals with
| .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope")
| .ok _ => addTest $ assertUnreachable "(continuation failure)"
-- Continuation should fail if some goals have not been solved
match state2.continue state1 with
| .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Target state has unresolved goals")
| .ok _ => addTest $ assertUnreachable "(continuation failure)"
return ()
def suite: IO LSpec.TestSeq := do
let env: Lean.Environment ← Lean.importModules
(imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
let tests := [
("2 < 5", test_m_couple),
("2 < 5", test_m_couple_simp),
("Proposition Generation", test_proposition_generation),
("Partial Continuation", test_partial_continuation)
]
let tests ← tests.foldlM (fun acc tests => do
let (name, tests) := tests
let tests ← proofRunner env tests
return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
return LSpec.group "Metavar" tests
end Pantograph.Test.Metavar

316
Test/Proofs.lean Normal file
View File

@ -0,0 +1,316 @@
/-
Tests pertaining to goals with no interdependencies
-/
import LSpec
import Pantograph.Goal
import Pantograph.Serial
import Test.Common
namespace Pantograph.Test.Proofs
open Pantograph
open Lean
inductive Start where
| copy (name: String) -- Start from some name in the environment
| expr (expr: String) -- Start from some expression
abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
def addTest (test: LSpec.TestSeq): TestM Unit := do
set $ (← get) ++ test
def startProof (start: Start): TestM (Option GoalState) := do
let env ← Lean.MonadEnv.getEnv
match start with
| .copy name =>
let cInfo? := name.toName |> env.find?
addTest $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
match cInfo? with
| .some cInfo =>
let goal ← GoalState.create (expr := cInfo.type)
return Option.some goal
| .none =>
return Option.none
| .expr expr =>
let syn? := syntax_from_str env expr
addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
match syn? with
| .error error =>
IO.println error
return Option.none
| .ok syn =>
let expr? ← syntax_to_expr_type syn
addTest $ LSpec.check s!"Elaborating" expr?.isOk
match expr? with
| .error error =>
IO.println error
return Option.none
| .ok expr =>
let goal ← GoalState.create (expr := expr)
return Option.some goal
def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal :=
{
userName?,
target := { pp? := .some target},
vars := (nameType.map fun x => ({
userName := x.fst,
type? := .some { pp? := .some x.snd },
isInaccessible? := .some false
})).toArray
}
def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
let coreContext: Lean.Core.Context ← createCoreContext #[]
let metaM := termElabM.run' (ctx := defaultTermElabMContext)
let coreM := metaM.run'
match ← (coreM.run' coreContext { env := env }).toBaseIO with
| .error exception =>
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
| .ok (_, a) =>
return a
-- Individual test cases
example: ∀ (a b: Nat), a + b = b + a := by
intro n m
rw [Nat.add_comm]
def proof_nat_add_comm (manual: Bool): TestM Unit := do
let state? ← startProof <| match manual with
| false => .copy "Nat.add_comm"
| true => .expr "∀ (a b: Nat), a + b = b + a"
addTest $ LSpec.check "Start goal" state?.isSome
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n m") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"])
match ← state1.execute (goalId := 0) (tactic := "assumption") with
| .failure #[message] =>
addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
| other => do
addTest $ assertUnreachable $ other.toString
let state2 ← match ← state1.execute (goalId := 0) (tactic := "rw [Nat.add_comm]") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty
return ()
def proof_delta_variable: TestM Unit := do
let options: Protocol.Options := { noRepeat := true }
let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a"
addTest $ LSpec.check "Start goal" state?.isSome
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
#[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
let state2 ← match ← state1.execute (goalId := 0) (tactic := "intro m") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "intro m" ((← state2.serializeGoals (parent := state1) options).map (·.devolatilize) =
#[buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n"])
return ()
where
-- Like `buildGoal` but allow certain variables to be elided.
buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal :=
{
target := { pp? := .some target},
vars := (nameType.map fun x => ({
userName := x.fst,
type? := x.snd.map (λ type => { pp? := type }),
isInaccessible? := x.snd.map (λ _ => false)
})).toArray
}
example (w x y z : Nat) (p : Nat → Prop)
(h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
assumption
def proof_arith: TestM Unit := do
let state? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.execute (goalId := 0) (tactic := "intros") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "intros" (state1.goals.length = 1)
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
let state2 ← match ← state1.execute (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test "assumption" state3.goals.isEmpty
addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
return ()
-- Two ways to write the same theorem
example: ∀ (p q: Prop), p q → q p := by
intro p q h
cases h
apply Or.inr
assumption
apply Or.inl
assumption
example: ∀ (p q: Prop), p q → q p := by
intro p q h
cases h
. apply Or.inr
assumption
. apply Or.inl
assumption
def proof_or_comm: TestM Unit := do
let state? ← startProof (.expr "∀ (p q: Prop), p q → q p")
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p q")] "q p"])
addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
#[branchGoal "inl" "p", branchGoal "inr" "q"])
addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
let state2parent ← serialize_expression_ast state2.parentExpr?.get! (sanitize := false)
-- This is due to delayed assignment
addTest $ LSpec.test "(2 parent)" (state2parent ==
"((:mv _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let state3_1parent ← serialize_expression_ast state3_1.parentExpr?.get! (sanitize := false)
addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))")
addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check " assumption" state4_1.goals.isEmpty
let state4_1parent ← serialize_expression_ast state4_1.parentExpr?.get! (sanitize := false)
addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)")
addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1)
let state4_2 ← match ← state3_2.execute (goalId := 0) (tactic := "assumption") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check " assumption" state4_2.goals.isEmpty
addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone
-- Ensure the proof can continue from `state4_2`.
let state2b ← match state4_2.continue state2 with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0])
let state3_1 ← match ← state2b.execute (goalId := 0) (tactic := "apply Or.inr") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check " assumption" state4_1.goals.isEmpty
addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isSome
return ()
where
typeProp: Protocol.Expression := { pp? := .some "Prop" }
branchGoal (caseName varName: String): Protocol.Goal := {
userName? := .some caseName,
target := { pp? := .some "q p" },
vars := #[
{ userName := "p", type? := .some typeProp, isInaccessible? := .some false },
{ userName := "q", type? := .some typeProp, isInaccessible? := .some false },
{ userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true }
]
}
def suite: IO LSpec.TestSeq := do
let env: Lean.Environment ← Lean.importModules
(imports := #[{ module := "Init".toName, runtimeOnly := false}])
(opts := {})
(trustLevel := 1)
let tests := [
("Nat.add_comm", proof_nat_add_comm false),
("Nat.add_comm manual", proof_nat_add_comm true),
("Nat.add_comm delta", proof_delta_variable),
("arithmetic", proof_arith),
("Or.comm", proof_or_comm)
]
let tests ← tests.foldlM (fun acc tests => do
let (name, tests) := tests
let tests ← proofRunner env tests
return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
return LSpec.group "Proofs" tests
end Pantograph.Test.Proofs

88
Test/Serial.lean Normal file
View File

@ -0,0 +1,88 @@
import LSpec
import Pantograph.Serial
import Test.Common
import Lean
open Lean
namespace Pantograph.Test.Serial
open Pantograph
deriving instance Repr, DecidableEq for Protocol.BoundExpression
def test_name_to_ast: LSpec.TestSeq :=
let quote := "\""
let escape := "\\"
LSpec.test "a.b.1" (name_to_ast (Name.num (.str (.str .anonymous "a") "b") 1) = "a.b.1") ++
LSpec.test "seg.«a.b»" (name_to_ast (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}") ++
-- Pathological test case
LSpec.test s!"«̈{escape}{quote}»" (name_to_ast (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«{escape}{quote}»{quote}")
def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
let entries: List (Name × Protocol.BoundExpression) := [
("Nat.add_comm".toName, { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }),
("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "n.succ ≤ m")], target := "n ≤ m" })
]
let coreM: CoreM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
let env ← MonadEnv.getEnv
let expr := env.find? symbol |>.get! |>.type
let test := LSpec.check symbol.toString ((← type_expr_to_bound expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
runCoreMSeq env coreM
def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
let entries: List (String × String) := [
-- This one contains unhygienic variable names which must be suppressed
("Nat.add", "(:forall _ (:c Nat) (:forall _ (:c Nat) (:c Nat)))"),
-- These ones are normal and easy
("Nat.add_one", "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"),
("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"),
-- Handling of higher order types
("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
]
let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
let env ← MonadEnv.getEnv
let expr := env.find? symbol.toName |>.get! |>.type
let test := LSpec.check symbol ((← serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
runMetaMSeq env metaM
def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
let entries: List (String × String) := [
("λ x: Nat × Bool => x.1", "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))")
]
let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
let env ← MonadEnv.getEnv
let s := syntax_from_str env source |>.toOption |>.get!
let expr := (← syntax_to_expr s) |>.toOption |>.get!
let test := LSpec.check source ((← serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
let metaM := termElabM.run' (ctx := defaultTermElabMContext)
runMetaMSeq env metaM
-- Instance parsing
def test_instance (env: Environment): IO LSpec.TestSeq := do
let metaM: MetaM LSpec.TestSeq := do
let env ← MonadEnv.getEnv
let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y"
let s := syntax_from_str env source |>.toOption |>.get!
let _expr := (← runTermElabMInMeta <| syntax_to_expr s) |>.toOption |>.get!
return LSpec.TestSeq.done
runMetaMSeq env metaM
def suite: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
return LSpec.group "Serialization" $
(LSpec.group "name_to_ast" test_name_to_ast) ++
(LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
(LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env)) ++
(LSpec.group "Sexp from expr" (← test_sexp_of_expr env)) ++
(LSpec.group "Instance" (← test_instance env))
end Pantograph.Test.Serial

73
doc/icon.svg Normal file
View File

@ -0,0 +1,73 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!-- Created with Inkscape (http://www.inkscape.org/) -->
<svg
width="256"
height="256"
viewBox="0 0 55.900957 55.900957"
version="1.1"
id="svg21534"
xml:space="preserve"
inkscape:version="1.2.2 (b0a8486541, 2022-12-01)"
sodipodi:docname="icon.svg"
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
xmlns="http://www.w3.org/2000/svg"
xmlns:svg="http://www.w3.org/2000/svg"><sodipodi:namedview
id="namedview21536"
pagecolor="#ffffff"
bordercolor="#111111"
borderopacity="1"
inkscape:showpageshadow="0"
inkscape:pageopacity="0"
inkscape:pagecheckerboard="1"
inkscape:deskcolor="#d1d1d1"
inkscape:document-units="px"
showgrid="true"
inkscape:zoom="5.1754899"
inkscape:cx="158.82554"
inkscape:cy="91.682142"
inkscape:window-width="3777"
inkscape:window-height="2093"
inkscape:window-x="0"
inkscape:window-y="0"
inkscape:window-maximized="1"
inkscape:current-layer="layer1"><inkscape:grid
type="xygrid"
id="grid23833"
spacingx="3.4938098"
spacingy="3.4938098"
empspacing="4" /></sodipodi:namedview><defs
id="defs21531" /><g
inkscape:label="Layer 1"
inkscape:groupmode="layer"
id="layer1"><rect
style="fill:#3e3e3e;fill-opacity:1;fill-rule:evenodd;stroke:none;stroke-width:1.78013;stroke-miterlimit:3.4;stroke-dasharray:none"
id="rect26805"
width="11.502316"
height="2.2512667"
x="33.344425"
y="7.6690259"
ry="0.28140834"
rx="0.47926313" /><path
style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
d="m 35.764667,9.9513013 c 0,0 -26.8581417,13.7987337 -28.0863506,14.9501437 -1.250042,1.171878 3.2347846,3.945325 3.2347846,3.945325 l 21.34979,14.934062 6.624567,0.453105 -27.599216,-17.304358 c 0,0 -0.603209,-0.08927 -0.600411,-0.762283 0.0028,-0.673015 27.32022,-16.4227356 27.32022,-16.4227356 z"
id="path27381"
sodipodi:nodetypes="csccccscc" /><path
style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
d="M 10.97848,26.985751 40.537772,9.7943227 41.921795,9.7005084 11.210626,27.421377 Z"
id="path27479" /><path
style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
d="m 7.0509847,25.522367 c -0.8266141,1.386819 -2.4011783,4.48805 -2.4706357,4.90223 -0.069458,0.414182 0.4434324,0.513474 0.8491061,0.757041 C 5.835129,31.425204 19.33424,43.917182 19.33424,43.917182 l 0.324562,-0.539228 c 0,0 -14.2055729,-12.369493 -14.0644435,-12.868167 0.1411292,-0.498672 3.544896,-3.777392 3.544896,-3.777392 L 7.4596884,25.117508 Z"
id="path27481" /><rect
style="fill:#3e3e3e;fill-opacity:1;fill-rule:evenodd;stroke:none;stroke-width:2.11692;stroke-miterlimit:3.4;stroke-dasharray:none;stroke-opacity:1"
id="rect27483"
width="36.38942"
height="3.6217353"
x="13.953447"
y="43.009739"
rx="0.43672624"
ry="0.43672624" /><path
style="fill:none;stroke:#000000;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
d="M -2.1119274,7.666599 H 64.179192"
id="path27487" /></g></svg>

After

Width:  |  Height:  |  Size: 3.5 KiB

238
flake.lock Normal file
View File

@ -0,0 +1,238 @@
{
"nodes": {
"flake-parts": {
"inputs": {
"nixpkgs-lib": "nixpkgs-lib"
},
"locked": {
"lastModified": 1709336216,
"narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=",
"owner": "hercules-ci",
"repo": "flake-parts",
"rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2",
"type": "github"
},
"original": {
"owner": "hercules-ci",
"repo": "flake-parts",
"type": "github"
}
},
"flake-utils": {
"locked": {
"lastModified": 1656928814,
"narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "flake-utils",
"type": "github"
}
},
"lean": {
"inputs": {
"flake-utils": "flake-utils",
"lean4-mode": "lean4-mode",
"nix": "nix",
"nixpkgs": "nixpkgs_2",
"nixpkgs-old": "nixpkgs-old"
},
"locked": {
"lastModified": 1711508550,
"narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=",
"owner": "leanprover",
"repo": "lean4",
"rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
"type": "github"
},
"original": {
"owner": "leanprover",
"ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
"repo": "lean4",
"type": "github"
}
},
"lean4-mode": {
"flake": false,
"locked": {
"lastModified": 1676498134,
"narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
"owner": "leanprover",
"repo": "lean4-mode",
"rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
"type": "github"
},
"original": {
"owner": "leanprover",
"repo": "lean4-mode",
"type": "github"
}
},
"lowdown-src": {
"flake": false,
"locked": {
"lastModified": 1633514407,
"narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
"owner": "kristapsdz",
"repo": "lowdown",
"rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
"type": "github"
},
"original": {
"owner": "kristapsdz",
"repo": "lowdown",
"type": "github"
}
},
"lspec": {
"flake": false,
"locked": {
"lastModified": 1701971219,
"narHash": "sha256-HYDRzkT2UaLDrqKNWesh9C4LJNt0JpW0u68wYVj4Byw=",
"owner": "lurk-lab",
"repo": "LSpec",
"rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
"type": "github"
},
"original": {
"owner": "lurk-lab",
"ref": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
"repo": "LSpec",
"type": "github"
}
},
"nix": {
"inputs": {
"lowdown-src": "lowdown-src",
"nixpkgs": "nixpkgs",
"nixpkgs-regression": "nixpkgs-regression"
},
"locked": {
"lastModified": 1657097207,
"narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
"owner": "NixOS",
"repo": "nix",
"rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nix",
"type": "github"
}
},
"nixpkgs": {
"locked": {
"lastModified": 1653988320,
"narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixos-22.05-small",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-lib": {
"locked": {
"dir": "lib",
"lastModified": 1709237383,
"narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8",
"type": "github"
},
"original": {
"dir": "lib",
"owner": "NixOS",
"ref": "nixos-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-old": {
"flake": false,
"locked": {
"lastModified": 1581379743,
"narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixos-19.03",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-regression": {
"locked": {
"lastModified": 1643052045,
"narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
"type": "github"
}
},
"nixpkgs_2": {
"locked": {
"lastModified": 1686089707,
"narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixpkgs-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs_3": {
"locked": {
"lastModified": 1711703276,
"narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=",
"owner": "nixos",
"repo": "nixpkgs",
"rev": "d8fe5e6c92d0d190646fb9f1056741a229980089",
"type": "github"
},
"original": {
"owner": "nixos",
"ref": "nixos-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"root": {
"inputs": {
"flake-parts": "flake-parts",
"lean": "lean",
"lspec": "lspec",
"nixpkgs": "nixpkgs_3"
}
}
},
"root": "root",
"version": 7
}

81
flake.nix Normal file
View File

@ -0,0 +1,81 @@
{
description = "Pantograph";
inputs = {
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
flake-parts.url = "github:hercules-ci/flake-parts";
lean = {
url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
# Do not follow input's nixpkgs since it could cause build failures
};
lspec = {
url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
flake = false;
};
};
outputs = inputs @ {
self,
nixpkgs,
flake-parts,
lean,
lspec,
...
} : flake-parts.lib.mkFlake { inherit inputs; } {
flake = {
};
systems = [
"x86_64-linux"
"x86_64-darwin"
];
perSystem = { system, pkgs, ... }: let
leanPkgs = lean.packages.${system};
lspecLib = leanPkgs.buildLeanPackage {
name = "LSpec";
roots = [ "Main" "LSpec" ];
src = "${lspec}";
};
project = leanPkgs.buildLeanPackage {
name = "Pantograph";
roots = [ "Main" "Pantograph" ];
src = pkgs.lib.cleanSourceWith {
src = ./.;
filter = path: type:
!(pkgs.lib.hasInfix "/Test/" path) &&
!(pkgs.lib.hasSuffix ".md" path) &&
!(pkgs.lib.hasSuffix "Makefile" path);
};
};
test = leanPkgs.buildLeanPackage {
name = "Test";
# NOTE: The src directory must be ./. since that is where the import
# root begins (e.g. `import Test.Environment` and not `import
# Environment`) and thats where `lakefile.lean` resides.
roots = [ "Test.Main" ];
deps = [ lspecLib project ];
src = pkgs.lib.cleanSourceWith {
src = ./.;
filter = path: type:
!(pkgs.lib.hasInfix "Pantograph" path);
};
};
in rec {
packages = {
inherit (leanPkgs) lean lean-all;
inherit (project) sharedLib executable;
default = project.executable;
};
checks = {
test = pkgs.runCommand "test" {
buildInputs = [ test.executable leanPkgs.lean-all ];
} ''
#export LEAN_SRC_PATH="${./.}"
${test.executable}/bin/test > $out
'';
};
devShells.default = pkgs.mkShell {
buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
};
};
};
}

14
lake-manifest.json Normal file
View File

@ -0,0 +1,14 @@
{"version": 7,
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/lurk-lab/LSpec.git",
"type": "git",
"subDir": null,
"rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
"name": "LSpec",
"manifestFile": "lake-manifest.json",
"inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
"inherited": false,
"configFile": "lakefile.lean"}],
"name": "pantograph",
"lakeDir": ".lake"}

View File

@ -1,19 +1,25 @@
import Lake import Lake
open Lake DSL open Lake DSL
package pantograph
package pantograph {
-- add package configuration options here
}
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @ "8e5a00a8afc8913c0584cb85f37951995275fd87"
lean_lib Pantograph { lean_lib Pantograph {
-- add library configuration options here defaultFacets := #[LeanLib.sharedFacet]
} }
@[default_target] @[default_target]
lean_exe pantograph { lean_exe pantograph {
root := `Main root := `Main
-- Somehow solves the native symbol not found problem
supportInterpreter := true
}
require LSpec from git
"https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
lean_lib Test {
}
lean_exe test {
root := `Test.Main
-- Somehow solves the native symbol not found problem
supportInterpreter := true
} }

View File

@ -1 +1 @@
leanprover/lean4:nightly-2023-05-06 leanprover/lean4:nightly-2024-03-27