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
Wojciech Nawrocki
485f8ea2d0
feat: setup Emscripten file paths
2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
8ada0ba043
feat: initial Emscripten support
2021-06-06 15:34:44 +02:00
Leonardo de Moura
7424f9c8b0
chore: remove HashableUSize
2021-06-02 09:58:46 -07:00
Leonardo de Moura
43812444a7
chore: Hashable => HashableUSize
2021-06-02 07:24:26 -07:00
Sebastian Ullrich
6857076df4
feat: leanpkg build without external dependencies
2021-05-30 17:29:54 +02:00
Sebastian Ullrich
619873c842
feat: make System.FilePath opaque
2021-05-28 14:19:59 +02:00
Sebastian Ullrich
98a4dfc429
fix: module names on case-insensitive platforms
2021-05-28 14:19:59 +02:00
Sebastian Ullrich
4354534fda
feat: make FilePath a concrete type
...
Resolves #363
2021-05-28 14:19:59 +02:00
Leonardo de Moura
2646f134d5
chore: add MonadBacktrack instance for ExceptT
2021-05-20 19:24:28 -07:00
Leonardo de Moura
030f53fa43
fix: closes #421
...
The unifier used to implement the `cases` tactic should not discard
equations of the form `x = t` and `t = x` using proof irrelanvance.
The new test demonstrates the issue. The unifier was reaching the
state
```
x : Conw Con.nil
|- x = Conw.nilw -> x = Conw.nilw
```
and discarding the equality instead of substituting `x`
because `x` and `Conw.nilw` are definionally equal due to
proof irrelevance.
@javra Do you have more complicated examples that were being
affected by this issue?
2021-04-23 12:27:39 -07:00
Sebastian Ullrich
c09958cf78
chore: do not display MessageData tags by default
2021-04-17 23:46:15 +02:00
Leonardo de Moura
23f49c35fc
refactor: MonadBacktrack for TacticM
2021-04-11 19:10:41 -07:00
Leonardo de Moura
2694e7798a
refactor: add MonadBacktrack
...
The new class specifies an interface for saving and restoring the
backtrackable part of the state.
This commit also fixes a few issues.
- `commitWhen` at `LevelDefEq` was defining a checkpoint for
the `isDefEq` methods, and it affects how postponed universe
constraints are handled. However, the name suggests it is
similar to `commitWhenSome?`, and consequently it was used
in other places that had nothing to do with `isDefEq`.
So, I renamed it, and provided the generic `commitWhen` at the new
`MonadBacktrack.lean` file.
- We were restoring more state then needed in a few places.
For example, we were discarding all caches.
- At `SyntheticMVars.lean`, we were using the `Meta.commitWhenSome?`
method which does not restore the `Term.State`.
2021-04-11 19:10:41 -07:00
Sebastian Ullrich
40bb034b51
fix: use pp.raw options when falling back to raw parser
2021-04-01 16:42:04 +02:00
Leonardo de Moura
7c2338546c
feat: add pp.rawOnError
...
@Kha after I enabled elaboration on syntactically incorrect terms, the
fallback is activated more often, and the raw term seems to have
little value for most users, and it is just scary.
Not sure whether the flag is a good idea, but it produces are more
user friendly output.
2021-03-31 17:05:34 -07:00
Leonardo de Moura
148594ca67
chore: use register_builtin_option
2021-03-31 17:05:34 -07:00
Sebastian Ullrich
3af7bc0b87
fix: wrong dir in new error message
2021-03-23 14:06:20 +01:00
Sebastian Ullrich
ed55fdfd3e
chore: better error message when failing to find current package
2021-03-23 12:10:26 +01:00
Leonardo de Moura
9a5f239513
refactor: remove Monad Option and Alternative Option
...
We should use `OptionM` instead.
`Option` still implements `Functor` and `OrElse`.
cc @Kha
2021-03-20 18:25:25 -07:00
Leonardo de Moura
68143ca8ba
chore: trace[...]! ==> trace[...]
...
@Kha I think this one is a good change, there is no real reason for
using the `!` suffix here.
2021-03-10 18:44:43 -08:00
Leonardo de Moura
0ea267e4de
feat: add simp lemma preprocessor
2021-03-09 19:16:14 -08:00
Leonardo de Moura
7a79ef62d1
fix: bug at hasSyntheticSorry
...
It was missing a constructor, and not taking assigned metavariables
into account.
Fixes a problem reported by @JasonGross at Zulip
2021-03-05 19:08:10 -08:00
Leonardo de Moura
4908eaf396
perf: add workaround for destructive update issue
2021-02-21 13:03:45 -08:00
Leonardo de Moura
4ec85a39a5
fix: Not should not be reducible, special support for Ne
...
Unification hint for `Not`
2021-02-15 17:36:11 -08:00
Leonardo de Moura
1a15b0183b
chore: occursCheck semantics was confusing
2021-02-03 15:04:18 -08:00
Leonardo de Moura
d1efcab6f5
perf: improve occursCheck
2021-02-03 15:04:18 -08:00
Leonardo de Moura
a58ff18a5b
refactor: pos at time_task::time_task was a dead field
2021-01-30 11:10:18 -08:00
Leonardo de Moura
761b64c929
fix: missing occursCheck at SyntheticMVars
...
fixes #301
2021-01-29 17:13:04 -08:00
Leonardo de Moura
c86803392e
refactor: withNestedTraces
2021-01-29 17:13:03 -08:00
Leonardo de Moura
dff6bd300e
chore: add Expr.const?
2021-01-27 15:16:15 -08:00
Leonardo de Moura
6c119a1921
chore: use register_builtin_option
2021-01-26 18:24:56 -08:00
