Gabriel Ebner
|
0656482b91
|
feat: show number of files to go when building
|
2023-04-18 20:58:40 -04:00 |
|
Gabriel Ebner
|
312960820c
|
feat: priority for bindSync
|
2023-04-18 20:58:40 -04:00 |
|
Gabriel Ebner
|
98a55105ff
|
chore: update Lean version
|
2023-04-18 20:58:40 -04:00 |
|
Gabriel Ebner
|
a1a30aac1c
|
refactor: simplify recBuildLeanCore
|
2023-04-18 20:58:40 -04:00 |
|
tydeu
|
c49a7d84e9
|
chore: fix test
|
2023-04-15 21:04:46 -04:00 |
|
tydeu
|
346da2c29c
|
feat: bare lake run default scripts
|
2023-04-15 20:07:47 -04:00 |
|
tydeu
|
227a350747
|
doc: tweak README + fix some typos
|
2023-04-15 18:32:21 -04:00 |
|
Gabriel Ebner
|
caa4494cb7
|
chore: remove dangerous instances
|
2023-04-15 18:16:53 -04:00 |
|
Scott Morrison
|
a45f808da4
|
chore: don't rely on simp calling decide (leanprover/lake#168)
|
2023-03-28 12:32:39 -04:00 |
|
Sebastian Ullrich
|
7648ec57b5
|
fix: adapt to new Handle.mk signature
The previous code was arguably wrong in any case as the result of `lake
init` should not depend on the current platform
|
2023-03-17 09:15:26 -04:00 |
|
Gabriel Ebner
|
620587fc42
|
feat: make lake clean clean all packages
Fixes leanprover/lake#155
|
2023-03-10 22:51:11 -05:00 |
|
Gabriel Ebner
|
57fea2d8e3
|
feat: accept empty git hash as version
Fixes leanprover/lake#154
|
2023-03-10 22:49:36 -05:00 |
|
Gabriel Ebner
|
276bf837e2
|
feat: show stdout by default
|
2023-03-10 22:48:35 -05:00 |
|
Kaiyu Yang
|
421e73f6c5
|
doc: fix typo in README (leanprover/lake#157)
|
2023-02-24 16:02:00 -05:00 |
|
Martin Dvořák
|
83dffbc2f8
|
doc: mention lake clean in README (leanprover/lake#156)
|
2023-02-23 12:14:17 -05:00 |
|
tydeu
|
16af1dddf4
|
fix: include link args in shared lib trace of extern lib
|
2023-02-21 06:35:39 -05:00 |
|
tydeu
|
5080b08922
|
chore: reduce imports in Lake.Build.Actions
|
2023-02-02 20:38:06 -05:00 |
|
Arthur Paulino
|
05c2ac5f3c
|
download lean-toolchain directly
|
2023-02-02 20:34:02 -05:00 |
|
tydeu
|
7055f953f1
|
doc: fix typo
closes leanprover/lake#151
|
2023-02-02 15:40:02 -05:00 |
|
tydeu
|
e1887fa510
|
fix: put FFI lib in pkg lib dir in example (for Linux)
|
2023-01-11 18:24:15 -05:00 |
|
tydeu
|
55fa486ce6
|
fix: packages dir path and repo url
|
2023-01-11 18:18:09 -05:00 |
|
tydeu
|
15d656bd9a
|
fix: Linux still needs augmented library path
|
2023-01-11 17:32:26 -05:00 |
|
tydeu
|
4f505cd056
|
fix: use full path when loading dynlibs in the server
closes leanprover/lake#146
|
2023-01-11 16:17:47 -05:00 |
|
tydeu
|
8c793eaae5
|
chore: bump Lean version
|
2023-01-11 15:11:26 -05:00 |
|
Gabriel Ebner
|
cee959078d
|
fix: do not require Environment to be inhabited
|
2023-01-11 15:01:45 -05:00 |
|
tydeu
|
148b067724
|
test: fix shell script permissions
|
2022-12-02 17:58:51 -05:00 |
|
tydeu
|
479fe81894
|
feat: print log on failing lake print-paths
closes leanprover/lake#116
|
2022-12-02 17:26:36 -05:00 |
|
Gabriel Ebner
|
47b4eae9a6
|
perf: use ByteArray.hash directly
|
2022-12-02 14:31:48 -05:00 |
|
tydeu
|
c60ccdc974
|
test: increase sleep in 44
|
2022-12-02 14:20:58 -05:00 |
|
tydeu
|
25ab266a2e
|
fix: escape names from new/init
closes leanprover/lake#128
|
2022-12-02 14:17:57 -05:00 |
|
tydeu
|
b8c4ed5a83
|
feat: -U to update & build; add packagesDir to manifest
|
2022-12-02 14:17:57 -05:00 |
|
tydeu
|
93f1d05e2a
|
fix: various build problems
fixes leanprover/lake#139
touches on leanprover/lake#132
|
2022-12-02 14:17:56 -05:00 |
|
tydeu
|
b813197b36
|
chore: cleanup
|
2022-12-02 14:17:56 -05:00 |
|
Gabriel Ebner
|
b76bfcac91
|
fix: do not rely on iteration order of NameSet
|
2022-12-02 14:11:12 -05:00 |
|
Gabriel Ebner
|
7603e49169
|
chore: bump Lean version
|
2022-12-02 14:06:15 -05:00 |
|
Leonardo de Moura
|
8fbb866798
|
fix: incorrect use of outParam
We have
```
class BindAsync (n : Type u → Type v) (k : outParam $ Type u → Type u)
instance : BindAsync BaseIO (EIOTask ε)
instance : BindAsync BaseIO OptionIOTask
instance [BindAsync n k] [Pure n] [Pure k] : BindAsync n (ExceptT ε k)
instance [BindAsync n k] [Pure n] [Pure k] : BindAsync n (OptionT k)
```
See discussion at: https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-maintainers/topic/Increasing.20.60Expr.2Ehash.60.20to.2064.20bits/near/313183466
|
2022-11-30 16:56:09 -08:00 |
|
Leonardo de Moura
|
dc937cb1f9
|
chore: Name.append
|
2022-11-29 23:05:19 -08:00 |
|
Gabriel Ebner
|
733f015c65
|
chore: reduce imports
|
2022-11-23 20:56:40 -05:00 |
|
Gabriel Ebner
|
42a8e0f190
|
refactor: split code for lake update and lake build
|
2022-11-23 20:56:40 -05:00 |
|
Gabriel Ebner
|
1949285fdb
|
chore: disable parallel testing in ci
|
2022-11-23 20:56:40 -05:00 |
|
Gabriel Ebner
|
2808cc2744
|
feat: improve manifest test
|
2022-11-23 20:56:40 -05:00 |
|
Gabriel Ebner
|
031d9712d5
|
chore: simplify test/manifest/test.sh
|
2022-11-23 20:56:40 -05:00 |
|
Gabriel Ebner
|
716fe7abb8
|
perf: use parseImports'
|
2022-11-11 13:21:42 -05:00 |
|
Gabriel Ebner
|
c614ffa2f7
|
chore: bump Lean version
|
2022-11-11 13:21:42 -05:00 |
|
tydeu
|
837eec5d9a
|
feat: add buildO helper
closes leanprover/lake#126
|
2022-11-10 20:48:05 -05:00 |
|
tydeu
|
8e6abd7c56
|
doc: add --old to lake help
|
2022-11-10 20:48:05 -05:00 |
|
tydeu
|
ddd7581ee4
|
refactor: lean_packages -> lake-packages + cleanup
|
2022-11-10 20:48:04 -05:00 |
|
tydeu
|
855a655033
|
refactor: split actions requiring load into separate file
see 1bd8430c15 (r82430947)
|
2022-11-10 20:48:03 -05:00 |
|
tydeu
|
0bf59a5921
|
feat: library defaultFacets setting
closes leanprover/lake#117
|
2022-11-10 20:48:02 -05:00 |
|
tydeu
|
d3d526d43f
|
test: make FFI example builds verbose
|
2022-11-10 20:46:57 -05:00 |
|