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

7857 commits

Author SHA1 Message Date
Leonardo de Moura
627594b88a fix: "dot"-notation should apply default instances before failing 
See new test for motivating example.
 2022-07-05 14:27:55 -07:00
Leonardo de Moura
2b2d4245dc fix: extensible tactics bug 
See comment at `expandMacros`
 2022-07-05 13:20:22 -07:00
Sebastian Ullrich
6303fb77d2 fix: expansion info for macro commands 
TODO: investigate that pp error
 2022-07-05 13:18:59 +02:00
tydeu
bff560759e feat: add missing literal TSyntax helpers 2022-07-05 13:18:58 +02:00
Leonardo de Moura
2061c9bbea chore: reduce test size 
TODO: investigate why there is a stack overflow in the CI.
I didn't manage to reproduce it on my machine.
 2022-07-04 13:58:06 -07:00
Leonardo de Moura
1999db1d7c test: add test for performance issue 
This issue has bee reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout.20with.20structures/near/288180087
 2022-07-04 07:20:12 -07:00
Leonardo de Moura
c434e4e096 chore: remove old tests 2022-07-04 07:18:07 -07:00
Leonardo de Moura
64edb50687 chore: fix tests 2022-07-04 06:35:21 -07:00
Leonardo de Moura
76245b39d1 chore: remove dead field 
We have remove the old frontend a long time ago.
 2022-07-03 15:38:48 -07:00
Gabriel Ebner
07a3cd6980 chore: fix tests 2022-07-03 22:46:59 +02:00
Leonardo de Moura
03ce7cb17c fix: dependent pattern matching bug 
closes #1279
Originally reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/case.20in.20dependent.20match.20not.20triggering.20.28.3F.29/near/288328239
 2022-07-03 13:25:12 -07:00
Leonardo de Moura
68024b11a4 fix: simp_all bug when goal has duplicate hypotheses 2022-07-03 12:44:53 -07:00
Sebastian Ullrich
2f67295c7d feat: strengthen pp* signatures 2022-07-03 19:14:49 +02:00
Leonardo de Moura
a0fdc2d050 chore: fix tests 2022-07-02 15:57:05 -07:00
Leonardo de Moura
4568fe755c chore: fix tests 2022-07-02 15:25:06 -07:00
Leonardo de Moura
e4b472a9a2 chore: fix tests 2022-07-02 15:17:01 -07:00
Leonardo de Moura
8bf90b128e fix: interactive test driver 2022-07-02 10:01:04 -07:00
Leonardo de Moura
053bc889a3 feat: elaborate a[i]! and a[i]? 2022-07-02 07:29:58 -07:00
tydeu
515541709a chore: fix tests 2022-07-02 10:37:22 +02:00
Leonardo de Moura
a639eb185c fix: dsimp zeta issue 2022-07-01 06:42:09 -07:00
Leonardo de Moura
14260f454b feat: improve is_def_eq for projections 
It implements in the kernel the optimization in the previous commit.

This commit addresses the following issue raised on Zulip.
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unfold.20essentially.20loops/near/288083209
 2022-06-30 17:50:44 -07:00
Leonardo de Moura
467ac9d98a feat: add support for CommandElabM at #eval 
Note that it does not use `MetaEval` to execute the term of type
`CommandEval`. Thus, we can now use `#eval` to execute simple commands.

see #1256
 2022-06-29 16:34:49 -07:00
Leonardo de Moura
d4eed2e490 test: test for #1267 2022-06-29 15:40:13 -07:00
Leonardo de Moura
e968dfb68c feat: elaborate do notation even when expected type is not available 
see issue #1256
 2022-06-29 13:30:06 -07:00
Leonardo de Moura
598898a087 fix: fixes #1265 2022-06-29 12:41:14 -07:00
Leonardo de Moura
15e2a7d5b4 feat: report errors an unassigned metavars at #eval 
See #1256
 2022-06-29 11:53:33 -07:00
Sebastian Ullrich
c8fb72195b feat: print panic backtraces on Linux 2022-06-29 16:29:35 +02:00
Leonardo de Moura
a888b21bce fix: compiler bug at And.casesOn 
Fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.28libc.2B.2Babi.29.20lean.3A.3Aexception.3A.20incomplete.20case/near/287839995
 2022-06-29 06:56:17 -07:00
Sebastian Ullrich
c64ac02ffc fix: declModifiers syntax kind 2022-06-28 22:35:13 +02:00
Leonardo de Moura
34dc2572f3 fix: make sure OfScientific Float instance is never unfolded during type class resolution 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout/near/287654818

Type class resolution was diverging when trying to synthesize
```lean
 HSub (optParam Float 0.0) (optParam Float 1.0) ?m.472
```
and Lean was diverging while unfolding
```lean
 instance : OfScientific Float where
   ofScientific m s e :=
     if s then
       let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
       let m := (m <<< (3 * e + s)) / 5^e
       Float.ofBinaryScientific m (-4 * e - s)
     else
       Float.ofBinaryScientific (m * 5^e) e
```
was being unfolded.

Anothe potential solution for the problem above is to erase the
`optParam` annotations before performing type class resolution.
 2022-06-27 17:40:34 -07:00
Leonardo de Moura
5901fef43a feat: protected aliases 
See message: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Namespace-based.20overloading.20does.20not.20find.20exports/near/287633118
 2022-06-27 13:56:58 -07:00
Sebastian Ullrich
3a56db2812 chore: fix tests 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
0bd864deca fix: nesting of pattern info nodes 2022-06-27 22:37:02 +02:00
Leonardo de Moura
f4e083d507 feat: dot notation and aliases 
This commit addresses the issue raised at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Namespace-based.20overloading.20does.20not.20find.20exports/near/282946185
 2022-06-27 12:42:25 -07:00
Leonardo de Moura
fc25689f21 feat: add Syntax.eraseSuffix? 2022-06-27 10:30:57 -07:00
Leonardo de Moura
3f0a9eb424 test: add test for issue #1253 
closes #1253
 2022-06-27 09:56:47 -07:00
Leonardo de Moura
220d2e3816 feat: add filterTR and [csimp] theorem 2022-06-24 06:40:38 -07:00
Leonardo de Moura
1fd2b17a92 fix: bug at addDependencies 
closes #1247
 2022-06-24 06:20:00 -07:00
Gabriel Ebner
233a787e65 chore: add test for sepByIndent.formatter 2022-06-24 10:59:55 +02:00
Leonardo de Moura
98c775da34 feat: save mutual block information for definitions/theorems/opaques 2022-06-23 16:39:51 -07:00
Henrik Böving
0fde2db75e feat: improve the heuristic for notation delab 
Instead of the previous constraints on the right hand side that only
allowed a permutation of variables as parameters to a function the
new heuristic allows anything to the right of a function as long as
each variable only appears at most once.
 2022-06-23 13:27:53 -07:00
Leonardo de Moura
96a72d67f2 fix: avoid unnecessary dependencies at mkMatcher 
fixes #1237
 2022-06-23 10:21:32 -07:00
Leonardo de Moura
939f8d9f16 fix: fixes #1240 2022-06-23 05:53:06 -07:00
Sebastian Ullrich
1f13729756 feat: show term goal at end of term as well 2022-06-23 14:44:19 +02:00
Sebastian Ullrich
13bcbce144 chore: fix Nix test output filter 2022-06-23 14:05:53 +02:00
Leonardo de Moura
53acd3e355 feat: allow ext conv tactic to go inside let-declarations 2022-06-22 19:27:04 -07:00
Leonardo de Moura
a802544c90 fix: intro tactic at let-expr 2022-06-22 16:10:33 -07:00
Leonardo de Moura
9678be4d81 fix: store discharge depth when caching simp results 
Closes #1234
 2022-06-21 15:35:47 -07:00
Leonardo de Moura
65d24f4e39 fix: typo at LinearExpr.toExpr 
closes #1236
 2022-06-21 14:28:26 -07:00
Leonardo de Moura
e442fbbf54 fix: remove kabstractWithPred 
The function `kabstractWithPred` was never used, and introduced the
bug exposed by issue #1235.

fixes #1235
 2022-06-20 16:35:18 -07:00