Adrien Champion
5111595753
chore: discuss alternative calc syntax in RELEASES.md
2023-03-09 18:11:11 +01:00
Sebastian Ullrich
8509a28798
feat: profile tactic execution
2023-03-09 17:18:19 +01:00
Gabriel Ebner
0cc9d7a43d
fix: do not reverse subgoals of local instances
2023-03-08 15:54:07 -08:00
Gabriel Ebner
2262579f9b
fix: tc: filter out assigned subgoals at the correct place
2023-03-08 15:54:07 -08:00
Gabriel Ebner
3ab859553e
fix: allow function coercion to assign universe mvars
2023-03-08 15:54:07 -08:00
Gabriel Ebner
1c641b569a
chore: synthInstance trace message on cache hit
2023-03-08 15:54:07 -08:00
Gabriel Ebner
1f61633da7
fix: typo in trace class name
2023-03-08 15:54:07 -08:00
Gabriel Ebner
e6b3202df3
chore: remove dead code
2023-03-08 15:54:07 -08:00
Sebastian Ullrich
d4caf1f922
fix: $_* anonymous suffix splice syntax pattern
2023-03-06 16:30:18 +01:00
Martin Dvořák
3b50410ec0
doc: typo
2023-03-04 11:19:25 +01:00
Gabriel Ebner
0da281fab4
fix: reject occurrences of inductive type in index
...
Fixes #2125
2023-02-28 12:22:54 -08:00
Adrien Champion
473486eeb9
fix: calc indentation and allow underscore in first relation
2023-02-23 14:20:21 -08:00
Sebastian Ullrich
3f6c5f17db
fix: unhygiene in expandExplicitBinders
2023-02-22 17:07:31 +01:00
Gabriel Ebner
7992ce6b4d
chore: add test for calc
2023-02-21 16:41:46 -08:00
Gabriel Ebner
adcca17991
chore: add option to enable structure eta in tc search
2023-02-21 16:41:30 -08:00
Sebastian Ullrich
c826168cfa
fix: atomic --profile output for xargs -P
2023-02-11 17:41:07 +01:00
Sebastian Ullrich
3146aa477d
fix: accumulate_profile: accept category names containing digits (e.g. hygiened decl names)
2023-02-11 17:41:07 +01:00
Gabriel Ebner
75252d2b85
perf: whnf projections during defeq
2023-02-09 19:54:23 -08:00
Gabriel Ebner
ecc74c5a9d
fix: defeq condition for projections
2023-02-09 19:54:23 -08:00
Gabriel Ebner
448f49ee91
Revert "fix: reenable structure eta during tc search"
...
The fix is blocked by slow defeq checks for TC instances; see issues
1986 and 2055. Enabling it right now causes lots of timeouts in
mathlib4.
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/bump.20to.202023-02-06/near/326223768
This reverts commit 15a045ee66
2023-02-09 11:37:30 -08:00
Gabriel Ebner
3c562c1a9b
fix: unify goal before executing nested tactics in calc
...
Fixes #2095
2023-02-09 11:34:07 -08:00
Jon Eugster
07bd2a8488
feat: add quot_precheck Lean.Parser.Term.explicit
2023-02-08 12:21:40 +01:00
Sebastian Ullrich
9d013ba3f5
chore: update stage0
2023-02-08 12:11:41 +01:00
Gabriel Ebner
15a045ee66
fix: reenable structure eta during tc search
...
Fixes #2074 .
2023-02-05 11:41:00 -08:00
tydeu
4b974fd60b
chore: update Lake
2023-02-03 22:10:15 +01:00
Gabriel Ebner
d4b9a532d2
fix: calc: synthesize default instances
...
This is necessary to figure out the types with exponentiations.
Fixes #2079
2023-02-02 14:29:21 -08:00
Gabriel Ebner
8265d8bb13
chore: calc: improve error range
2023-02-02 14:21:06 -08:00
Leonardo de Moura
35ccf7b163
chore: update CONTRIBUTING.md
2023-02-01 12:07:15 -08:00
Sebastian Ullrich
7327b66179
doc: update FPiL entry in README
...
/cc @david-christiansen
I think it's progressed far enough that no "in development" annotation is necessary on this page
2023-01-31 08:10:44 -08:00
Gabriel Ebner
18b3bd7875
fix: calc: do not take lhs/rhs from expected type
...
Fixes #2073
2023-01-30 15:02:40 -08:00
tydeu
38a0d1e373
chore: update Lake
2023-01-28 18:29:00 +01:00
int-y1
b69fcbc28f
chore: fix typos
2023-01-28 15:15:12 +01:00
Gabriel Ebner
e37f209c1a
fix: unify types in calc
2023-01-27 13:38:42 -08:00
Gabriel Ebner
dd8319c3cd
fix: disable gmp on windows
...
The msys2 gmp package does not support static linking at the moment.
f31bdf893a
2023-01-27 12:28:34 -08:00
Leonardo de Moura
decb08858f
fix: kernel must ensure that safe functions cannot use partial ones.
...
Fix issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Meaning.20of.20.60DefinitionSafety.2Epartial.60
2023-01-27 12:17:37 -08:00
Sebastian Ullrich
1f41b91206
test: update Lean variant benchmarks
2023-01-26 13:33:28 +01:00
Sebastian Ullrich
2a7ae7b28a
chore: Nix: explicit src
2023-01-26 13:32:42 +01:00
Sebastian Ullrich
12356b739b
test: add rbmap_2 benchmark
2023-01-26 13:32:42 +01:00
Sebastian Ullrich
d01a521be2
test: fix
2023-01-26 13:31:16 +01:00
Sebastian Ullrich
badfcdc49f
fix: missing info tree on elab failure
2023-01-26 13:05:57 +01:00
Sebastian Ullrich
f24608c4d1
fix: make eoi an actual command with info tree
2023-01-26 13:05:57 +01:00
Sebastian Ullrich
8a4059dc65
fix: avoid notation in quotation elaborator output
2023-01-26 13:05:33 +01:00
Sebastian Ullrich
18297d8d91
fix: notation unexpander on overapplication of non-nullary notation
2023-01-26 13:05:33 +01:00
Sebastian Ullrich
94547b3d85
chore: CI: avoid deprecated set-output
2023-01-25 10:23:22 +01:00
Gabriel Ebner
f4d005e86d
chore: only build small allocator if enabled
...
This prevents us from calling alloc/dealloc if LEAN_SMALL_ALLOCATOR is
disabled.
2023-01-24 11:37:43 -08:00
Gabriel Ebner
3deef5d32a
fix: mpz: honor LEAN_SMALL_ALLOCATOR
2023-01-24 11:37:43 -08:00
Gabriel Ebner
345aa6f835
chore: put throws in separate function for debugger
2023-01-23 09:27:09 -08:00
Gabriel Ebner
34777c9b90
fix: catch missing exceptions in kernel
2023-01-23 09:27:09 -08:00
Evgenia Karunus
a125a36bcc
doc: Expr docs fix ( #2047 )
...
```
open Lean Meta
-- Docs text:
-- The let-expression `let x : Nat := 2; Nat.succ x` is represented as
def old : Expr :=
Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.bvar 0) true
elab "old" : term => return old
#check old -- let x := 2; x : Nat
#reduce old -- 2
def new : Expr :=
Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.app (.const `Nat.succ []) (.bvar 0)) true
elab "new" : term => return new
#check new -- let x := 2; Nat.succ x : Nat
#reduce new -- 3
```
2023-01-20 09:51:55 +01:00
Sebastian Ullrich
cbdd76f6b6
test: retire .perf benchmarks, cache misses are not very enlightening
2023-01-19 14:44:20 +01:00
