Commit graph

730 commits

Author SHA1 Message Date
Siddharth Bhat
dfb5548cab fix: update libleanrt.bc, rename to lean.h.bc
This adds `lean.h.bc`, a LLVM bitcode file of the Lean
runtime that is to be inlined. This is programatically generated.

1. This differs from the previous `libleanrt.ll`, since it produces an
   LLVM bitcode file, versus a textual IR file. The bitcode file
   is faster to parse and build an in-memory LLVM module from.
2. We build `lean.h.bc` by adding it as a target to `shell`,
   which ensures that it is always built.

3. We eschew the need for:

```cpp
```

which causes breakage in the build, since changing the meaning of
`static` messes with definitions in the C++ headers.

Instead, we build `lean.h.bc` by copying everything in
`src/include/lean/lean.h`, renaming `inline` to
`__attribute__(alwaysinline)` [which forces LLVM to generate
`alwaysinline` annotations], then running the `-O3` pass pipeline
to get reasonably optimised IR, and will be perfectly inlined
when linked into the generated LLVM code by
`src/Lean/Compiler/IR/EmitLLVM.lean`.

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2022-11-28 16:20:12 +01:00
Sebastian Ullrich
c112ae7c58 test: fix Lake rename 2022-11-28 15:12:18 +01:00
Siddharth
48b6fee467
chore: remove stray STATIC in src/shell (#1736) 2022-10-15 14:27:13 +02:00
Sebastian Ullrich
4a9bc88a4e chore: fix USE_GMP=OFF by removing GMP linking customization 2022-03-26 16:29:52 +01:00
Leonardo de Moura
52a52fbed7 chore: add doc/examples to the test suite 2022-03-24 15:20:18 -07:00
Sebastian Ullrich
8cbd7ccf09 test: reimplement package tests using Lake 2022-02-09 12:21:11 -08:00
Sebastian Ullrich
a7ba103e0a chore: remove leanpkg 2022-02-04 19:03:40 +01:00
Leonardo de Moura
d953ac8d0d feat: allow users to use initialize registerBuiltinDerivingHandler ... 2022-01-11 09:50:09 -08:00
Leonardo de Moura
448bac5b3e chore: one add_test per lake test 2021-12-14 11:48:14 -08:00
Sebastian Ullrich
7333de1766 refactor: cmake: make more use of string(APPEND)
I guess CMake might not actually be that painful if one was motivated to
learn it

```
sed -Ei 's/set\(([A-Z_]+) "\$\{\1\}/string(APPEND \1 "/' src/**/CMakeLists.txt
```
2021-11-18 10:09:55 +01:00
Sebastian Ullrich
db5b150b38 chore: do not use bundled compiler for foreign test 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
09d549aecd chore: fix foreign test on macOS, again 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
d2a1e20dd0 feat: bundling LLVM on Linux 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
a345a98ef7 chore: fix foreign test on macOS 2021-11-09 11:03:14 +01:00
Sebastian Ullrich
d7b8479760 chore: use configured C++ compiler for foreign test
Fixes #775
2021-11-09 09:27:10 +01:00
Sebastian Ullrich
697e34e229 test: --load-dynlib 2021-11-04 15:32:07 -07:00
Leonardo de Moura
f01a124f18 fix: builtin attribute initialization
The failure was triggered if a module declared (only) builtin
attributes that do not have any persistent extension associated with
them.

Fixes #726
2021-10-20 13:55:54 -07:00
Sebastian Ullrich
89f9045646 test: add lake tests 2021-10-15 06:56:02 -07:00
Chris Lovett
ad7c5b26a7
fix: UTF-8 file path support for lean on Windows
* fix msys2 windows build so the windows apps support utf-8 file paths.

* use windres to compile default-manifest.o

* windres is in binutils.

* stop modifying default-manifest.o

* copy to stage0

* fix semicolon joining of lists in add_custom_target

* undo changes to stage0 as per CR feedback.

* fix makefile

* fix: revert cmakelists.txt COMMAND_EXPAND_LISTS  change

* fix: msys2 dependencies

* add unit test for decoding UTF-8 chars to prove "lean.exe" can read utf-8 encoded files where utf-8 is also used in the file name.

* fix: utf-8 test by using windows-2022

* fix: do we really need cmake 3.11 or will 3.10 do?

* nope, really does require cmake 11.
2021-09-22 12:21:52 +02:00
Sebastian Ullrich
130eac1b77 chore: reintroduce lean.cpp in separate commit so Git doesn't freak out 2021-09-16 07:03:37 -07:00
Sebastian Ullrich
b3bb2bac97 chore: move all C++ code into libleanshared, use C stub for main
Avoids any issues with cross-lib C++
2021-09-16 07:03:37 -07:00
Sebastian Ullrich
c5940f0149 fix: cmake/make dependencies 2021-09-09 18:12:55 +02:00
Sebastian Ullrich
2159a90c8c fix: lean target dependencies
Fixes #661
2021-09-09 11:55:33 +02:00
Sebastian Ullrich
68a3799b7c refactor: build lean in stdlib.make 2021-09-08 17:24:31 +02:00
Sebastian Ullrich
9702fe1981 chore: leanc: use C instead of C++ compiler 2021-09-08 17:24:31 +02:00
Sebastian Ullrich
3787c6081c fix: pass worker cmdline options to Lean code 2021-09-08 11:34:31 +02:00
Leonardo de Moura
c8406a301d chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
Sebastian Ullrich
5f4b1b1d44 Revert "Revert "feat: reintroduce libleanshared, link lean & leanpkg against it""
This reverts commit ccbc9d00db.
2021-08-20 09:42:05 -07:00
Sebastian Ullrich
ccbc9d00db Revert "feat: reintroduce libleanshared, link lean & leanpkg against it" 2021-08-20 15:39:00 +02:00
Sebastian Ullrich
f33cdf6bf9 fix: linking against dl 2021-08-19 19:44:28 +02:00
Sebastian Ullrich
09a0347fdc chore: fix compilation of executables containing code to be interpreted 2021-08-18 13:54:52 +02:00
Sebastian Ullrich
1ed329b305 test: try reenabling plugin test on Windows 2021-08-18 13:54:52 +02:00
Sebastian Ullrich
6827928594 chore: cpack: copy required libraries via ldd/otool 2021-08-18 13:54:52 +02:00
Sebastian Ullrich
68ecda843b chore: remove STATIC cmake flag 2021-08-18 13:54:52 +02:00
Sebastian Ullrich
617f17facb feat: reintroduce libleanshared, link lean & leanpkg against it 2021-08-18 13:54:52 +02:00
Sebastian Ullrich
fc707f3343 test: fix test on Windows 2021-08-17 12:50:58 +02:00
Leonardo de Moura
d775dc6195 feat: add flag for controlling the execution of initialize commands when importing modules programmatically
Fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Environment.20extensions.20in.20importModules
2021-08-16 17:43:28 -07:00
Leonardo de Moura
81ff285427 chore: use leanmake instead of leanpkg 2021-08-16 08:52:27 -07:00
Sebastian Ullrich
917eb4d081 chore: collect stdlib compilation flags in new header 2021-08-12 07:51:50 -07:00
Sebastian Ullrich
0aaab9e024 chore: remove file_lock.h 2021-08-04 16:40:57 +02:00
Leonardo de Moura
01d902f905 feat: add register_option command
User-defined options.
2021-08-03 14:31:04 -07:00
Leonardo de Moura
d864afae91 feat: private fields
closes #418
2021-08-02 20:20:21 -07:00
Leonardo de Moura
a77598f7cf feat: user-defined attributes
See new test for an example.

closes #513
2021-07-26 18:24:10 -07:00
Leonardo de Moura
cdd1dbbb36 feat: user-defined environment extensions
New test demonstrates how to use them.
The user-defined extensions cannot be used in the same file where they
were declared because the `initialize` commands are only executed when
we import the modules containing them.

TODO: user-defined attributes.
2021-07-26 16:18:48 -07:00
Sebastian Ullrich
a006558bb3 chore: search for llvm-config in PATH instead of LLVM_TOOLS_BINARY_DIR
...because it is not there with Nix
2021-07-09 11:00:58 +02:00
Sebastian Ullrich
5c07c188b4 feat: generate LLVM module of runtime 2021-07-09 11:00:58 +02:00
Sebastian Ullrich
b3535e4e3e fix: LLVM setup 2021-06-18 12:24:43 +02:00
Wojciech Nawrocki
e6b2818169 chore: fixes 2021-06-15 22:53:19 +02:00
Wojciech Nawrocki
12a4ef54a9 chore: document io_mark_end_initialization setup 2021-06-13 17:32:35 -07:00
Wojciech Nawrocki
bf41d40b1d fix: allow plugins to run IO initializers 2021-06-13 17:32:35 -07:00