Sebastian Ullrich
|
7ebe80ad2a
|
chore: update Nix, Nixpkgs, vscode-lean4
|
2021-06-06 15:00:40 +02:00 |
|
Sebastian Ullrich
|
65efa9603c
|
fix: lean4-mode: show latest file progress data
|
2021-06-05 17:13:28 +02:00 |
|
Sebastian Ullrich
|
6a76c95bcf
|
feat: lean4-mode: port fringe indicator from lean-mode
|
2021-06-05 17:13:24 +02:00 |
|
Sebastian Ullrich
|
822f74a35c
|
chore: update stage0
|
2021-06-05 14:23:00 +02:00 |
|
Daniel Fabian
|
4b7cb058d3
|
feat: Add support for inductive types to FromJson and ToJson handlers.
|
2021-06-05 13:53:10 +02:00 |
|
Gabriel Ebner
|
f50647e1c2
|
doc: describe non-standard requests and notifications
|
2021-06-05 13:49:28 +02:00 |
|
Gabriel Ebner
|
501c31da4d
|
feat: send $/lean/fileProgress notification
|
2021-06-05 13:49:28 +02:00 |
|
Sebastian Ullrich
|
10cf219213
|
doc: clarify RFC issues
|
2021-06-04 14:12:59 +02:00 |
|
Daniel Fabian
|
06d1d3ae07
|
fix: Use UInt64 in deriving handler for Hashable.
|
2021-06-03 06:38:44 -07:00 |
|
Gabriel Ebner
|
c47fff1b92
|
fix: cancel queued messages, not pending requests
Fixes #499.
|
2021-06-02 14:46:33 -07:00 |
|
Leonardo de Moura
|
995136d46b
|
chore: fix test
|
2021-06-02 10:03:12 -07:00 |
|
Leonardo de Moura
|
55691e2951
|
chore: update stage0
|
2021-06-02 10:00:01 -07:00 |
|
Leonardo de Moura
|
7424f9c8b0
|
chore: remove HashableUSize
|
2021-06-02 09:58:46 -07:00 |
|
Leonardo de Moura
|
37da993032
|
chore: remove HashableUSize instances
|
2021-06-02 08:48:11 -07:00 |
|
Leonardo de Moura
|
e619e7c093
|
chore: update stage0
|
2021-06-02 08:31:20 -07:00 |
|
Leonardo de Moura
|
cbab9438c9
|
chore: Hashable instances for Expr and Level
|
2021-06-02 08:30:25 -07:00 |
|
Leonardo de Moura
|
d276b47f63
|
chore: update stage0
|
2021-06-02 08:08:31 -07:00 |
|
Leonardo de Moura
|
d435b435c5
|
chore: remove workaround
|
2021-06-02 08:06:52 -07:00 |
|
Leonardo de Moura
|
d841c2e1d8
|
chore: remove dead code
|
2021-06-02 08:04:10 -07:00 |
|
Leonardo de Moura
|
a0eabad8b1
|
chore: update stage0
|
2021-06-02 08:01:07 -07:00 |
|
Leonardo de Moura
|
5219593823
|
chore: use UInt64 to define Name
|
2021-06-02 08:00:23 -07:00 |
|
Leonardo de Moura
|
30ddaaffe4
|
chore: update stage0
|
2021-06-02 07:49:54 -07:00 |
|
Leonardo de Moura
|
5ac2e14173
|
chore: add Hashable that uses UInt64
|
2021-06-02 07:47:41 -07:00 |
|
Leonardo de Moura
|
300af47e41
|
chore: update stage0
|
2021-06-02 07:25:10 -07:00 |
|
Leonardo de Moura
|
43812444a7
|
chore: Hashable => HashableUSize
|
2021-06-02 07:24:26 -07:00 |
|
Leonardo de Moura
|
6a87bba9c0
|
chore: mixHash => mixUSizeHash
|
2021-06-02 07:05:42 -07:00 |
|
Leonardo de Moura
|
d404ad67ee
|
chore: update stage0
|
2021-06-02 06:53:58 -07:00 |
|
Leonardo de Moura
|
c566ad97a4
|
chore: prepare to use UInt64 hash codes
|
2021-06-02 06:51:18 -07:00 |
|
Sebastian Ullrich
|
7839f2c99b
|
doc: direct link & instructions for elan on Windows
|
2021-06-01 16:38:03 +02:00 |
|
Sebastian Ullrich
|
812c8d0d6e
|
doc: clarify Windows limitations
|
2021-06-01 16:12:16 +02:00 |
|
Leonardo de Moura
|
3499016895
|
chore: improve error message when compiling code containing axioms or noncomputable definitions
closes #496
|
2021-05-31 20:27:15 -07:00 |
|
Sebastian Ullrich
|
3fb7a2c0e1
|
fix: make problematic Ord -> LT instance a def
|
2021-05-31 19:05:50 -07:00 |
|
Leonardo de Moura
|
fb9c1913d7
|
feat: prototype for equality theorem generator for auxiliary match functions
|
2021-05-31 18:52:22 -07:00 |
|
Leonardo de Moura
|
764ccc4fb4
|
chore: add default value for parameter
|
2021-05-31 18:52:00 -07:00 |
|
Leonardo de Moura
|
7303761569
|
feat: add modifyTarget
|
2021-05-31 18:17:07 -07:00 |
|
Leonardo de Moura
|
97ac231138
|
feat: add missing OptionT instance
|
2021-05-31 16:37:18 -07:00 |
|
Leonardo de Moura
|
4062dee864
|
fix: fixes #498
|
2021-05-31 15:42:13 -07:00 |
|
Sebastian Ullrich
|
c5957dc069
|
fix: ignore other leanpkg print-paths output
|
2021-05-31 17:39:55 +02:00 |
|
François G. Dorais
|
29dc5c5b1b
|
fix: duplicate namespace prefix
|
2021-05-31 13:31:57 +02:00 |
|
Sebastian Ullrich
|
744423f25a
|
fix: leanpkg: make flags; extend test
|
2021-05-30 17:29:54 +02:00 |
|
Sebastian Ullrich
|
db304448de
|
fix: leanpkg: rebuild if dependencies or leanpkg.toml (e.g. lean_version) changed
|
2021-05-30 17:29:54 +02:00 |
|
Sebastian Ullrich
|
693c2ccf71
|
feat: min, max, List.min/maximum?
|
2021-05-30 17:29:54 +02:00 |
|
Sebastian Ullrich
|
0e7ed52111
|
feat: leanpkg: suppress "uncaught exception: ..." message
|
2021-05-30 17:29:54 +02:00 |
|
Sebastian Ullrich
|
6857076df4
|
feat: leanpkg build without external dependencies
|
2021-05-30 17:29:54 +02:00 |
|
Sebastian Ullrich
|
37dcbf3421
|
feat: have Ord imply LT/LE
|
2021-05-30 17:29:54 +02:00 |
|
Sebastian Ullrich
|
a9fa84815b
|
feat: IO.createDir, IO.createDirAll
|
2021-05-30 17:29:54 +02:00 |
|
Sebastian Ullrich
|
94aea76922
|
feat: FilePath.metadata
|
2021-05-30 17:29:54 +02:00 |
|
Sebastian Ullrich
|
8cb116ed11
|
feat: leanpkg: better root file detection
|
2021-05-30 17:29:54 +02:00 |
|
Wojciech Nawrocki
|
e5182fe4af
|
fix: exported symbol arities
|
2021-05-29 07:56:54 +02:00 |
|
Sebastian Ullrich
|
fdad29770b
|
chore: Nix: expose vscode & extension without lean-dev wrapper
|
2021-05-28 15:31:20 +02:00 |
|