Gabriel Ebner
412691c958
feat: support LEAN_NUM_THREADS environment variable
2021-12-21 17:01:08 +01:00
Sebastian Ullrich
b732484663
fix: do not consider worker threads as idle during startup
...
Without this change, enqueuing multiple tasks before the first worker
was started led to only a single worker being created. Now the first
increment and decrement happen under the task manager mutex, so
effectively the worker is never idle until it is out of tasks.
2021-12-21 12:01:23 +01:00
Leonardo de Moura
b278a20ac2
feat: ensure #eval converts unassigned universe metavars into parameters
...
see #898
2021-12-20 06:11:36 -08:00
Sebastian Ullrich
51dc32957b
feat: show universe args on hover
...
We might also want to replace them with fresh vars to make the hover
completely independent of the context, but this change at least avoids
any hidden information.
2021-12-20 10:51:44 +01:00
Sebastian Ullrich
6f9c6e4556
doc: match: mention (generalizing := true)
2021-12-19 11:14:27 +01:00
Sebastian Ullrich
5f96a9fc4d
fix: do not show type of sort in hover
...
Fixes #896
2021-12-19 11:03:15 +01:00
tydeu
f4a73889e7
feat: expose more version info (e..g., toolchain)
2021-12-19 10:44:35 +01:00
Sebastian Ullrich
167dccce0b
chore: move Leanpkg.leanVersionString to Init
2021-12-18 10:59:37 -08:00
Sebastian Ullrich
234d806f6b
chore: deprecate leanpkg
2021-12-18 10:59:37 -08:00
Mario Carneiro
f22f699d62
feat: split replicate / replicateTR with @[csimp]
2021-12-18 10:58:57 -08:00
Leonardo de Moura
be6bc67eb0
fix: ensure match-expressions compiled using if-then-else can be reduced with TransparencyMode.reducible
...
closes #891
2021-12-18 10:55:42 -08:00
Leonardo de Moura
b3d8766b09
chore: use doubleticks at WHNF.lean
2021-12-18 08:43:50 -08:00
Leonardo de Moura
b6fbdd8679
feat: add Meta.Context.canUnfold?
2021-12-18 08:25:56 -08:00
Leonardo de Moura
c954fc9ec7
fix: bug at simpLoop
2021-12-18 06:48:08 -08:00
Sebastian Ullrich
cd94ec20b0
fix: aux_def: avoid creating unparseable names
2021-12-17 14:21:35 -08:00
Mario Carneiro
51a78fd7af
fix: change argument order of List.get[!?D]
2021-12-17 14:21:00 -08:00
Mario Carneiro
caf09e85ad
chore: universe generalize implies_true
2021-12-17 14:19:54 -08:00
Leonardo de Moura
dce55f79ed
feat: eliminate recursive application syntax annotation at addAndCompileUnsafe
2021-12-17 07:24:44 -08:00
Leonardo de Moura
7df9cf6a0a
feat: eliminate "recAppSyntax" information during structural recursion
2021-12-17 07:15:14 -08:00
Leonardo de Moura
6b82e15069
feat: preserve variable names when packing domain
2021-12-17 07:10:26 -08:00
Leonardo de Moura
8b7411bdd8
feat: improve error location at well-founded recursion
2021-12-17 06:50:20 -08:00
Sebastian Ullrich
9e5ff3db0e
feat: setMainModule in worker
2021-12-17 12:22:53 +01:00
Sebastian Ullrich
51adfa2e0c
fix: do not call lake print-paths for lakefile.lean
...
Fixes #873
2021-12-17 12:22:30 +01:00
tydeu
e34c892f89
chore: update Lake
2021-12-17 10:20:37 +01:00
Leonardo de Moura
2d4d5ae96f
feat: save syntax around recursive applications
...
Motivation: better error messages at structural and well-founded recursion.
2021-12-16 17:13:55 -08:00
Leonardo de Moura
e38fab1b4e
fix: ignore Expr.MData at deltaRHS?
2021-12-16 16:58:10 -08:00
Leonardo de Moura
de29657594
feat: implement bool operator==(data_value const & a, data_value const & b) using Lean autogenerated code
2021-12-16 16:37:47 -08:00
Leonardo de Moura
867134614b
feat: add constructor DataValue.ofSyntax
2021-12-16 15:41:29 -08:00
Gabriel Ebner
e65f3fe810
fix: use redirected stderr for tout()
2021-12-16 10:23:05 -08:00
Sebastian Ullrich
1221bdd3c7
fix: use redirected stderr for timeit & allocprof
2021-12-16 06:38:35 -08:00
Sebastian Ullrich
87e860f871
perf: Array.push: move elements directly when source is unique
2021-12-16 06:37:37 -08:00
tydeu
72cfe18e9f
chore: update Lake
2021-12-16 11:10:33 +01:00
Joe Hendrix
5a307a93ac
fix: bug at ByteArray.copySlice
2021-12-16 11:05:19 +01:00
Leonardo de Moura
81f7335269
fix: ensure motive is type correct at simpProj
2021-12-15 17:07:31 -08:00
Leonardo de Moura
0a81093db5
fix: bug at simpProj
...
This bug was reported at https://github.com/dwrensha/lean4-maze/issues/1
2021-12-15 17:07:00 -08:00
Leonardo de Moura
9a24db4e86
fix: check generated motives at ▸ notation
...
This commit also improves the `▸` notation a bit.
It now tries `subst` (if applicable) before failing.
2021-12-15 16:16:42 -08:00
Leonardo de Moura
89edc184fb
feat: compleation at #print command
2021-12-15 13:13:39 -08:00
Leonardo de Moura
653b684651
feat: improve getCompletionKindForDecl
2021-12-15 12:57:09 -08:00
Leonardo de Moura
7d7c6d8be5
feat: add CompletionItemKind
2021-12-15 11:24:11 -08:00
Leonardo de Moura
31f845c5ed
feat: keyword completion
2021-12-15 11:24:11 -08:00
Leonardo de Moura
043e9c80b4
feat: add Trie.findPrefix
2021-12-15 11:24:11 -08:00
Sebastian Ullrich
ba83721109
chore: add comment for previous fix
2021-12-15 20:10:48 +01:00
Sebastian Ullrich
c8c39aa4bb
chore: lean-gdb: fix RC printing
2021-12-15 15:58:31 +01:00
Sebastian Ullrich
3c9ea3b113
fix: wait on tasks before Lean program exit
2021-12-15 15:58:24 +01:00
larsk21
efa2ded224
chore: bump server version to 0.1.1
2021-12-15 13:00:05 +01:00
larsk21
d50c08360d
feat: change error flag to progress kind in LeanFileProgressProcessingInfo
2021-12-15 13:00:05 +01:00
larsk21
dcbc526115
feat: report header processing errors as error progress
2021-12-15 13:00:05 +01:00
larsk21
925c530673
feat: add error field to LeanFileProgressProcessingInfo
2021-12-15 13:00:05 +01:00
Gabriel Ebner
230d6d2cf5
fix: use group for if-then-else
2021-12-15 11:42:38 +00:00
Gabriel Ebner
d6f629860b
feat: add ppRealFill and ppRealGroup combinators
2021-12-15 11:42:38 +00:00
