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

207 commits

Author SHA1 Message Date
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
Sebastian Ullrich
3abb70dbb5 refactor: factor out common source search path logic 2022-01-18 18:22:50 +01:00
Leonardo de Moura
bac91b9b5b chore: remove arbitrary 2022-01-15 12:14:27 -08:00
Sebastian Ullrich
753e396705 fix: recurse in findAllWithExt 2022-01-14 18:59:58 +01:00
Sebastian Ullrich
8e5fc66330 fix: do not error on non-existent search path entries 2022-01-14 09:18:57 +01:00
Joscha
4fd1d22c31 feat: load and unload ileans on LSP notifications 2022-01-14 09:18:57 +01:00
Joscha
4e12cc902b feat: load ilean files from olean search path 2022-01-14 09:18:57 +01:00
Leonardo de Moura
0fc8c1da77 feat: eta for structures at recursors 
see #777
 2021-11-25 11:31:00 -08:00
Sebastian Ullrich
c6c56b15e1 feat: findSysroot? & reworked initSearchPath 2021-11-20 11:04:39 +01:00
Gabriel Ebner
34eda689a1 fix: use eraseMacroScopes on trace classes 2021-10-08 11:13:19 -07:00
Sebastian Ullrich
0a43a9c466 refactor: use JSON to communicate between server & package manager 2021-10-08 11:28:04 +02:00
Leonardo de Moura
da69b10056 chore: cleanup 2021-09-17 15:00:58 -07:00
Leonardo de Moura
445cc3085f refactor: avoid Name, MVarId, and FVarId confusion 2021-09-07 19:06:50 -07:00
Leonardo de Moura
d43a1c7d9a chore: move Constructions to Meta 2021-09-06 10:51:11 -07:00
Leonardo de Moura
79938056ad chore: add isIte and isDIte 2021-08-30 07:08:19 -07:00
Wojciech Nawrocki
e3d866bc03 feat: initial TraceExplorer 
Motivation: trace messages from systems such as instance synthesis or defeq checks can be massive and it is hard to find the relevant info within. We provide an interactive TraceExplorer component to do this.
 2021-08-24 08:57:41 -07:00
Leonardo de Moura
bb755d6245 feat: add commitIfNoEx 2021-08-17 21:32:32 -07:00
Leonardo de Moura
4635c3afd1 chore: add notNot? 2021-08-17 21:32:32 -07:00
Sebastian Ullrich
94437bcfbb fix: import hint 2021-08-17 11:14:42 +02:00
Leonardo de Moura
7cec20582b feat: add instance Alternative (MonadCacheT α β m) 2021-08-10 14:28:04 -07:00
Daniel Selsam
c6e1e356ab perf: trace messages should disable pp.analyze 2021-08-06 18:30:40 +02:00
Daniel Selsam
b8b48b0f72 refactor: move FindLevelMVar to Lean/Util 2021-08-03 09:13:18 +02:00
Gabriel Ebner
3cff5ceb99 perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
Sebastian Ullrich
4ed66cae3e feat: add --print-prefix, --print-libdir flags 
The names were taken from `llvm-config`
 2021-06-11 17:53:51 -07:00
Sebastian Ullrich
1ebcf76d48 refactor: remove explicitly lifted IO functions and move more things into IO.FS 
Automatic lifting takes care of this, and it wasn't consistently applied anyway
 2021-06-11 17:53:51 -07:00