Sebastian Ullrich
|
db2e710072
|
chore: Nix: update lean4-mode
|
2023-03-15 10:52:03 +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
|
4cc6057f4a
|
chore: ensure consistent (Unix) encoding for source files
|
2023-03-10 16:27:56 +01:00 |
|
Sebastian Ullrich
|
15c146b382
|
feat: proper I/O errors from getLine
|
2023-03-10 16:27:56 +01:00 |
|
Sebastian Ullrich
|
51e77d152c
|
fix: do not inherit file handles across process creation
|
2023-03-10 16:27:56 +01:00 |
|
Sebastian Ullrich
|
113de7cca1
|
refactor: move from fopen to open
|
2023-03-10 16:27:56 +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 |
|
int-y1
|
0477276f66
|
chore: fix typos in prelude
|
2023-03-09 18:12:24 +01:00 |
|
Adrien Champion
|
ce0d2a6928
|
chore: formatting/capitalization in RELEASES.md
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
|
2023-03-09 18:11:11 +01:00 |
|
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 |
|