Sebastian Ullrich
bddb2152e5
chore: default compiler.enableNew to false until development restarts ( #3034 )
2023-12-21 07:48:25 +00:00
Leonardo de Moura
4afcdeb771
fix: fixes #2775
...
fixes #2744
2023-11-03 05:56:59 -07:00
Sebastian Ullrich
9874848f83
perf: inline checkInterrupted
...
Amazingly, the extra result allocation seems to have triggered a mathlib
heartbeat timeout
2023-10-26 08:33:09 +02:00
Sebastian Ullrich
74b8dda181
feat: check task cancellation in elaborator
2023-10-26 08:33:09 +02:00
Scott Morrison
fb0d0245db
Revert "Cancel outstanding tasks on document edit in the language server" ( #2703 )
...
* Revert "perf: inline `checkInterrupted`"
This reverts commit 6494af45135aae74199bc0e3b9568ea2e2481c5114c640c15e2070df2328bf48a18cf9
2023-10-17 00:59:11 +00:00
Sebastian Ullrich
6494af4513
perf: inline checkInterrupted
...
Amazingly, the extra result allocation seems to have triggered a mathlib
heartbeat timeout
2023-10-13 09:52:26 +02:00
Sebastian Ullrich
2070df2328
feat: check task cancellation in elaborator
2023-10-13 09:52:26 +02:00
Henrik
28538fc748
feat: trace nodes for kernel type checking
2023-05-31 06:10:26 -07:00
Henrik Böving
f6c8923a9b
feat: add compiler.enableNew for the new compiler
2023-05-28 17:43:32 -07:00
Sebastian Ullrich
b15d7b8f17
feat: add kernel type checking profile metric
2023-03-13 16:17:20 +01:00
Gabriel Ebner
a2f5959118
chore: use deriving Nonempty
2022-12-22 03:48:15 +01:00
Gabriel Ebner
eeab2af7ae
fix: remove Inhabited Environment instance
2022-12-21 20:08:08 +01:00
Gabriel Ebner
725aa8b39a
refactor: instantiateTypeLevelParams in Lean
2022-10-24 12:23:13 -07:00
Mario Carneiro
dd8bbe9367
fix: catch kernel exceptions in Kernel.{isDefEq, whnf}
...
fixes #1756
2022-10-20 05:38:29 -07:00
Mario Carneiro
583e023314
chore: snake-case attributes (part 2)
2022-10-19 09:28:08 -07:00
Leonardo de Moura
3f076fc836
perf: missing annotations and helper instances
2022-10-14 08:42:50 -07:00
Mario Carneiro
85119ba9d1
chore: move Std.* data structures to Lean.*
2022-09-26 05:46:04 -07:00
Leonardo de Moura
ce90e98648
feat: activate new compiler first phase
2022-09-24 14:20:21 -07:00
Leonardo de Moura
c165317b28
feat: add ImportM.runCoreM
2022-09-23 07:52:13 -07:00
Leonardo de Moura
a5abe864f3
chore: prepare to activate new code generator
2022-09-21 18:09:19 -07:00
Leonardo de Moura
9080701126
refactor: move compileDecl, compileDecls, and addDecl to CoreM
...
The new code generator entry point is in `CoreM`.
2022-09-21 18:09:19 -07:00
Leonardo de Moura
772beeeb29
feat: add withAtLeastMaxRecDepth
2022-09-19 22:04:04 -07:00
Mario Carneiro
6392c5b456
chore: import reductions
2022-09-15 14:02:38 -07:00
Leonardo de Moura
52f3a3ff2c
refactor: move mkArrow to CoreM
2022-08-10 20:21:42 -07:00
Leonardo de Moura
a489bdb107
doc: some doc strings
2022-07-30 21:18:50 -07:00
Leonardo de Moura
6fbf15043f
refactor: move InfoState to CoreM
...
We want to be able to update `InfoState` at `AttrM` which is just an
alias for `CoreM`.
I considered defining `AttrM` as `StateRefT InfoState CoreM`, but this
is problematic because we also want to invoke `AttrM` monadic
actions from `MetaM`.
Closes #1350
2022-07-25 11:57:56 -07:00
Leonardo de Moura
ca4bd67746
chore: cleanup
2022-07-12 16:42:31 -07:00
Leonardo de Moura
9102f8cb13
fix: generate sorry warning only if there are no error messages
...
see #1163
2022-06-01 06:32:05 -07:00
Leonardo de Moura
0631c90794
feat: implement MonadLog at CoreM
2022-05-31 17:40:55 -07:00
E.W.Ayers
917fa74366
doc: docstrings for decls and attributes
...
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2022-04-08 04:19:38 -07:00
Leonardo de Moura
3193acecfa
fix: flush the CoreM and MetaM caches at modifyEnv
...
This fix may impact performance. Note that we don't need to flush the
cache if we are "adding" stuff to the environment. We only need to
flush the caches if the change is not monotonic. BTW, most of the
changes are monotonic. I think this is why we did not hit this bug before.
We may also move all these caches to an environment extension. It is
an easy way to make sure we preserve the cache when extending the
environment.
I tried a few benchmarks and did not notice a significant difference.
cc @kha @gebner
fixes #1051
2022-03-17 16:02:30 -07:00
Leonardo de Moura
0bd9de1cb9
perf: add InstantiateLevelCaches for types and values at CoreM
2022-03-15 17:42:38 -07:00
Leonardo de Moura
2fb9a39cb4
refactor: implement MonadQuotation at CoreM
2022-03-10 09:55:20 -08:00
Leonardo de Moura
adf3510e08
chore: increase maxHeartbeats default values
...
We now increase the number of heartbeats at `expr_eq_fn`. Thus, the
old default values are too small.
2022-02-28 15:44:08 -08:00
Leonardo de Moura
eff63632b3
feat: improve error message when max heartbeats is reached during TC
...
see #1007
2022-02-07 11:23:48 -08: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
Leonardo de Moura
bac91b9b5b
chore: remove arbitrary
2022-01-15 12:14:27 -08:00
Mac
eb5852448e
feat: generalize IO task functions to BaseIO := EIO Empty ( #744 )
...
* feat: generalize `asTask`/`bindTask`/`mapTask` to `EIO`
* feat: generalize task functions to the `EIO Empty` monad
* chore: fix test + correct doc
* feat: further generalize task functions to `RealM := EIO Empty`
* chore: `RealM`/Task API touch-ups
* refactor: `abbrev RealM` -> `def BaseIO`
* chore: remame args / remove `EIO.toBaseIO_` as per code review
* refactor: use `BaseIO` at `checkCanceled`/`getNumHeartbeats`
* chore: fix `lean_io_bind_task_fn` signature error
2021-11-04 15:37:55 -07:00
Leonardo de Moura
633dc9829e
feat: add withOptions
2021-09-17 14:20:28 -07:00
Sebastian Ullrich
16026e9edd
perf: restore monad instance specialization hack
2021-08-12 21:09:09 +02:00
Sebastian Ullrich
30a0954424
refactor: revert MonadRef changes
2021-06-21 10:17:26 -07:00
Sebastian Ullrich
da4c46370d
feat: store elaborator declaration name in info tree
2021-06-21 10:17:26 -07:00
Sebastian Ullrich
380c6c285a
perf: specialize some monad instances
2021-06-17 11:25:58 +02:00
Leonardo de Moura
dbc84c502c
chore: make sure we don't lift methods over binders
2021-04-15 12:06:46 -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
Leonardo de Moura
be841a7cad
chore: throwError! => throwError, throwErrorAt! => throwErrorAt
...
@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
2021-03-11 11:59:45 -08:00
Leonardo de Moura
d75c4e2101
chore: cleanup
2021-03-06 15:32:59 -08:00
Leonardo de Moura
6c119a1921
chore: use register_builtin_option
2021-01-26 18:24:56 -08:00
Leonardo de Moura
f53e83b182
feat: add options maxHeartbeats and synthInstance.maxHeartbeats
2021-01-24 17:45:50 -08:00
Leonardo de Moura
04a07c15b9
chore: use deriving Inhabited
2020-12-13 11:57:59 -08:00
