Sebastian Ullrich
f9dcc9ca1b
fix: trim syntax in messages
2023-04-10 16:57:54 +02:00
Sebastian Ullrich
bafa4e0a78
feat: use with_trace for important trace classes
2023-04-10 16:57:54 +02:00
Sebastian Ullrich
d8e826c2a7
feat: trace.profiler
2023-04-10 16:57:54 +02:00
Sebastian Ullrich
d51e404d6a
refactor: move profiling options to Lean
2023-04-10 16:57:54 +02:00
Gabriel Ebner
742d053a97
fix: respect pp.raw in interactive .ofGoal
...
Fixes #2175
2023-03-30 17:19:35 -07:00
Sebastian Ullrich
b076d488e3
feat: show typeclass and tactic names in profile output
2023-03-27 17:47:52 +02:00
int-y1
9bc6fa1c6e
chore: fix typos
2023-03-27 10:05:50 +02:00
Gabriel Ebner
8650804b02
perf: cache tc results with mvars
2023-03-16 15:26:38 -07:00
Gabriel Ebner
d3c55ef249
perf: do not reset tc cache when adding local instances
2023-03-16 15:26:38 -07:00
Sebastian Ullrich
a62d412dce
fix: implement · tacs as a builtin elaborator, part 2
...
Fixes #2153
2023-03-15 17:00:15 +01:00
Sebastian Ullrich
9d144c73fd
fix: implement · tacs as a builtin elaborator
2023-03-15 13:59:16 +01:00
Sebastian Ullrich
a89accfbbe
feat: parser alias for tacticSeqIndentGt
2023-03-15 10:54:05 +01:00
Sebastian Ullrich
d7a0197fee
chore: improve tacticSeqIndentGt error message
2023-03-15 10:52:57 +01:00
Sebastian Ullrich
3d21124445
perf: scale Expr.replace cache with input size
2023-03-14 23:20:23 +01:00
Sebastian Ullrich
96aa021007
feat: add attribute application profile metric
2023-03-13 16:17:20 +01:00
Sebastian Ullrich
b15d7b8f17
feat: add kernel type checking profile metric
2023-03-13 16:17:20 +01:00
Sebastian Ullrich
a4f732e6b1
fix: ignore vanishing files during watchdog update
2023-03-10 19:13:24 +01:00
Sebastian Ullrich
aacab14394
chore: remove support for text-mode I/O
...
This didn't do anything except on Windows, where it would make the
application differ from standard Windows applications, which we don't
want.
2023-03-10 16:27:56 +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
Adrien Champion
473486eeb9
fix: calc indentation and allow underscore in first relation
2023-02-23 14:20:21 -08:00
Gabriel Ebner
adcca17991
chore: add option to enable structure eta in tc search
2023-02-21 16:41:30 -08: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
Gabriel Ebner
15a045ee66
fix: reenable structure eta during tc search
...
Fixes #2074 .
2023-02-05 11:41:00 -08: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
Gabriel Ebner
18b3bd7875
fix: calc: do not take lhs/rhs from expected type
...
Fixes #2073
2023-01-30 15:02:40 -08: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
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
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
Rishikesh Vaishnav
561e404fe4
feat: make go-to-definition on a typeclass projection application go to the instance(s) ( #1767 )
2023-01-19 09:10:01 +00:00
Rishikesh Vaishnav
600758ba49
fix: fuzzy-find bonus for matching last characters of pattern and symbol ( #1917 )
2023-01-19 09:06:53 +01:00
Sebastian Ullrich
43c5ab802f
fix: show tactic info on canonical by
2023-01-18 10:23:37 +01:00
Sebastian Ullrich
223f1073d1
chore: info tree format should not leak hygiene IDs
2023-01-16 08:33:58 -08:00
Sebastian Ullrich
d59f5c2ffa
fix: binop% info tree
2023-01-16 08:33:58 -08:00
