Commit graph

21 commits

Author SHA1 Message Date
Henrik Böving
50cfe354be
chore: remove old LEAN_AUTO_THREAD_FINALIZATION workaround (#8885)
This PR removes an old workaround around non-implemented C++11 features
in the thread finalization.

This `ifdef` dates back to approximately 2015 as can be seen
[here](https://github.com/leanprover/lean3/blame/master/src/util/thread.cpp#L177),
the comments mention that it was originally implemented because not all
compilers at the time were able to support the C++11 `thread_local`
keyword. 10 years later this is hopefully the case and we can remove
this workaround.

There is an additional motivation for doing this,
`lean::initialize_thread` contains the following allocation:
```cpp
    g_thread_finalizers_mgr = new thread_finalizers_manager;
```
this is supposed to be freed at some point but:
```cpp
// TODO(gabriel): race condition with thread finalizers
void delete_thread_finalizer_manager() {
    // delete g_thread_finalizers_mgr;
    // g_thread_finalizers_mgr = nullptr;
}
```
so `g_thread_finalizers_mgr` leaks upon repeated invocation of
`lean::initialize_thread`.

Note that Windows has already been using this alternative implementation
for a while so the alternative implementation has (hopefully) not rotten
away in the meantime.
2025-06-20 08:52:17 +00:00
Mac Malone
2e44585ce9
fix: set CP_UTF8 on Windows (#7213)
This PR adds `SetConsoleOutputCP(CP_UTF8)` during runtime initialization
to properly display Unicode on the Windows console. This effects both
the Lean executable itself and user executables (including Lake).

Closes #4291.
2025-02-26 18:36:32 +00:00
Sebastian Ullrich
680ede7a89
fix: set LLVM sysroot consistently (#6574)
This PR actually prevents Lake from accidentally picking up other
toolchains installed on the machine.

Fixes regression introduced in #6176
2025-01-08 12:56:27 +00:00
Sebastian Ullrich
a2a525f5c7
fix: set absolute linker path (#6547)
This PR should prevent Lake from accidentally picking up other linkers
installed on the machine.
2025-01-07 14:06:24 +00:00
Sebastian Ullrich
76f883b999
fix: remove unused -static-libgcc MinGW linker arg (#6535)
This PR avoids a linker warning on Windows.

The argument may have been superfluous ever since the initial
implementation.
2025-01-05 21:57:56 +00:00
Markus Himmel
f0c190239a
feat: compile against Windows SDK headers under Windows (#5753)
Breaking changes:

To build Lean from source on Windows, it is now necessary to install the
[Windows
SDK](https://developer.microsoft.com/en-us/windows/downloads/windows-sdk/).
The build instructions have been updated to reflect this. Note that the
Windows SDK is **not** needed to compile Lean programs using a Lean
toolchain obtained using `elan`. The Windows SDK is only needed to build
Lean itself from source.

Furthermore, we are dropping support for Windows versions older than
Windows 10 1903 (released in May 2019).

No Windows version that is still supported by Microsoft as part of
mainstream support is affected by this.

The following Windows versions are still supported by Microsoft as part
of commercial extended support but are no longer supported by Lean:

- Windows 10 Enterprise LTSC 2015
- Windows 10 Enterprise LTSC 2016
- Windows 10 Enterprise LTSC 2019
- Windows Server 2019
2024-10-22 13:00:02 +00:00
Henrik Böving
9b6696be1d
feat: use libuv for tempfiles (#5135)
This is currently broken because of linker issues. CC @TwoFX

---------

Co-authored-by: Markus Himmel <markus@lean-fro.org>
2024-10-14 13:56:56 +00:00
Markus Himmel
c237c1f9fb
feat: link LibUV (#4963) 2024-08-12 12:33:24 +00:00
Henrik
8d3af73853 feat: Linux LLVM CI for stage1+ 2023-08-14 13:33:46 +02:00
Siddharth
4d47c8abc6
feat: add LLVM C API bindings (#1497)
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2022-11-21 09:50:01 +01:00
Siddharth
e3f064ef87
Bump up to LLVM 15 (#1691) 2022-10-14 14:43:13 +00:00
Sebastian Ullrich
c755aa81bd fix: properly distinguish between internal and public linker flags 2022-05-02 13:53:52 +02:00
Sebastian Ullrich
bba0baf92c chore: CI: I'm sure they work fine 2022-03-22 12:22:23 +01:00
Sebastian Ullrich
82049c519c chore: CI: fix MinGW library root 2022-03-22 12:22:23 +01:00
Sebastian Ullrich
f3279824a3 fix: Windows: do not use standard sysroot 2022-01-30 17:43:14 +01:00
Sebastian Ullrich
ccf1292e07 fix: rework header/lib handling with bundled clang
* use `-nostdinc` to make sure system headers don't affect us
* include clang headers with `-isystem`, which suppresses all those warnings
* do not use default sysroot on Windows after all, since that can be a
  surprising location

Fixes #922
2022-01-20 16:05:54 +01:00
Sebastian Ullrich
068ea1beb4 fix: leanc: do not change sysroot
Apparently clang is smart enough to look up runtime files missing from
the sysroot in the installation directory automatically.
2021-12-19 18:55:57 +01:00
Sebastian Ullrich
8f88b1f3f8 feat: bundle llvm-ar with Lean 2021-11-25 15:05:06 +01:00
Sebastian Ullrich
99aee53172 fix: restore macOS compile flags 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
74a616a965 chore: final cleanup? 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
3db3fb1429 feat: bundle LLVM on Windows 2021-11-18 09:42:35 +01:00