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
Leonardo de Moura
b70820929f
chore: update stage0
2021-11-09 07:42:40 -08:00
Leonardo de Moura
ced179f2f5
feat: elaborate binrel_no_prop%
2021-11-09 07:24:46 -08:00
Leonardo de Moura
fac091498c
chore: update stage0
2021-11-09 07:02:35 -08:00
Leonardo de Moura
3c00c3270e
feat: add variant of binrel%
2021-11-09 06:51:54 -08:00
Sebastian Ullrich
138d9eea43
fix: server: custom search path should win over package one should win over system one
...
I think that's all permutations now
2021-11-09 14:27:13 +01:00
Sebastian Ullrich
a345a98ef7
chore: fix foreign test on macOS
2021-11-09 11:03:14 +01:00
Sebastian Ullrich
b053679d6d
doc: fix a few links
2021-11-09 09:55:11 +01:00
Sebastian Ullrich
941b4c21e0
chore: CRLF be gone
2021-11-09 09:49:09 +01:00
Sebastian Ullrich
c29ad9a9b3
doc: ubuntu: specify fewer versions that will become outdated anyway
2021-11-09 09:41:18 +01:00
Sebastian Ullrich
d7b8479760
chore: use configured C++ compiler for foreign test
...
Fixes #775
2021-11-09 09:27:10 +01:00
tydeu
7fcfb78fd5
feat: use BaseIO at MonadLift (ST IO.RealWorld)
2021-11-09 09:11:33 +01:00
Leonardo de Moura
a5b1b8de4f
fix: bug at Offset.lean
...
Offset equalities should not assume default `Nat` instances for
numerals, `+`, `*`, and `-` have been used.
fixes #755
2021-11-08 18:27:25 -08:00
Leonardo de Moura
84d4d771ca
fix: bug at addPPExplicitToExposeDiff
2021-11-08 18:25:57 -08:00
Sebastian Ullrich
d5e05f31e4
chore: compiler-dependent test flag
2021-11-06 23:37:19 +01:00
Sebastian Ullrich
177d45a752
chore: fail without decreasing proof
2021-11-06 18:29:59 +01:00
