Sebastian Ullrich
2f35651308
perf: leak environments not freed before process exit
2023-11-14 17:33:04 +01:00
Sebastian Ullrich
fa3cf4d613
feat: translate interrupted kernel exception
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
Mario Carneiro
e0cba05167
refactor: env extensions can only modify .extensions ( #2661 )
2023-10-16 14:22:09 +11:00
Sebastian Ullrich
14c640c15e
feat: translate interrupted kernel exception
2023-10-13 09:52:26 +02:00
Scott Morrison
5d096c3fd8
chore: make Environment.add private ( #2642 )
...
* feat: replay constants into an Environment
* suggestions from code review
* chore: make Environment.add private
* patch Lake to use Environment.add via extern
2023-10-12 15:00:27 +11:00
Mario Carneiro
89b65c8f1d
feat: make Environment.mk private ( #2604 )
...
* feat: make `Environment.mk` private
---------
2023-10-04 22:02:54 +11:00
Denis Gorbachev
4b47462ccc
refactor: remove redundant let
2023-10-02 14:27:04 +02:00
Sebastian Ullrich
83ecac4fd8
perf: lake: build lakefile environment incrementally
2023-09-22 22:01:07 +02:00
David Renshaw
ba416f2c1c
fix: rename parameter of withImportModules to match doc string
2023-09-18 05:40:47 -04:00
tydeu
926663505e
chore: split up & simplify importModules
2023-08-31 15:37:33 -04:00
Gabriel Ebner
34777c9b90
fix: catch missing exceptions in kernel
2023-01-23 09:27:09 -08: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
Alex J Best
eff3c95f23
chore: fix typo in getNumBuiltiAttributes name
2022-11-21 09:22:31 -08:00
Leonardo de Moura
69bd25af4f
chore: add Repr and Inhabited instances for Import
2022-11-09 14:35:57 -08:00
Leonardo de Moura
dd45391568
chore: hoist out error generation code
...
Motivation: it was affecting my performance tests
2022-10-27 18:26:38 -07:00
Gabriel Ebner
c16d7728b0
feat: improve import duplicate definition error
2022-10-27 16:42:09 -07:00
Leonardo de Moura
346c18a5b5
perf: improve namespacesExt import function
2022-10-27 08:59:24 -07:00
Leonardo de Moura
635ccef5a3
perf: improve setImportedEntries
...
Remove linear scan at `getEntriesFor`.
2022-10-27 08:29:18 -07:00
Leonardo de Moura
44e889bd52
chore: avoid runtime bounds check
2022-10-27 07:48:30 -07:00
Leonardo de Moura
0a35ce7e3e
perf: add ModuleData.constNames
2022-10-27 07:34:07 -07:00
Leonardo de Moura
95689d914f
perf: use NameHashSet instead of NameSet
2022-10-27 07:10:54 -07:00
Leonardo de Moura
23ba495205
perf: better initial const2ModIdx size
2022-10-26 22:22:41 -07:00
Gabriel Ebner
dcc97c9bbe
fix: preserve sharing in instantiateLevelParams
2022-10-24 12:23:13 -07:00
Gabriel Ebner
725aa8b39a
refactor: instantiateTypeLevelParams in Lean
2022-10-24 12:23:13 -07:00
David Renshaw
e4ab10dc30
doc: fix some typos
...
assinged -> assigned
collction -> collection
2022-10-24 16:01:39 +02:00
David Renshaw
16320a297f
doc: fix some typos
...
Leah -> Lean
giveName -> givenName
2022-10-22 21:16:35 +02: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
4b018cdc72
chore: missing annotations
2022-10-15 19:51:56 -07:00
Mario Carneiro
391aef5cd7
feat: automatic extension names
2022-10-06 17:19:30 -07:00
Patrick Massot
f0c8e6fa2d
doc: add docstrings in PersistentExtension
...
Add docstring to functions with non-obvious persistence properties. See the discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/HashMap.20extension/near/300784691
2022-09-27 10:34:09 -07:00
Mario Carneiro
85119ba9d1
chore: move Std.* data structures to Lean.*
2022-09-26 05:46:04 -07:00
Leonardo de Moura
dadfe84c15
doc: update const2ModIdx docstring
2022-09-25 14:06:07 -07:00
Leonardo de Moura
1fb112f84b
test: Environment.addExtraName
2022-09-21 15:03:11 -07:00
Leonardo de Moura
8987de75c1
feat: add Environment.addExtraName
2022-09-21 10:57:39 -07:00
Mario Carneiro
ebb5b97d73
chore: move Bootstrap.Data -> Lean.Data
2022-08-31 11:48:57 -07:00
Mario Carneiro
bf89c5a0f5
chore: move Std -> Bootstrap
2022-08-29 01:26:12 -07:00
Patrick Massot
c9ccc9c253
doc: some SimplePersistentEnvExtension methods
...
See discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Persistent.20extension.20not.20persisting
2022-08-15 12:09:00 -07:00
Leonardo de Moura
f7ca057fea
doc: add some doc strings at Environment.lean
2022-07-30 15:05:13 -07:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -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
b48061ed23
feat: expose lower level compile function
2022-07-11 12:26:53 -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
2ebcf29cde
chore: use a[i]! for array accesses that may panic
2022-07-02 15:12:05 -07:00
Leonardo de Moura
939f8d9f16
fix: fixes #1240
2022-06-23 05:53:06 -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
