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

231 commits

Author SHA1 Message Date
Mario Carneiro
b2b02295b0 chore: move ShareCommon to Init / Lean 2022-08-30 07:51:43 -07:00
Mario Carneiro
bf89c5a0f5 chore: move Std -> Bootstrap 2022-08-29 01:26:12 -07:00
Gabriel Ebner
2e6395d525 doc: trace messages 2022-08-15 08:55:25 -07:00
Gabriel Ebner
5e4b30c777 chore: remove traceCtx 2022-08-15 08:55:25 -07:00
Gabriel Ebner
64031e5231 chore: remove obsolete addTraceOptions 2022-08-15 08:55:25 -07:00
Gabriel Ebner
4e2899e354 chore: remove nested trace api 2022-08-15 08:55:25 -07:00
Gabriel Ebner
ef223c02b8 feat: make trace class inheritance opt-in 2022-08-15 08:55:25 -07:00
Gabriel Ebner
847125d2e8 chore: remove global trace enabled flag 2022-08-15 08:55:25 -07:00
Gabriel Ebner
7e020d45e6 feat: add emoji helpers for trace messages 2022-08-15 08:55:25 -07:00
Gabriel Ebner
c7e45722a3 feat: trace nodes with messages 2022-08-15 08:55:25 -07:00
Leonardo de Moura
3896244c55 chore: cleanup 2022-07-25 22:39:56 -07:00
Leonardo de Moura
a62949c49b refactor: add type LevelMVarId (and abbreviation LMarId) 
Motivation: make sure we do not mixup metavariable ids for
expression and universe level.

cc @bollu
 2022-07-24 17:21:45 -07:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
Gabriel Ebner
eda3eae18e perf: implement Expr.update* in Lean 2022-07-19 05:55:13 -07:00
Gabriel Ebner
a8cab84735 refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
Gabriel Ebner
eba400543d refactor: use computed fields for Name 2022-07-11 14:19:41 -07:00
Gabriel Ebner
3176943750 refactor: use computed fields for Level 2022-07-11 14:19:41 -07:00
Leonardo de Moura
394d49da58 perf: Expr.hasSorry and similar functions 
Functions were ignoring sharing while traversing `Expr`.

Addresses performance problem exposed by #1287
 2022-07-10 07:39:38 -07:00
Leonardo de Moura
e4b358a01e refactor: prepare to elaborate a[i] notation using typeclasses 2022-07-09 15:24:22 -07:00
Leonardo de Moura
c9771fa1b2 chore: unused variables 2022-07-07 20:24:18 -07:00
Leonardo de Moura
608a306ef0 refactor: simplify/cleanup DelayedMetavarAssignment 2022-07-06 15:24:17 -07:00
Leonardo de Moura
2446c64a99 chore: cleanup 2022-07-04 07:15:04 -07:00
Leonardo de Moura
a1413b8fa1 feat: cache failures at isDefEq 
We can compile Lean with these changes, but 3 tests are still broken.
This cache is used to address a performance issue reported at
  https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout.20with.20structures/near/288180087
 2022-07-03 21:52:01 -07:00
Sebastian Ullrich
2f67295c7d feat: strengthen pp* signatures 2022-07-03 19:14:49 +02:00
Sebastian Ullrich
a12cde41e1 chore: work around macro limitations 
It would be nice if `macro` was as expressive as syntax quotations, but
right now it's not.
 2022-06-27 22:37:02 +02:00
Leonardo de Moura
96a72d67f2 fix: avoid unnecessary dependencies at mkMatcher 
fixes #1237
 2022-06-23 10:21:32 -07:00
Leonardo de Moura
2a940dd4ae feat: add Expr.collectFVars, LocalDecl.collectFVars, Pattern.collectFVars, and AltLHS.collectFVars 
They are all in `MetaM`.

These are helper functions for issue #1237. We need to "cleanup" the
local context before trying to compile the match-expression.

see issue #1237
 2022-06-22 15:53:43 -07:00
Leonardo de Moura
02c4e548df feat: replace constant with opaque 2022-06-14 17:02:59 -07:00
Leonardo de Moura
041827bed5 chore: unused variables 2022-06-07 17:54:10 -07:00
Sebastian Ullrich
ae7b895f7a refactor: unname some unused variables 2022-06-07 16:37:45 -07:00
Sebastian Ullrich
85e0e0ad20 doc: fix Expr.forEach' docstring 2022-06-05 14:16:29 +02:00
Leonardo de Moura
64c36fffda feat: generate warning message if declaration has a non-synthetic sorry 
closes #1163
 2022-05-31 18:00:48 -07:00
Leonardo de Moura
be69d04af4 feat: add Declaration.hasSorry 2022-05-31 16:39:37 -07:00
Leonardo de Moura
c65537aea5 feat: Option is a Monad again 
TODO: remove `OptionM` after update stage0

see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084
 2022-05-04 15:27:42 -07:00
Sebastian Ullrich
e1fbc04c3b chore: accept unregistered syntax kinds in stage 1 2022-04-15 08:50:46 -07:00
Leonardo de Moura
3cf425ba52 fix: pattern hover information 
We annotate patterns with the corresponding `Syntax` during
elaboration, and do not populate the info tree. Reason: the set of
pattern variables is not known during pattern elaboration.
 2022-04-08 15:03:42 -07:00
Leonardo de Moura
5283007aa4 feat: add HasConstCache 2022-03-15 08:39:48 -07:00
Sebastian Ullrich
147a5c2933 chore: prefer LEAN_SRC_PATH 2022-03-14 17:24:25 +01:00
Leonardo de Moura
63a5cd5056 fix: trace_state messages should not be lost during backtracking 2022-02-28 11:07:41 -08:00
Sebastian Ullrich
53d313c74c chore: fix function name 2022-02-28 16:16:22 +01:00
Leonardo de Moura
15546fbc48 feat: add Expr.findExt? 2022-02-23 12:32:17 -08:00
Leonardo de Moura
12e2a79170 chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
Sebastian Ullrich
22526051e0 fix: install sources to src/lean/, not lib/lean 
Not only is this more semantically appropriate (see e.g.
`/usr/src/{linux,rust,...}` on Debian), it also prevents .ilean files
from Lake tests (which are symlinked into the build directory as part of
`src/` during development) from ending up in the built-in LEAN_PATH and
being watched & loaded by the server.
 2022-02-03 18:20:21 +01:00
Leonardo de Moura
cf3b8d4eb4 chore: cleanup 
Make the code style more uniform.
We still have a lot of leftovers from the old frontend.
 2022-01-26 09:18:17 -08:00
Sebastian Ullrich
cfaba85199 feat: load precompiled modules in the server 2022-01-25 23:25:52 +01:00
Leonardo de Moura
02677cf326 fix: igore instance implicit arguments in term ordering used at simp 
closes #972
 2022-01-24 18:57:31 -08:00
Leonardo de Moura
7ada79bf2e fix: use an AC-compatible ordering on Expr at simp 
closes #968
 2022-01-22 09:42:59 -08:00
Joscha
9949f92648 refactor: base findModuleWithExt on findWithExt 2022-01-20 17:20:01 +01:00
Joscha
7540889bd3 feat: implement LSP workspace symbol request 2022-01-20 17:20:01 +01:00
Leonardo de Moura
9d05023325 chore: remove some [specialize] annotations 2022-01-18 09:24:06 -08:00