Commit Graph

191 Commits

Author SHA1 Message Date
Leni Aniva 2d422dc532 Merge pull request 'fix: Instantiation causes infinite loop' (#54) from output/expr into dev
Reviewed-on: #54
2024-03-31 16:43:53 -07:00
Leni Aniva 6235d61433
fix: unfoldAuxLemma should be coreM 2024-03-31 15:40:14 -07:00
Leni Aniva e13b119ed1
fix: Instantiation causes infinite loop 2024-03-30 00:17:16 -07:00
Leni Aniva 0c260addcf Merge pull request 'feat: Instantiation tests' (#52) from io/serial into dev
Reviewed-on: #52
2024-03-30 00:08:32 -07:00
Leni Aniva 90f7f251e9
Merge branch 'dev' into io/serial 2024-03-30 00:07:46 -07:00
Leni Aniva ff8a462bcd Merge pull request 'fix: Build failure on macOS due to LLVM version' (#53) from misc/toolchain into dev
Reviewed-on: #53
2024-03-30 00:07:26 -07:00
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 bc83a5732e
feat: Instantiation tests
Note that delay assigned metavariables are not instantiated.
2024-03-29 23:46:08 -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