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
tydeu
f262f77396
chore: update Lake
2021-11-06 09:18:15 +01:00
Leonardo de Moura
b28f92a9ea
feat: improve error message produced by #eval command when it fails to synthesize "eval" instance
...
closes #765
2021-11-05 15:03:57 -07:00
Leonardo de Moura
7e0bc23e5d
chore: cleanup syntax
2021-11-05 15:03:57 -07:00
tydeu
3f867acfd7
feat: decidable Prop Eq based on propext
2021-11-05 14:09:53 -07:00
Sebastian Ullrich
03551487ad
chore: simplify test
2021-11-05 10:45:27 +01:00
Mac
eb5852448e
feat: generalize IO task functions to BaseIO := EIO Empty ( #744 )
...
* feat: generalize `asTask`/`bindTask`/`mapTask` to `EIO`
* feat: generalize task functions to the `EIO Empty` monad
* chore: fix test + correct doc
* feat: further generalize task functions to `RealM := EIO Empty`
* chore: `RealM`/Task API touch-ups
* refactor: `abbrev RealM` -> `def BaseIO`
* chore: remame args / remove `EIO.toBaseIO_` as per code review
* refactor: use `BaseIO` at `checkCanceled`/`getNumHeartbeats`
* chore: fix `lean_io_bind_task_fn` signature error
2021-11-04 15:37:55 -07:00
Sebastian Ullrich
85fb03f22c
fix: cannot dynamically link against library that depends on statically linked runtime on Windows
2021-11-04 15:32:07 -07:00
Sebastian Ullrich
b2f331f502
doc: --load-dynlib
2021-11-04 15:32:07 -07:00
Sebastian Ullrich
697e34e229
test: --load-dynlib
2021-11-04 15:32:07 -07:00
Sebastian Ullrich
1adefe197b
fix: leanc: respect LEAN_SYSROOT
2021-11-04 15:32:07 -07:00
Sebastian Ullrich
4b51d00fcb
feat: --load-dynlib
2021-11-04 15:32:07 -07:00
Sebastian Ullrich
5a65189894
chore: use empty string for --githash instead of weird "GITDIR-NOTFOUND" when not building from commit
2021-11-04 15:29:48 -07:00
Sebastian Ullrich
b5e7b2ab6e
feat: Lean.githash
2021-11-04 15:29:48 -07:00
Sebastian Ullrich
6e45685310
fix: propositions should never be considered enum types
2021-11-04 15:27:15 -07:00
Sebastian Ullrich
89ab3cadf9
doc: server: mention infoTree test
2021-11-04 18:31:36 +01:00
Sebastian Ullrich
756a2ae99a
doc: server: update & extend readme
2021-11-04 18:31:36 +01:00
Sebastian Ullrich
e92f7f1b4b
refactor: server: assume 1 info tree per snapshot
2021-11-04 18:31:36 +01:00
Sebastian Ullrich
fc5082eaef
perf: server: reset info trees for each snapshot
2021-11-04 18:31:36 +01:00
Wojciech Nawrocki
bbaf98addf
fix: relax LSP spec compliance
2021-11-01 09:11:31 -07:00
