Connor Baker
24cfae2421
doc: fix typo in Lake's Require DSL
2023-08-21 12:43:56 -04:00
Mario Carneiro
ea60ac1443
doc: fix mid priority doc comment
2023-08-21 13:19:43 +02:00
Sebastian Ullrich
63d2bdd490
fix: integer type in llvm_count_params
2023-08-18 19:34:21 +02:00
Sebastian Ullrich
4e52283728
fix: FFI signature mismatches
2023-08-18 19:34:21 +02:00
tydeu
9d05b5f081
feat: warn rather than error if lake.lock disappears
2023-08-17 23:24:11 -04:00
Leonardo de Moura
50bece202b
doc: add RFC questions
2023-08-17 20:23:38 -07:00
Joachim Breitner
6b429fed8f
doc: fix markup in IO.RealWorld ( #2430 )
...
so that
<https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html#IO.RealWorld >
looks good.
2023-08-17 11:55:03 -07:00
Scott Morrison
f1412ddb45
feat: enable failIfUnchanged by default in simp
2023-08-16 10:14:23 -07:00
Scott Morrison
58d19b80b9
test: compiling from the interpreter, with common imports
...
hacky fix to windows test
Include test from #2407 as well
2023-08-16 10:11:50 -07:00
Sebastian Ullrich
f22695fdc5
fix: interpret module initializer at most once
2023-08-16 10:11:50 -07:00
Sebastian Ullrich
d4be21b559
chore: CI: Linux LLVM is not a release
2023-08-16 10:37:30 +02:00
tydeu
6176fdba9e
feat: warn on local changes to dependency & related fixes
2023-08-16 09:44:12 +02:00
tydeu
b328835f4d
fix: lake: reverse-ffi, manifest, and 62 tests
2023-08-15 20:33:09 -04:00
Henrik
35aa2c91a2
feat: LLVM backend: implement the equivalent of -fstack-clash-protection
2023-08-15 14:45:58 +02:00
tydeu
b81224c570
feat: lake update <pkg> & related tweaks
2023-08-15 09:50:39 +02:00
Leonardo de Moura
b5a736708f
fix: fixes #2419
2023-08-14 16:18:30 -07:00
tydeu
736af918f5
doc: IO.Process.getPID tweak + IO.FS.Mode
2023-08-14 18:42:04 +02:00
Tobias Grosser
beddf011d7
chore: update stage0
2023-08-14 13:33:46 +02:00
Siddharth Bhat
496460020a
fix: disabling forwarding --target to lean.
...
This will ensure that we do not invoke `lean --target` without compiling
using LLVM.
2023-08-14 13:33:46 +02:00
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
