Wojciech Nawrocki
2f97ecb723
chore: restore COPY_LIBS in CMake
2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
7e1faa0be1
chore: fix CMake dependencies
2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
8ada0ba043
feat: initial Emscripten support
2021-06-06 15:34:44 +02:00
Sebastian Ullrich
b82b90a687
feat: KeyedDeclAttribute: expose declaration names
2021-06-06 15:32:58 +02:00
Sebastian Ullrich
67519e226a
chore: prepare change
2021-06-06 15:32:58 +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
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
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
cbab9438c9
chore: Hashable instances for Expr and Level
2021-06-02 08:30:25 -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
5219593823
chore: use UInt64 to define Name
2021-06-02 08:00:23 -07:00
Leonardo de Moura
5ac2e14173
chore: add Hashable that uses UInt64
2021-06-02 07:47:41 -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
c566ad97a4
chore: prepare to use UInt64 hash codes
2021-06-02 06:51:18 -07: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
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
9f72ebe29b
fix: source search path from leanpkg print-paths
2021-05-28 15:30:42 +02:00
Sebastian Ullrich
e4995ce8ba
feat: add convenience coercion from String to FilePath
2021-05-28 14:19:59 +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
96b5574f21
fix: use withoutProofIrrelevance at getFixedPrefix
2021-05-27 13:42:22 -07:00
Leonardo de Moura
a247249880
feat: add configuration option for disabling proof irrelevance at MetaM
2021-05-27 13:37:26 -07:00
Leonardo de Moura
773dcf3f2e
fix: skippingBinders
...
This method was assuming the arguments of a `match` auxiliary
application were lambdas. This is not true for the automatically
generated equation theorems.
2021-05-26 20:09:12 -07:00
Leonardo de Moura
341cd7d296
fix: accidental free variable id reuse in the pretty printer
2021-05-26 16:20:50 -07:00
Sebastian Ullrich
f81abe158c
fix: memleak in release build
2021-05-26 10:24:45 +02:00
Sebastian Ullrich
2988897cac
feat: IO.FS.readDir
2021-05-26 09:47:43 +02:00
Wojciech Nawrocki
18e6f78089
fix: publish header processing message log
2021-05-26 09:30:29 +02:00
