max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
30639 commits 1 branch 0 tags 5.3 GiB
Commit graph

8493 commits

Author SHA1 Message Date
Sebastian Ullrich
b81cff87bc chore: update temci 2023-03-24 11:34:21 +01: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
b8cc5b277e fix: strict indentation check in · tacs 2023-03-15 11:33:19 +01:00
Sebastian Ullrich
4cc6057f4a chore: ensure consistent (Unix) encoding for source files 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
d4caf1f922 fix: $_* anonymous suffix splice syntax pattern 2023-03-06 16:30:18 +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
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
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
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
Gabriel Ebner
e37f209c1a fix: unify types in calc 2023-01-27 13:38:42 -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
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
cbdd76f6b6 test: retire .perf benchmarks, cache misses are not very enlightening 2023-01-19 14:44:20 +01:00
Sebastian Ullrich
d0ca604d89 test: update mlton 2023-01-19 14:44:20 +01:00
Sebastian Ullrich
899b673531 test: add binarytrees.st benchmark 2023-01-19 14:44:20 +01:00
Sebastian Ullrich
83450d4bd9 test: clean up binarytrees.lean 2023-01-19 14:44:20 +01:00
Sebastian Ullrich
46f467db66 test: add single-threaded SML binarytrees 2023-01-19 14:44:20 +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
78bc2fd92b chore: more benchmarking setup 2023-01-17 13:28:05 +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
James Gallicchio
65db25bf49
feat: funext no arg tactic (#2027) 
* feat: `funext` no arg tactic

Description of funext tactic includes behavior that is not implemented. This implements the behavior.

* fix

* feat: test new funext tactic

* use repeat for clarity of intent
 2023-01-15 08:53:49 -08:00
Sebastian Ullrich
9b1f5c4df4 test: use OCaml 5 multicore binarytrees implementation 2023-01-12 18:28:41 +01:00
Sebastian Ullrich
f726891baf test: update benchmark flake 2023-01-12 18:28:41 +01:00
Siddharth Bhat
0900aa1348 feat: implement unreachable codegen for LLVM 
Also add a test case that exercises `unreachable` code
generation.
 2023-01-12 09:17:41 +01:00
Eric Wieser
8cd9ce0684 refactor: redefine Nat.mod such that rfl : 0 % n = 0 
This property was true in Lean 3, and it was very convenient for working with `Fin n`.
 2023-01-11 09:49:58 -08:00
James Gallicchio
37650f9147
fix: add done alternative to decreasing_with (#2019) 
Previously `decreasing_with` failed if `simp_wf` closes the goal on its
own. This can cause undesired regressions when new `simp` lemmas are
introduced.

Closes #2018.
 2023-01-09 09:46:37 -08:00
Siddharth
5615ba6606
feat: implement uset for LLVM (#2025) 
Fixes #1958.
 2023-01-09 12:25:37 +00:00
Sebastian Ullrich
fff1e12878 fix: be more careful with MatchResult.uncovered in syntax match 2023-01-09 13:05:00 +01:00
Siddharth
a0a0463451
fix: codegen initUnboxed correctly in LLVM backend (#2015) 
Closes #2004.

In porting the bugfix from
6eb852e28f,
I noticed that the LLVM backend was incorrectly generating declaration
initializers (in `callIODeclInitFn`), by assuming the return type of the
initializer is the return type of the declaration. Rather, it must be be
`lean_object`, since the initializer returns an `IO a` value which must be unpacked.

TODO: stop using the `getOrCreateFunction` pattern pervasively.
  perform the `create` at the right location, and the `get`
  at the correct location.
 2023-01-07 16:26:53 +01:00
Leonardo de Moura
474f1a4d39 feat: try to unify show type and expected type 
The goal is to address the regression
```
example : (0 : Nat) + 0 = 0 :=
  show 0 + 0 = 0 from rfl
```
introduced by fedf235cba

Note that we should only *try to* unify the types. Otherwise, we would
produce another regression.
```
example : Int :=
  show Nat from 0
```

cc @kha
 2023-01-06 08:48:48 -08:00