Sebastian Ullrich
9cca1a57e0
feat: generalize syntax of fvar-accepting tactics
2021-11-29 10:06:15 -08:00
Anders Christiansen Sørby
cfe924e53e
feat: Nix: add nativeSharedLibs option
...
* feat: Add nativeSharedLibs option
Use LD_PRELOAD with staticLibDeps
Add a verbose flag when debug is true
Use shared libs instead
feat: Add recursive nativeSharedLibs
Repair printPaths
Remove -v flag from lean call
feat: Use new load-dynlib option
Remove LD_PRELOAD
fix: Add allNativeSharedLibs to allLinkFlags
Trying to fix native linking
feat: Automatic link flags of nativeSharedLibs
fix: Add gmp to sharedLib buildInputs
* fix: Wrap executable files in a linker group
This is a bit slower but ensures that cycles or bad ordering of the
static lib dependencies is resolved.
* Convert allExternalDeps to a list
Breaking change if you depend on allExternalDeps being a attrset
2021-11-28 17:56:01 +01:00
Joshua Seaton
a9317760e7
chore: update IR interpreter enum hygiene
...
This change addresses -Wreturn type and -Wimplicit-fallthrough
infractions in the IR interpreter. Moreover, default switch cases on
enum classes are removed to leverage compiler complaints of missing
cases, which ensures that all related switch logic gets thoughtfully
extended when the enums are extended themselves.
2021-11-28 10:29:08 +01:00
Sebastian Ullrich
a329896e70
feat: refine declaration ranges at instance & example
2021-11-27 07:25:15 -08:00
Sebastian Ullrich
4f15805787
feat: annotate declarations with term infos
2021-11-27 07:25:15 -08:00
Leonardo de Moura
0aa32d643e
fix: eta struct and proof irrelevance issue
...
see #777
2021-11-27 07:15:57 -08:00
Leonardo de Moura
b5afc34391
chore: update stage0
2021-11-26 08:38:34 -08:00
Leonardo de Moura
2d113e83f9
feat: eta struct support for unit-like datatypes
...
For example, given `a b : Unit`, we have that `a` and `b` are
definitionally equal by `etaStruct`.
See #777
2021-11-26 08:36:25 -08:00
Leonardo de Moura
f9a5ac1d8e
fix: missing condition at matchConstStruct
2021-11-26 08:36:25 -08:00
Leonardo de Moura
693a96681a
doc: fix eta struct comment
2021-11-26 08:36:25 -08:00
Sebastian Ullrich
676b5e5ea8
chore: typo
...
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2021-11-26 17:13:19 +01:00
Sebastian Ullrich
14bc140efe
fix: server: do not show parent node on synthetic sorry
2021-11-26 17:13:19 +01:00
Sebastian Ullrich
4063729b6c
doc: document some built-in term notations
2021-11-26 17:13:19 +01:00
Sebastian Ullrich
093fd48e48
chore: update stage0
2021-11-26 17:13:19 +01:00
Sebastian Ullrich
2a1aee2b7a
feat: record declaration ranges of builtin parsers & elaborators
2021-11-26 17:13:19 +01:00
Sebastian Ullrich
e9f7c88299
feat: record doc strings of builtin parsers & elaborators
2021-11-26 17:13:19 +01:00
Sebastian Ullrich
8176084dcf
refactor: factor out declareBuiltin
2021-11-26 17:13:19 +01:00
larsk21
e641ae4eae
fix: prefix check in set_option completion
2021-11-26 11:42:54 +01:00
Leonardo de Moura
3ccd44fafa
fix: proofs after adding eta struct support at recursors
...
see #777
2021-11-25 11:34:31 -08:00
Leonardo de Moura
cec573024c
chore: update stage0
2021-11-25 11:32:53 -08:00
Leonardo de Moura
88b6ad4756
feat: add etaStruct to Meta.Simp.Config
2021-11-25 11:31:00 -08:00
Leonardo de Moura
d806344ee2
fix: set etaStruct := false at MatchEqns
2021-11-25 11:31:00 -08:00
Leonardo de Moura
43217884c0
feat: add Meta.Config.etaStruct
...
It is useful to disable eta for structures for meta programs.
2021-11-25 11:31:00 -08:00
Leonardo de Moura
0fc8c1da77
feat: eta for structures at recursors
...
see #777
2021-11-25 11:31:00 -08:00
Leonardo de Moura
50ac21d0a6
refactor: move is_constructor_app to inductive.cpp
2021-11-25 11:31:00 -08:00
Leonardo de Moura
e22bffa94f
refactor: move is_structure_like to inductive.cpp
2021-11-25 11:31:00 -08:00
Leonardo de Moura
03e346bc66
chore: simplify to_cnstr_when_K
2021-11-25 11:31:00 -08:00
Leonardo de Moura
9e1704f658
chore: simplify toCtorWhenK
2021-11-25 11:31:00 -08:00
Leonardo de Moura
ccc3f99507
chore: use isStructureLike
2021-11-25 11:31:00 -08:00
Leonardo de Moura
0de700fe45
chore: naming convetion
2021-11-25 11:31:00 -08:00
Sebastian Ullrich
8f88b1f3f8
feat: bundle llvm-ar with Lean
2021-11-25 15:05:06 +01:00
Sebastian Ullrich
9a939f98ec
chore: update stage0
2021-11-24 15:04:27 +01:00
Sebastian Ullrich
f7decd2d46
fix: go to definition for macro_rules etc.
2021-11-24 11:54:13 +01:00
Wojciech Nawrocki
17f99e353e
fix: tactic state at EOF
2021-11-24 09:15:56 +01:00
Leonardo de Moura
292d3218c2
chore: update stage0
2021-11-23 17:40:44 -08:00
Leonardo de Moura
a8f4146070
feat: support eta struct recursively
...
Addresses issues raised by @gebner at #777
2021-11-23 17:38:48 -08:00
Sebastian Ullrich
653ff184a8
fix: semantic highlighting, once more
2021-11-23 17:20:01 +01:00
Sebastian Ullrich
573c3c9760
fix: semantic highlighting, again
2021-11-23 17:02:09 +01:00
Leonardo de Moura
c447db5db9
chore: update stage0
2021-11-23 07:36:16 -08:00
Gabriel Ebner
7537fa7795
fix: unfold x<y in discrimination tree module
2021-11-23 07:34:51 -08:00
Leonardo de Moura
e15a656fd2
fix: remove @[reducible] annotation from Function.comp and Function.const
...
closes #813
2021-11-23 07:29:25 -08:00
Leonardo de Moura
9fde1d53b7
chore: adjust proofs affected by struct eta
...
closes #777
2021-11-23 06:23:50 -08:00
Leonardo de Moura
8af1024931
chore: update stage0
2021-11-23 06:23:06 -08:00
Leonardo de Moura
d685c545b4
feat: eta for structures
2021-11-23 06:21:25 -08:00
Sebastian Ullrich
dd146d50cf
fix: extra linker flags (e.g. -ldl) must come after stdlib linker flags
2021-11-23 13:07:05 +01:00
Sebastian Ullrich
12306ba401
fix: -lgmp should come last
2021-11-23 13:07:05 +01:00
Sebastian Ullrich
226121433f
fix: semantic highlighting of projection notation elaborated twice
2021-11-23 13:01:51 +01:00
Varun Gandhi
9ae6380b43
fix: only check for ccache if variables aren't passed explicitly
...
The existing CMake will emit a spurious warning when someone
tries to explicitly pass CMAKE_C(XX)_COMPILER_LAUNCHER, such
as when they point it to sccache instead of ccache.
2021-11-23 09:15:42 +01:00
Scott Morrison
43315f7f94
fix: correct spacing in the pretty printer
2021-11-23 09:13:31 +01:00
Leonardo de Moura
d9b057af03
fix: fixes #793
2021-11-22 13:28:08 -08:00
