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
Gabriel Ebner
f55649f81b
fix: prefer simp lemmas with *higher* priority
2021-11-22 11:52:45 -08:00
larsk21
9028405798
fix: handle _root_ in unresolveNameGlobal with pp.fullNames
2021-11-21 15:23:21 +01:00
larsk21
8cf520209f
feat: show fully-qualified name in hover text
2021-11-21 15:23:21 +01:00
larsk21
63f9b37c0a
fix: return fully-qualified name in PrettyPrinter when pp.fullNames is set
2021-11-21 15:23:21 +01:00
Sebastian Ullrich
c6c56b15e1
feat: findSysroot? & reworked initSearchPath
2021-11-20 11:04:39 +01:00
Sebastian Ullrich
6e9574045a
feat: expose C & linker flags as API
2021-11-20 11:04:39 +01:00
Sebastian Ullrich
d4683e0169
chore: clean up LEAN_EXTRA_FLAGS
2021-11-20 11:04:39 +01:00
Sebastian Ullrich
44f9edff87
feat: resolve symlinks in LEAN_SRC_PATH
2021-11-19 10:09:26 +01:00
Sebastian Ullrich
c5b6968c86
chore: symlink to source from build dir
2021-11-19 10:09:26 +01:00
Gabriel Ebner
6475e3d5cc
fix: add missing LEAN_EXPORT
2021-11-18 11:14:26 +01:00
Sebastian Ullrich
7333de1766
refactor: cmake: make more use of string(APPEND)
...
I guess CMake might not actually be that painful if one was motivated to
learn it
```
sed -Ei 's/set\(([A-Z_]+) "\$\{\1\}/string(APPEND \1 "/' src/**/CMakeLists.txt
```
2021-11-18 10:09:55 +01:00
Sebastian Ullrich
99aee53172
fix: restore macOS compile flags
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
77ccd92963
chore: remove redundant cmake install directive
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
6cda043e5b
chore: add missing LICENSES
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
ad2fe8de80
feat: bundle LLVM on macOS
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
db5b150b38
chore: do not use bundled compiler for foreign test
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
3db3fb1429
feat: bundle LLVM on Windows
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
0a40269fcb
fix: build with mingw-clang64 clang
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
09d549aecd
chore: fix foreign test on macOS, again
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
6ca944f453
chore: avoid C++ warning
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
ac5afd6b71
chore: fix leanc.sh -v
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
27bc6397a0
fix: actually link against GMP statically
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
acf7903691
feat: upload .tar.zst and .zip for every platform
...
Also, do so only for releases since `zstd -19` takes a while.
Also, stop double-wrapping artifacts
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
75a0b43aed
feat: reimplement assert without system headers
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
bfe7583356
chore: install license
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
6ef56efb79
fix: leanc: drop empty arguments
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
fe5e731064
chore: gc libleanshared sections
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
b236273780
feat: link external dependencies statically again
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
c3d1b2592c
fix: leanc: discard internal flag when using external compiler
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
5562beccee
fix: actually install all bundled files
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
d2a1e20dd0
feat: bundling LLVM on Linux
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
978e94272c
feat: String.replace
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
f232915cc0
fix: libleanshared.so needs rpath too
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
3a7fa704c3
refactor: avoid non-compiler headers in lean.h
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
25ebc68b87
fix: emit info tree on command without elaborator
...
Fixes #792
2021-11-16 10:44:17 +01:00
Scott Morrison
0fc3702d02
chore: remove superfluous abbrev
...
This abbreviation already exists as Lean.Meta.FVarIdToLemmaId, which is imported. (And in fact the code relies on the fact they are definitionally equal.)
Closes #781 .
2021-11-15 18:21:55 -08:00
Scott Morrison
835bd0869b
feat: simpLocation
2021-11-15 18:20:50 -08:00
Leonardo de Moura
2a7b33089a
fix: transparency settings at simp TC check
...
fixes #790
2021-11-15 18:09:31 -08:00
Leonardo de Moura
4b2fa38cb8
fix: #check_failure command should succeed if there are stuck TC problems
2021-11-15 16:56:55 -08:00
Leonardo de Moura
9a152d2051
fix: use withSynthesize at elabStructInstance
...
fixes #783
2021-11-15 16:45:26 -08:00
tydeu
781a28b8f4
chore: update Lake
2021-11-11 09:38:42 +01:00
tydeu
f0fd17138c
fix: pass --trust to frontend
2021-11-11 08:39:53 +01:00
Sebastian Ullrich
6e4fcaaea9
fix: produce info tree even on macro or elab failure
2021-11-11 08:39:31 +01:00
Sebastian Ullrich
8df2b07209
refactor: remove double exception layer in RequestM
2021-11-09 16:58:13 +01:00
Sebastian Ullrich
d8d7eba6c5
feat: liftExcept
2021-11-09 16:58:13 +01:00
