Leonardo de Moura
ebcab266c6
chore: remove empty line
2023-05-05 12:18:36 -07:00
Henrik Böving
0e042d8ef6
fix: LCNF simp forgot to mark normalized decls as simplified
2023-05-05 12:17:26 -07:00
Mario Carneiro
c9e84a6ad6
fix: remove private from string defs
2023-05-05 12:09:38 -07:00
Jakob von Raumer
45b49e7f02
fix: typos
2023-05-05 12:07:54 -07:00
Bulhwi Cha
401e9868f8
doc: uncapitalize a letter
...
"this Type" should be "this type".
2023-05-05 12:04:35 -07:00
Gabriel Ebner
f9da1d8b55
chore: update Lake
2023-04-19 10:57:48 -07:00
Scott Morrison
ac7c447855
chore: update src/Init/Tactics.lean
2023-04-19 07:15:08 -07:00
Scott Morrison
96969363e6
chore: modify misleading doc-string for repeat tactic
2023-04-18 15:56:49 +02:00
Henrik Böving
a6ae661195
feat: profiling of linters
2023-04-18 15:30:21 +02:00
Henrik Böving
36f0acfc51
feat: add timing profiling to the new compiler
2023-04-18 12:20:27 +02:00
Sebastian Ullrich
8a302e6135
fix: match discriminant reduction should not unfold irreducible defs
2023-04-10 21:09:04 -07:00
Gabriel Ebner
7f51628986
fix: simp: strip mdata when testing for True/False
...
Fixes #2173
2023-04-10 21:06:42 -07:00
Scott Morrison
06c752448b
chore: add missing simp lemma (¬ False) = True
2023-04-10 21:05:54 -07:00
Gabriel Ebner
8075d1f45d
fix: reset local context in mkInjectiveTheorems
2023-04-10 21:05:16 -07:00
Gabriel Ebner
4af329588e
doc: clarify semi-out params
2023-04-10 13:00:04 -07:00
Gabriel Ebner
56c3e3334f
doc: semiOutParam
2023-04-10 13:00:04 -07:00
Gabriel Ebner
54c02d75b2
chore: let consumeTypeAnnotations remove semiOutParam
2023-04-10 13:00:04 -07:00
Gabriel Ebner
5eb9688846
chore: flaky tests
2023-04-10 13:00:04 -07:00
Gabriel Ebner
b8671ed18d
fix: disable checkSynthOrder for Quote instance
2023-04-10 13:00:04 -07:00
Gabriel Ebner
d58f552b84
chore: update stage0
2023-04-10 13:00:04 -07:00
Gabriel Ebner
4544443d98
feat: reorder tc subgoals according to out-params
2023-04-10 13:00:04 -07:00
Gabriel Ebner
25fe723b14
chore: add semiOutParam annotations
2023-04-10 13:00:04 -07:00
Sebastian Ullrich
a0b960b77b
perf: --profile can use tracing fast path
2023-04-10 16:57:54 +02:00
Sebastian Ullrich
41a3ebed02
fix: profiler threshold in C++
2023-04-10 16:57:54 +02:00
Sebastian Ullrich
59ac123f61
chore: remove with_trace macro again
2023-04-10 16:57:54 +02:00
Sebastian Ullrich
427540db45
chore: remove redundant Elab.input trace class in favor of Elab.command
2023-04-10 16:57:54 +02:00
Sebastian Ullrich
6fdb73c6ed
feat: pp.oneline
2023-04-10 16:57:54 +02:00
Sebastian Ullrich
3336443358
fix: convert traces to messages at outermost level only
2023-04-10 16:57:54 +02:00
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
Olivier Taïbi
9aeae67708
fix: advance pointer into array when generating random bytes
...
otherwise if we have more than one chunk then the first one is overwritten
over and over, and the end of the array is not really random
2023-04-06 11:32:12 +02:00
Bulhwi Cha
d694bf2d09
doc: heading ( #2180 )
...
Add '#' to the docstring.
2023-04-03 09:40:22 +02:00
Enrico Borba
6d583284df
chore: Nix: fix depRoot with huge number of deps ( #2179 )
...
If `deps` or `depRoots` are too large, bash will carsh when executing
the modified script. This is because there are OS-level limits on the
size of environment variables. This commit changes the script so that
`deps` and `depRoots` are written to files instead of being passed as
environment variables.
2023-04-01 09:45:38 +02:00
Gabriel Ebner
742d053a97
fix: respect pp.raw in interactive .ofGoal
...
Fixes #2175
2023-03-30 17:19:35 -07:00
Adrien Champion
39f0fa670a
doc: document Int and its basic operations ( #2167 )
2023-03-28 14:54:14 +02:00
Connor Baker
667d54640d
chore: Nix: use strings instead of URL literals ( #2172 )
2023-03-28 10:10:24 +02:00
github-actions[bot]
5495a4f91c
doc: update changelog
2023-03-27 15:48:22 +00:00
Sebastian Ullrich
b076d488e3
feat: show typeclass and tactic names in profile output
2023-03-27 17:47:52 +02:00
Sebastian Ullrich
4048455060
chore: Nix: fix asan attribute
2023-03-27 16:48:49 +02:00
int-y1
9bc6fa1c6e
chore: fix typos
2023-03-27 10:05:50 +02:00
Sebastian Ullrich
b81cff87bc
chore: update temci
2023-03-24 11:34:21 +01:00
Pietro Monticone
158d58f3c3
doc: fix typos ( #2160 )
2023-03-22 10:01:59 +01:00
Sebastian Ullrich
042d14c470
fix: List.append_eq name
...
Fixes #2157
2023-03-19 10:28:48 +01: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
83c1a1ab77
chore: bench: update temci
2023-03-16 16:39:50 +01: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
c327a61d33
chore: update stage0
2023-03-15 14:14:39 +01:00
