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
|
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
|
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 |