36 Commits

Author SHA1 Message Date
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
Markus Himmel
d835616573 chore: fix MSYS2 build instructions (#5617) 2024-10-07 12:42:37 +00:00
Markus Himmel
c237c1f9fb feat: link LibUV (#4963) 2024-08-12 12:33:24 +00:00
Sebastian Ullrich
73a0c73c7c chore: modernize build instructions (#4032)
Use `cmake --preset`, adjust and document parallelism settings
2024-05-23 10:55:07 +00:00
Sebastian Ullrich
d2c626e158 doc: refine development manual 2022-04-05 16:03:24 +02:00
Chris Lovett
6dc576121d doc: replace quickstart leanpkg info with info about lake 2022-03-11 16:31:58 -08:00
Sebastian Ullrich
dbdb92a411 doc: advise using Developer Mode on Windows 2021-11-19 10:09:26 +01:00
Chris Lovett
3a20b6be8a doc: add wsl setup docs and reorganize a new "dev" folder 2021-09-23 09:21:39 +02: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
Chris Lovett
1591bb1640 doc: fix msys text based on code review feedback 2021-09-10 10:07:57 +02:00
Chris Lovett
bc3900cbb9 doc: small fixes 2021-09-07 19:19:58 -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
440abd4bd1 chore: CI: switch to GCC on Windows for now
See discussion at https://github.com/leanprover/lean4/pull/555
2021-08-18 13:54:52 +02:00
Sebastian Ullrich
d5f58d27b0 chore: delete StyleCheck 2020-10-14 19:07:52 +02:00
Sebastian Ullrich
589afc4095 doc: wording 2020-08-25 16:12:19 +02:00
mhuisi
21d176c1ea doc: correct msys2 build instructions 2020-08-25 16:08:58 +02:00
Sebastian Ullrich
1756d31694 chore: update build instructions 2020-03-25 12:45:52 +01:00
Sebastian Ullrich
74eda000b4 doc(doc/make/msys2): update instructions 2019-07-05 11:24:15 +02:00
Sebastian Ullrich
7644de75d8 chore(doc/make/msys2): link generic build instructions 2018-02-01 10:46:12 +01:00
Sebastian Ullrich
19f8bfd9eb chore(doc/make): add platform-generic build instructions 2018-01-23 11:14:18 -08:00
Corey Richardson
eda6660b2d doc(msys2): add notes about installation 2017-06-30 08:04:14 +02:00
Leonardo de Moura
7eef501ae1 chore(*): remove mpfr dependency
closes #1380
2017-02-17 20:36:53 -08:00
Andrew Ashworth
3153b72415 fix(doc/make/msys2): incorrect build instructions
-D CMAKE_BUILD_TYPE=Release does nothing since the default build type is Release. Also, it should be enclosed in quotes "-D CMAKE_BUILD_TYPE=Release", otherwise the shell/cmake fails to properly interpret the arguments.
2016-12-15 10:07:01 -08:00
Leonardo de Moura
8e64665259 chore(src/CMakeLists): remove support for optional Boost 2016-12-03 11:34:58 -08:00
Gabriel Ebner
b7e781684f chore(doc/make/msys2): update msys2 build instructions 2016-12-02 17:01:58 -08:00
Gabriel Ebner
92f07720f2 refactor(emacs/load-lean): install emacs dependencies directly from (M)ELPA 2016-12-02 16:50:50 -08:00
Leonardo de Moura
222f4af898 chore(doc/make/msys2): add Win 10 2016-12-01 13:54:25 -08:00
Leonardo de Moura
f7e8e73186 fix(doc/make/msys2): we don't need lua anymore 2016-12-01 13:53:15 -08:00
Gabriel Ebner
db67c1fde3 chore(CMakeLists): make python dependency optional 2016-11-30 11:27:02 -05:00
Leonardo de Moura
6616f661f9 chore(doc/make/msys2): Remove Lua from installation instructions 2016-11-16 15:57:19 -08:00
Leonardo de Moura
fa7a527590 feat(doc/make/msys2): add emacs-dependencies 2015-07-20 17:32:20 -07:00
Soonho Kong
651345a89b doc(make/msys2.md): remove msys2's Python, add how to install native one
[skip ci]
2015-05-12 13:03:51 -04:00
Soonho Kong
4350382b90 doc(make/msys2): update instructions 2014-10-06 15:13:24 -07:00
Soonho Kong
fd11b28d15 doc(make/msys2): update instructions 2014-10-02 17:25:12 -07:00
Leonardo de Moura
fff0c2f84a doc(make/msys2): instructions for building native windows Lean binary 2014-09-26 16:26:32 -07:00