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

31535 commits

This branch
This branch
All branches
Author SHA1 Message Date
tydeu
28f7334139 chore: .gitignore fixes 2023-08-02 04:03:56 -04:00
tydeu
e330a57036 test: fix 62/116/buildArgs 2023-08-02 04:03:56 -04:00
tydeu
86f11311ba test: merge examples/git and test/104 & use local test repo 2023-08-02 04:03:56 -04:00
tydeu
5c8093eaff chore: delete Lake's .github directory 2023-08-02 04:03:56 -04:00
tydeu
de3b198676 fix: use exe over lib & add missing opts from lib config to exe 2023-08-02 04:03:56 -04:00
tydeu
bb5cf96664 fix: fetch target type signatures 2023-08-02 04:03:56 -04:00
tydeu
6721150367 refactor: touchup DSL target docstrings & reorg 2023-08-02 04:03:56 -04:00
Siddharth
b9ec36d089
chore: get rid of all inline C annotations for LLVM (#2363) 2023-07-30 10:39:40 +02:00
Sebastian Ullrich
2eaa400b8e
fix: do not unnecessarily wait on additional snapshot in server request handlers (#2370) 
Co-authored-by: Wojciech Nawrocki <wjnawrocki+gh@protonmail.com>
 2023-07-30 05:58:46 +00:00
Mario Carneiro
9c910ebe8e perf: faster replace "\r\n" "\n" 2023-07-29 17:31:48 -04:00
Siddharth
a436c225d8
chore: disable lake 116 test (#2358) 
The test is flaky due to the presence of a fixed 'sleep()'.

The LLVM backend has introduced a performance
regression in Lake which causes this test to fail, as the
current sleep duration of 3s is insufficient.
Further investigation into the performance regression is pending.

We decided to disable the `leanlaketest_116` entirely on account
of the test being flaky by construction
(https://github.com/leanprover/lean4/pull/2358#issuecomment-1655371232).
 2023-07-29 09:40:18 +00:00
Sebastian Ullrich
8fc1af650a fix: symmetry in orelse antiquotation parsing 2023-07-28 08:36:33 -07:00
Sebastian Ullrich
eceac9f12a perf: avoid syntax stack copy at orelseFn 2023-07-28 08:36:33 -07:00
Scott Morrison
b3fa4fd053 chore: revert #2317 2023-07-28 08:33:49 -07:00
Wojciech Nawrocki
74e0f09009
fix: handle error in withTraceNode message action (#2364) 
* fix: handle error in withTrace message action

* Update src/Lean/Util/Trace.lean

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

* Update Trace.lean

---------

Co-authored-by: Gabriel Ebner <gebner@gebner.org>
 2023-07-28 08:01:13 -07:00
Sebastian Ullrich
aeb60764c1 feat: auto-complete declaration names in arbitrary namespaces 2023-07-28 07:50:09 -07:00
Sebastian Ullrich
687f50ab33 fix: never show private names in completion 2023-07-28 07:50:09 -07:00
Sebastian Ullrich
e84ce2e1f1 test: make completion tests less dependent on core 2023-07-28 07:50:09 -07:00
Sebastian Ullrich
b15d6d41b8 fix: missing mkCIdents in Lean.Elab.Deriving.Util 2023-07-28 07:48:34 -07:00
Sebastian Ullrich
8ffb389f3f chore: Nix bump to LLVM 15 
Also update mdbook dependency hash from nixpkgs bump.

Peeled from https://github.com/leanprover/lean4/pull/2340
to enable LLVM for stage1+ builds.
 2023-07-28 10:56:54 +02:00
Mario Carneiro
776bff1948 fix: repeat conv should not auto-close the goal 2023-07-27 18:15:35 -04:00
Sebastian Ullrich
53477089fe chore: remove unused macOS dependencies 2023-07-26 15:36:36 +02:00
Sebastian Ullrich
132f655736 chore: add zlib search path on macOS only when linking libleanshared 2023-07-26 15:36:36 +02:00
Sebastian Ullrich
978a5b2528 fix: loading libc++ on macOS Sonoma 2023-07-26 15:36:36 +02:00
Siddharth Bhat
96c59ccced chore: update stage0 2023-07-25 11:03:16 +02:00
Siddharth Bhat
073c8fed86 feat: LLVM backend: support for visibility Style & DLL storage 
Changes peeled from:
https://github.com/leanprover/lean4/pull/2340

to allow a `stage0` bump on master before merging in the
changes that allow LLVM to build in stage1+.
 2023-07-25 11:03:16 +02:00
Alex J Best
808bb9b579
perf: dont repeatedly elab term in rw at multiple locations #2317 2023-07-24 08:47:52 -07:00
Bulhwi Cha
3b6bc4a87d style: remove unnecessary space characters 2023-07-23 16:11:11 +02:00
Mario Carneiro
dd313c6894 feat: add IO.FS.rename 2023-07-22 23:21:32 +02:00
Bulhwi Cha
7809d49a62 doc: fix type signature of Coe 2023-07-22 14:16:21 +02:00
Sebastian Ullrich
544b704a25 test: add Lake tests 2023-07-21 09:19:19 +02:00
Sebastian Ullrich
d991f5efe0 fix: ship libLake.a 2023-07-21 09:19:19 +02:00
Sebastian Ullrich
e2fbfb5731 chore: remove Lake flake 
Fixes leanprover/lake#165
 2023-07-21 09:19:19 +02:00
Sebastian Ullrich
8999ef067b chore: Nix: fixup Lake integration 2023-07-21 09:19:19 +02:00
Jannis Limperg
6407197e54 chore: better error message for loose bvar in whnf 2023-07-20 13:47:20 -07:00
Bulhwi Cha
367b38701f
refactor: simplify String.splitOnAux (#2271) 2023-07-19 11:50:27 +00:00
Wojciech Nawrocki
e1b3f10250 doc: fix contradictory docstring 2023-07-19 10:53:47 +02:00
F. G. Dorais
d10e3da673 fix: protect sizeOf lemmas 2023-07-19 08:50:59 +02:00
Sebastian Ullrich
d62fca4e9c chore: safer bench script 2023-07-19 08:31:39 +02:00
Leonardo de Moura
634193328b fix: fixes #2327 2023-07-18 07:18:27 -07:00
Sebastian Ullrich
daae36d44d chore: remove obsolete file 2023-07-17 10:38:35 +02:00
Sebastian Ullrich
c35e41ce15 chore: Nix: add lake executable 2023-07-17 10:38:35 +02:00
Sebastian Ullrich
90aab46071 chore: fix update-stage0 2023-07-17 10:38:35 +02:00
Sebastian Ullrich
bf76eca0cd chore: merge Lake into src/lake 2023-07-17 10:38:20 +02:00
Sebastian Ullrich
9a3657df3f chore: remove Lake submodule 2023-07-15 12:03:41 +02:00
tydeu
d37bbf4292 chore: update Lake 2023-07-14 23:43:04 -04:00
Floris van Doorn
1a6663a41b
chore: write "|-" as "|" noWs "-" (#2299) 
* remove |- as an alias for ⊢

* revert false positive |->

* fix docstring

* undo previous changes

* [unchecked] use suggestion

* next attempt

* add test
 2023-07-14 09:48:20 -07:00
Leonardo de Moura
212cd9c3e6 fix: fixes #2321 2023-07-13 14:41:32 -07:00
Scott Morrison
0d5c5e0191 feat: relax test in checkLocalInstanceParameters to allow instance implicits 2023-07-13 10:54:06 -07:00
Scott Morrison
7213ff0065
doc: document generating releases via tags (#2302) 2023-07-13 17:39:54 +02:00