Sebastian Ullrich
abef59ddbb
chore: remove LICENSE header that confused GitHub
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
74a616a965
chore: final cleanup?
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
60095ce13f
chore: CI: even shorter install tree listing
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
767e9cffda
chore: CI: check test binary as well
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
337c3715dc
chore: ci: fix List Install Tree
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
749158c8c1
perf: strip LLVM binaries
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
42ee91bcda
fix: Linux: bundle zlib
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
8f4e59d9b5
chore: update lean-llvm
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
c3f7f09aad
fix: use old nixpkgs for glibc only
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
d5d8ada8b8
chore: split LICENSE again
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
2cb625e9c4
chore: update lean-llvm
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
881238cc0d
chore: append licenses of LLVM & glibc
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
5bbc160f4b
feat: use custom, more minimal LLVM build
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
92b692808b
chore: CI: list archive contents & sizes
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
4b8a8d241d
chore: CI: no more need for binary patching
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
Leonardo de Moura
47956b9b9e
chore: fix test
2021-11-15 18:47:25 -08:00
Leonardo de Moura
c67541570f
fix: fixes #787
2021-11-15 18:31:57 -08: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
Leonardo de Moura
743810b77a
feat: use binrel_no_prop% to define == notation
...
fixes #764
2021-11-09 07:46:10 -08:00
