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

31573 commits

This branch
This branch
All branches
Author SHA1 Message Date
Henrik
8d3af73853 feat: Linux LLVM CI for stage1+ 2023-08-14 13:33:46 +02:00
Siddharth Bhat
146296b5fa feat: enable LLVM in stage1+ compiler 2023-08-14 13:33:46 +02:00
Siddharth Bhat
0054f6bfac feat: link 'llvm.h.bc' and then set linkage to internal 
This obviates the need to play weak linkage games when
we build `lean.h.bc` from `lean.h`. We perform the following steps:

1. We remove the `static` modifier from all definitions in `lean.h`.
   This makes all definitions have `extern` linkage. Thus, when we build
   a `lean.h.bc` using `clang`, we will actually get definitions
   (instead of an empty file)
2. We build `lean.h.bc` from `lean.h` using `clang`.
3. When it comes time to link, we link
   `current_module.bc := LLVMLinkModules2(current_module.bc, lean.h.bc)`.
4. We loop over every symbol that arrived from `lean.h.bc`
   in `current_module.bc` and we then set this symbol to have
   `internal` linkage. This simulates the effect of
   `#include <lean.h>` where every definition in `lean.h`
   has internal linkage.

This yajna, one hopes, pleases the linker gods.
 2023-08-14 13:33:46 +02:00
Leonardo de Moura
fac9e64cdf chore: update stage0 2023-08-13 09:56:29 -07:00
Scott Morrison
61fea57e73 feat: add failIfUnchanged flag to simp 2023-08-13 09:49:25 -07:00
Tobias Grosser
736a21cd5a chore: remove trailing whitespaces in EmitLLVM 
For some reason, these two were missed in the last commit.
 2023-08-13 16:18:23 +02:00
Tobias Grosser
d90176af71 chore: remove trailing whitespaces in CMakeLists.txt 2023-08-13 16:18:23 +02:00
Tobias Grosser
a0c0c486fd chore: remove trailing whitespace in EmitLLVM 
This patch should not result in any functional changes, but
will reduce the diff of an upcoming PR.
 2023-08-13 11:07:14 +02:00
Siddharth Bhat
0eddc167b9 feat: LLVM linkage bindings 2023-08-12 16:51:58 +02:00
Leonardo de Moura
dce7f71126 chore: clarify/fix contribution guidelines 2023-08-11 14:48:50 -07:00
Sebastian Ullrich
ff45efe3fa doc: one more enableInitializersExecution remark 2023-08-11 11:45:58 -07:00
Leonardo de Moura
133e03ce7f feat: update external contribution guidelines 2023-08-11 11:39:41 -07:00
tydeu
510bc47cc3 fix: delete lake.lock on error & test 2023-08-11 02:29:06 -04:00
tydeu
06853e5c3b fix: lake: lock test timeout + README typos 2023-08-10 12:17:47 -04:00
tydeu
75a9284320 feat: lake: lean lib extraDepTargets & related tweaks 2023-08-09 20:25:43 -04:00
Junyan Xu
2aeeed13cf
fix: generalize Prod.lexAccessible to match Lean 3 (#2388) 
* fix: generalize Prod.lexAccessible to match Lean 3

* fix

* fix
 2023-08-09 08:54:53 -07:00
Marcus Rossel
8af25455ae doc: fix comment for Nat.sub 2023-08-09 08:54:24 -07:00
Sebastian Ullrich
befc4b997b doc: writing good tests 2023-08-09 08:52:55 -07:00
tydeu
e7a1512da8 doc: lake: update README target signatures 2023-08-08 21:42:07 -04:00
tydeu
63d303558d test: lake clean 2023-08-08 21:42:07 -04:00
tydeu
4c04690c24 fix: -d option for lake print-paths + test 2023-08-08 21:42:07 -04:00
tydeu
874d44a26e feat: lake clean <pkgs> 2023-08-08 21:42:07 -04:00
tydeu
3e4232c204 feat: lake.lock file for builds 2023-08-08 16:23:43 -04:00
tydeu
c79c7c89b3 feat: IO.Process.getPID & IO.FS.Mode.writeNew 2023-08-08 16:23:43 -04:00
tydeu
a315fdceb3 test: lake: make 116 deterministic & related tweaks 2023-08-08 16:21:28 -04:00
Sebastian Ullrich
bb738796ae test: update parser benchmark, add to speedcenter suite 2023-08-08 18:40:19 +02:00
tydeu
8de1c0786c chore: make Lean build shell configurable 2023-08-07 23:05:37 +02:00
Eric Wieser
1f3ef28a1d fix: correct universe polymorphism in Lean.instFromJsonProd 
The previous type was
```
Lean.instFromJsonProd.{u, v} {α β : Type (max u v)} [FromJson α] [FromJson β] :
  FromJson (α × β)
```
where universe metavariable assignment assigned the wrong universe to both types!
 2023-08-06 07:32:30 -07:00
Sebastian Ullrich
254582c000 doc: link to FFI examples 2023-08-04 10:45:53 +02:00
Sebastian Ullrich
f19f329b4c test: reverse FFI from C with Lake 2023-08-04 10:45:53 +02:00
tydeu
98da3c9e46 fix: lake: do not hash remote dep names + test 
accidental leftover from a scrapped feature
 2023-08-03 21:21:28 -04:00
Scott Morrison
ca4d824d75 chore: correct doc-string for elabTerm 2023-08-03 06:52:08 -07:00
tydeu
125a0ba798 chore: lake: adapt versioning to Lean repo & bump to v5.0.0 2023-08-03 01:09:18 -04:00
tydeu
0aa570044a fix: lake: distinct lib and precompile lib names for roots 2023-08-03 01:09:18 -04:00
tydeu
bb8259b9af feat: lake: warn on mismatch pkg name and require name 
see #2324
 2023-08-03 01:09:18 -04:00
tydeu
35bad47c1b refactor: lake: cleanup source materialization 2023-08-03 01:09:18 -04:00
Sebastian Ullrich
17602d9f28 chore: avoid "unused parameter" warnings in lean.h 2023-08-02 10:20:57 +02:00
tydeu
5fb42eb5c1 fix: include extraDepJob in module trace 2023-08-02 04:03:56 -04:00
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