tydeu
|
94c48d2d29
|
refactor: cleanup runFrontend
|
2022-05-25 16:52:41 -04:00 |
|
Gabriel Ebner
|
b50f80c393
|
perf: cache imported environment
|
2022-05-25 13:13:38 -04:00 |
|
tydeu
|
55a2395db5
|
feat: retool configure into update
closes leanprover/lake#69
|
2022-05-24 13:57:30 -04:00 |
|
tydeu
|
85e3385aaa
|
feat: only update deps in configure + don't ignore manifest.json
closes leanprover/lake#59, leanprover/lake#63
|
2022-05-23 20:38:54 -04:00 |
|
tydeu
|
c1b4074d54
|
fix: only write manifest if a package was resolved
|
2022-05-23 20:28:36 -04:00 |
|
tydeu
|
e8d59a7a6e
|
feat: save resolved packages in a manifest
closes leanprover/lake#31
|
2022-05-23 19:47:29 -04:00 |
|
tydeu
|
10c444e5ef
|
fix: include moreLeanArgs in module trace
closes leanprover/lake#50
|
2022-05-19 14:28:00 -04:00 |
|
tydeu
|
e24d6f1181
|
fix: include Lean version in binary trace
closes leanprover/lake#62
|
2022-05-19 11:34:01 -04:00 |
|
tydeu
|
9f333147f5
|
chore: start next Lake version
|
2022-05-16 11:28:12 -04:00 |
|
tydeu
|
7a499ee09b
|
release: 3.0.1
|
2022-05-16 11:18:32 -04:00 |
|
tydeu
|
c03b388d6f
|
chore: bump Lean version
|
2022-05-16 11:12:49 -04:00 |
|
Gabriel Ebner
|
a28c1da704
|
fix: do not call git checkout unless necessary
See leanprover/lake#63.
|
2022-05-15 16:13:14 -04:00 |
|
Gabriel Ebner
|
be570305fc
|
perf: do not resolve full git object names
|
2022-05-15 16:13:14 -04:00 |
|
Gabriel Ebner
|
712b22b46f
|
perf: do not import Lean.Elab.Frontend from Lake
|
2022-05-15 15:56:50 -04:00 |
|
tydeu
|
0fe9930d67
|
chore: update Lean version
|
2022-03-21 09:16:12 -04:00 |
|
Leonardo de Moura
|
2a4684a9ae
|
chore: String.Pos is opaque now
See https://github.com/leanprover/lean4/issues/410
Remark: I did not try to fix the places where the code assumes all
characters have size 1. I marked them with `TODO`s
|
2022-03-21 09:14:54 -04:00 |
|
Sebastian Ullrich
|
bdd5185a7f
|
fix: serve + print-paths without lakefile
|
2022-03-21 08:51:59 -04:00 |
|
Sebastian Ullrich
|
65d00098c7
|
chore: fix List.get use (leanprover/lake#56)
|
2022-02-16 13:21:33 -05:00 |
|
Gabriel Ebner
|
926a253680
|
fix: serve: fall back to lean --server on error
|
2022-02-04 17:30:47 -05:00 |
|
Leonardo de Moura
|
8c40a31573
|
chore: auto pure was removed
|
2022-02-03 21:32:27 -05:00 |
|
tydeu
|
0869780376
|
chore: start next Lake version
|
2022-02-03 01:24:28 -05:00 |
|
tydeu
|
17ac0d7f94
|
release: 3.0.0
|
2022-01-31 06:51:57 -05:00 |
|
tydeu
|
a9793b0a50
|
feat: add root package to workspace + and use it
|
2022-01-31 02:24:11 -05:00 |
|
tydeu
|
1c4b5ff3ac
|
test: add package dependency diamond in deps example
|
2022-01-31 00:52:57 -05:00 |
|
tydeu
|
985bdcb4d0
|
fix: don't duplicate dep link targets in diamonds
closes leanprover/lake#43
|
2022-01-31 00:52:37 -05:00 |
|
tydeu
|
30e3f10c6c
|
chore: ilean code cleanup
|
2022-01-31 00:04:17 -05:00 |
|
Sebastian Ullrich
|
e6894c058b
|
feat: create .ilean files
|
2022-01-30 23:46:08 -05:00 |
|
tydeu
|
bffcfde602
|
refactor: ModuleInfo -> Module
|
2022-01-30 23:16:08 -05:00 |
|
tydeu
|
705962847d
|
fix: glob bugs + cleanup
closes leanprover/lake#42
|
2022-01-30 22:49:05 -05:00 |
|
Sebastian Ullrich
|
df1c1cde12
|
refactor: make LeanPaths usage forward-compatible (leanprover/lake#48)
|
2022-01-22 20:55:16 -05:00 |
|
tydeu
|
6d7fc7216c
|
fix: get pkg for dep name not mod at buildDepOleans
Bug & fix first reported on Zulip: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lake.20mathport.20panic
|
2022-01-18 19:56:23 -05:00 |
|
tydeu
|
2be2466f78
|
chore: bump Lean version
|
2022-01-17 15:00:01 -05:00 |
|
Leonardo de Moura
|
4ac34f4cd5
|
chore: rename PointedType => NonemptyType
|
2022-01-15 11:42:09 -08:00 |
|
tydeu
|
f3d8fcc85d
|
test: don't check for lean-toolchain generation in init example
|
2022-01-15 11:35:40 -05:00 |
|
Leonardo de Moura
|
e880dd52a4
|
chore: PointedType
|
2022-01-14 20:41:47 -08:00 |
|
tydeu
|
752bc24f78
|
feat: add args to binary & .o file traces + some cleanup
closes leanprover/lake#41
|
2021-12-27 12:07:15 -05:00 |
|
tydeu
|
2680e1c66f
|
refactor: generalize computeHash + cleanup
|
2021-12-27 12:00:09 -05:00 |
|
tydeu
|
5029f30b27
|
refactor: tweak collectArgs in Cli
|
2021-12-27 11:00:18 -05:00 |
|
tydeu
|
5102d21cc5
|
feat: expand script CLI into its own script command
|
2021-12-24 03:26:34 -05:00 |
|
tydeu
|
2b0989ea28
|
refactor:: simplify/improve CLI API
|
2021-12-23 23:43:01 -05:00 |
|
tydeu
|
c9128d1ce6
|
refactor:: separate build and scheduler monads
|
2021-12-23 16:25:15 -05:00 |
|
tydeu
|
d4e7e33652
|
feat: split Lake context from BuildContext and also use it in scripts
|
2021-12-22 00:39:36 -05:00 |
|
tydeu
|
1b96c466ca
|
refactor: use new version info from Lean + cleanup
|
2021-12-19 21:59:17 -05:00 |
|
tydeu
|
9ac989f0c9
|
chore: bump Lean version
|
2021-12-19 21:47:46 -05:00 |
|
tydeu
|
adcf2df9b5
|
refactor: async API tweaks
|
2021-12-19 21:45:42 -05:00 |
|
tydeu
|
8fb9dd8478
|
fix: consider globbed files local
easiest way to fix mathport builds (for now)
|
2021-12-16 21:56:10 -05:00 |
|
tydeu
|
34bf090300
|
fix: build dep's extraDepTarget not root's for each dep
|
2021-12-16 01:03:21 -05:00 |
|
tydeu
|
d781c3411a
|
feat: add getLeanSysroot and getLeanLibDir
|
2021-12-15 20:08:14 -05:00 |
|
tydeu
|
f9e789af45
|
refactir: revamp install path API
|
2021-12-15 13:44:28 -05:00 |
|
tydeu
|
a23c5feec4
|
chore: bump Lean version
|
2021-12-15 11:14:02 -05:00 |
|