max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
26350 commits 1 branch 0 tags 5.3 GiB
Commit graph

26350 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Wojciech Nawrocki
128a71c726 fix: excessive RPC logging 2021-11-01 09:11:31 -07:00
Sebastian Ullrich
571fc66864 doc: ffi: move into dev/ 2021-10-29 08:46:31 -07:00
Sebastian Ullrich
81dca2ceb8 doc: ffi: address review 2021-10-29 08:46:31 -07:00
Sebastian Ullrich
627900ba9f doc: FFI 2021-10-29 08:46:31 -07:00
Leonardo de Moura
5f119cb54f feat: avoid metavariables at CompletionItems 
Not sure whether it helps or creates more confusion.
Note that we are still using the `?` prefix for metavariables on the
InfoView and hover info.
 2021-10-29 08:01:21 -07:00
Sebastian Ullrich
40cf61f67b doc: very important clarification 2021-10-29 07:52:48 -07:00
Chris Lovett
d3da41bac6
chore: remove unused header from lean.h 2021-10-29 09:43:19 +02:00
Leonardo de Moura
68120b24b8 feat: add docstring to CompletionItem 
closes #746
 2021-10-28 08:14:40 -07:00
Sebastian Ullrich
f92d494c48 chore: do not distribute Lake examples 2021-10-28 16:23:14 +02:00
Leonardo de Moura
3367501511 fix: inaccessible annotations at isDefEq issue 
Issue was reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Change.20in.20pattern.20matching.3B.20expected.20behaviour.3F/near/259059096

fixes #742
 2021-10-27 09:26:12 -07:00
Sebastian Ullrich
b1f7fc1439 fix: CI: copy Homebrew dependencies 2021-10-27 18:16:35 +02:00
Leonardo de Moura
b65da42b7e chore: update stage0 2021-10-26 12:41:23 -07:00