Sebastian Ullrich
cf1654df1f
fix: Nix: precompilation against stdlib, once more
2022-01-25 23:25:52 +01:00
Sebastian Ullrich
180cc59d64
chore: update Lake to https://github.com/leanprover/lake/pull/48/files
2022-01-25 23:25:52 +01:00
Sebastian Ullrich
cfaba85199
feat: load precompiled modules in the server
2022-01-25 23:25:52 +01:00
Sebastian Ullrich
a926c6b1b2
chore: Nix: more consistent drv name
2022-01-25 23:25:52 +01:00
Sebastian Ullrich
8893ba9fa0
fix: Nix: precompilation on macOS
2022-01-25 23:25:52 +01:00
Sebastian Ullrich
9b87428555
fix: Nix: work around https://github.com/NixOS/nixpkgs/issues/148189
2022-01-25 23:25:52 +01:00
Sebastian Ullrich
23db584b8f
fix: Nix: precompilation against stdlib
2022-01-25 23:25:52 +01:00
Sebastian Ullrich
b601f2ffb2
perf: Nix: use bare command for shared libs
2022-01-25 23:25:52 +01:00
Sebastian Ullrich
096250a585
feat: Nix: simple, opt-in precompilation scheme
2022-01-25 23:25:52 +01:00
Sebastian Ullrich
01987dbc8e
refactor: Nix: attach object drv to module drv
2022-01-25 23:25:52 +01:00
Sebastian Ullrich
ac28f89527
fix: Nix: link package's shared library dynamically against dependencies
...
refactor: Nix: dynlib handling
2022-01-25 23:25:52 +01:00
Leonardo de Moura
234f70fadb
chore: remove the now incorrect comment
2022-01-24 19:05:05 -08:00
Leonardo de Moura
02677cf326
fix: igore instance implicit arguments in term ordering used at simp
...
closes #972
2022-01-24 18:57:31 -08:00
Leonardo de Moura
d4f7899591
chore: avoid code duplication setting Simp.Config
2022-01-24 18:57:31 -08:00
Sebastian Ullrich
b20ecd02d7
chore: move out lean4-mode
2022-01-24 21:23:53 +01:00
Leonardo de Moura
722bf54929
fix: trace message with incorrect MetavarContext
2022-01-24 10:34:44 -08:00
Leonardo de Moura
7ada79bf2e
fix: use an AC-compatible ordering on Expr at simp
...
closes #968
2022-01-22 09:42:59 -08:00
Leonardo de Moura
763a337c25
chore: helper functions
2022-01-22 09:30:57 -08:00
Leonardo de Moura
d096f59f86
chore: update stage0
2022-01-22 08:06:31 -08:00
Leonardo de Moura
0615020cf7
feat: make sure Expr.approxDepth does not overflow
2022-01-22 07:45:19 -08:00
Tom Ball
0b140ea451
doc: fix error in manual example
...
Co-authored-by: Tom Ball <you@example.com>
2022-01-22 10:03:32 +01:00
Sebastian Ullrich
fb57b73e1f
fix: Nix: compatibility with standard build
2022-01-21 09:24:43 +01:00
Leonardo de Moura
79dec8fa7c
chore: fix test
2022-01-20 17:19:29 -08:00
Leonardo de Moura
253f3aa5ec
chore: update stage0
2022-01-20 17:16:50 -08:00
Leonardo de Moura
d39025e343
test: add test for issue #951
2022-01-20 17:16:06 -08:00
Leonardo de Moura
893b816f82
chore: update stage0
2022-01-20 17:11:09 -08:00
Leonardo de Moura
b0083e0dd0
feat: use elaborated type to generate instance name
...
closes #951
2022-01-20 17:09:55 -08:00
Leonardo de Moura
a9659afa50
chore: remove old decls
2022-01-20 15:35:19 -08:00
Leonardo de Moura
70de6dabb3
chore: update stage0
2022-01-20 15:33:45 -08:00
Leonardo de Moura
6f416147b4
chore: rename coeM and liftCoeM
2022-01-20 15:33:17 -08:00
Leonardo de Moura
0c959b6942
chore: fix tests
2022-01-20 15:25:59 -08:00
Leonardo de Moura
2192e6148b
chore: remove coe, coeSort, and coeFun abbreviations
...
The notation `↑ e` is now expanded eagerly.
See #403
2022-01-20 15:19:06 -08:00
Leonardo de Moura
7c0a790774
chore: update stage0
2022-01-20 15:10:13 -08:00
Leonardo de Moura
3c17755730
chore: prepare to remove coe definitions
...
The notation `↑ e` will eagerly expand the coersion.
See #403
2022-01-20 15:07:54 -08:00
Leonardo de Moura
f9fa24435d
chore: remove problematic instance hasOfNatOfCoe
...
See #403
See https://github.com/leanprover-community/mathport/issues/94
2022-01-20 14:47:25 -08:00
Sebastian Ullrich
f0f26728ed
doc: more about initializers
2022-01-20 18:55:57 +01:00
Sebastian Ullrich
dc148003cb
chore: Nix: remove annoying output
2022-01-20 18:55:57 +01:00
Sebastian Ullrich
52de670497
chore: clarify safety of compile-time code execution
2022-01-20 18:55:57 +01:00
Sebastian Ullrich
c59f7a55cf
fix: initialize precompiled modules
2022-01-20 18:55:57 +01:00
Leonardo de Moura
e7dd03d5d1
chore: remove tmp dir
2022-01-20 09:54:28 -08:00
Leonardo de Moura
b1a92f5cbf
feat: better Repr instances for Level.Data and Expr.Data
...
see #619
2022-01-20 09:45:30 -08:00
Leonardo de Moura
ff4be1e1db
feat: add Repr instances for Level and Expr
...
closes #619
TODO: a better `Repr` instance for `Expr.Data`
2022-01-20 09:26:06 -08:00
Leonardo de Moura
d190d6dda4
fix: use default reducibility when proving equation theorems for definition
...
Addresses issue reported by @fpfu at #945
2022-01-20 08:23:51 -08:00
Joscha
9949f92648
refactor: base findModuleWithExt on findWithExt
2022-01-20 17:20:01 +01:00
Joscha
2423a78db4
refactor: implement suggestions
2022-01-20 17:20:01 +01:00
Sebastian Ullrich
3a926b1047
fix: use user-facing private decl name in symbol query
2022-01-20 17:20:01 +01:00
Sebastian Ullrich
53d90a71ae
feat: do case-sensitive symbol query if query contains upper-case char
2022-01-20 17:20:01 +01:00
Sebastian Ullrich
1168334cca
fix: Unicode symbol lookup
2022-01-20 17:20:01 +01:00
Joscha
7540889bd3
feat: implement LSP workspace symbol request
2022-01-20 17:20:01 +01:00
Sebastian Ullrich
ccf1292e07
fix: rework header/lib handling with bundled clang
...
* use `-nostdinc` to make sure system headers don't affect us
* include clang headers with `-isystem`, which suppresses all those warnings
* do not use default sysroot on Windows after all, since that can be a
surprising location
Fixes #922
2022-01-20 16:05:54 +01:00
