mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
chore(doc/make): add platform-generic build instructions
This commit is contained in:
Sebastian Ullrich
committed by
Leonardo de Moura
Leonardo de Moura
parent
3a1ede2d73
commit
19f8bfd9eb
13
README.md
13
README.md
@@ -22,19 +22,10 @@ About
|
||||
- [FAQ](doc/faq.md)
|
||||
- For HoTT mode, please use [Lean2](https://github.com/leanprover/lean2).
|
||||
|
||||
Requirements
|
||||
Installation
|
||||
------------
|
||||
|
||||
- C++11 compatible compiler
|
||||
- [CMake](http://www.cmake.org)
|
||||
- [GMP (GNU multiprecision library)](http://gmplib.org/)
|
||||
|
||||
Build Instructions
|
||||
------------------
|
||||
|
||||
- [Linux (Ubuntu)](doc/make/ubuntu-16.04.md)
|
||||
- [Windows (msys2)](doc/make/msys2.md)
|
||||
- [macOS](doc/make/osx-10.9.md)
|
||||
Stable and nightly binary releases of Lean are available on the [homepage](http://leanprover.github.io/downloads). For building Lean from source, see the [build instructions](doc/make/index.md).
|
||||
|
||||
Miscellaneous
|
||||
-------------
|
||||
|
||||
@@ -1,17 +0,0 @@
|
||||
Using [CMake][cmake] + Make
|
||||
---------------------------
|
||||
Instructions for DEBUG build
|
||||
|
||||
mkdir -p build/debug
|
||||
cd build/debug
|
||||
cmake -DCMAKE_BUILD_TYPE=DEBUG ../../src
|
||||
make
|
||||
|
||||
Instructions for RELEASE build
|
||||
|
||||
mkdir -p build/release
|
||||
cd build/release
|
||||
cmake -DCMAKE_BUILD_TYPE=RELEASE ../../src
|
||||
make
|
||||
|
||||
[cmake]: http://www.cmake.org/
|
||||
@@ -1,25 +0,0 @@
|
||||
Using [CMake][cmake] + [Ninja][ninja]
|
||||
-------------------------------
|
||||
[CMake 2.8.11][cmake] supports [Ninja][ninja] build system using
|
||||
``-G`` option. [Some people report][ninja_work] that using
|
||||
[Ninja][ninja] can reduce the build time, esp when a build is
|
||||
incremental.
|
||||
|
||||
[ninja_work]: https://plus.google.com/108996039294665965197/posts/SfhrFAhRyyd
|
||||
|
||||
Instructions for DEBUG build
|
||||
|
||||
mkdir -p build/debug
|
||||
cd build/debug
|
||||
cmake -DCMAKE_BUILD_TYPE=DEBUG -G Ninja ../../src
|
||||
ninja
|
||||
|
||||
Instructions for RELEASE build
|
||||
|
||||
mkdir -p build/release
|
||||
cd build/release
|
||||
cmake -DCMAKE_BUILD_TYPE=RELEASE -G Ninja ../../src
|
||||
ninja
|
||||
|
||||
[cmake]: http://www.cmake.org/
|
||||
[ninja]: http://martine.github.io/ninja/
|
||||
@@ -1,14 +0,0 @@
|
||||
Install Packages on Fedora 19
|
||||
-----------------------------
|
||||
|
||||
Instructions for installing git, cmake, gmp, gperftools on Fedora
|
||||
|
||||
sudo yum install -y git cmake gmp-devel gperftools-devel
|
||||
|
||||
Instructions for installing gcc-4.8 (C++11 compatible) on Fedora
|
||||
|
||||
sudo yum install -y gcc-c++
|
||||
|
||||
Instructions for installing clang-3.3 (C++11 compatible) on Fedora
|
||||
|
||||
sudo yum install -y clang-devel
|
||||
71
doc/make/index.md
Normal file
71
doc/make/index.md
Normal file
@@ -0,0 +1,71 @@
|
||||
Requirements
|
||||
------------
|
||||
|
||||
- C++11 compatible compiler
|
||||
- [CMake](http://www.cmake.org)
|
||||
- [GMP (GNU multiprecision library)](http://gmplib.org/)
|
||||
|
||||
Platform-Specific Setup
|
||||
-----------------------
|
||||
|
||||
- [Linux (Ubuntu)](ubuntu-16.04.md)
|
||||
- [Windows (msys2)](msys2.md)
|
||||
- [macOS](osx-10.9.md)
|
||||
|
||||
Generic Build Instructions
|
||||
--------------------------
|
||||
|
||||
Setting up a basic release build using `make`:
|
||||
|
||||
```bash
|
||||
git clone https://github.com/leanprover/lean
|
||||
cd lean
|
||||
mkdir -p build/release
|
||||
cd build/release
|
||||
cmake ../../src
|
||||
make
|
||||
```
|
||||
|
||||
Setting up a basic debug build using `make`:
|
||||
|
||||
```bash
|
||||
git clone https://github.com/leanprover/lean
|
||||
cd lean
|
||||
mkdir -p build/debug
|
||||
cd build/debug
|
||||
cmake -D CMAKE_BUILD_TYPE=DEBUG ../../src
|
||||
make
|
||||
```
|
||||
|
||||
Useful CMake Configuration Settings
|
||||
-----------------------------------
|
||||
|
||||
Pass these along with the `cmake ../../src` command.
|
||||
|
||||
* `-G Ninja`
|
||||
CMake 2.8.11 supports the [Ninja][https://ninja-build.org/] build system.
|
||||
[Some people report][ninja_work] that using
|
||||
Ninja can reduce the build time, esp when a build is
|
||||
incremental. Call `ninja` instead of `make` to build the project.
|
||||
|
||||
[ninja_work]: https://plus.google.com/108996039294665965197/posts/SfhrFAhRyyd
|
||||
|
||||
* `-D CMAKE_BUILD_TYPE=`
|
||||
Select the build type. Valid values are `RELEASE` (default), `DEBUG`,
|
||||
`RELWITHDEBINFO`, and `MINSIZEREL`.
|
||||
|
||||
* `-D CMAKE_CXX_COMPILER=`
|
||||
Select the C++ compiler to use.
|
||||
|
||||
* `-D LEAN_IGNORE_OLEAN_VERSION`
|
||||
The `.olean` files are tagged with the Lean version they were produced with.
|
||||
This means that by default, the core library has to be recompiled after e.g.
|
||||
every `git commit`. Use this option to avoid the version check. The `.olean`
|
||||
files can be removed manually by invoking `make/ninja clean-olean`.
|
||||
|
||||
Further Information
|
||||
-------------------
|
||||
|
||||
- [Using CCache](ccache.md) to avoid recompilation
|
||||
- [Measuring Code Coverage](coverage.md)
|
||||
- [Compiling Lean with Split Stacks](split-stack.md)
|
||||
@@ -22,17 +22,7 @@ Here are the commands to install all dependencies needed to compile Lean on your
|
||||
pacman -S mingw-w64-x86_64-gcc mingw-w64-x86_64-ninja mingw-w64-x86_64-cmake git
|
||||
```
|
||||
|
||||
## Build Lean
|
||||
|
||||
In the [msys2] shell, execute the following commands.
|
||||
|
||||
```bash
|
||||
git clone https://github.com/leanprover/lean
|
||||
cd lean
|
||||
mkdir build && cd build
|
||||
cmake ../src -G Ninja
|
||||
ninja
|
||||
```
|
||||
Then follow the generic build instructions in the [msys2] shell.
|
||||
|
||||
## Install lean
|
||||
|
||||
|
||||
@@ -40,17 +40,7 @@ Required Packages: CMake, GMP
|
||||
brew install gmp
|
||||
|
||||
|
||||
Optional Packages: tcmalloc and ninja
|
||||
-------------------------------------
|
||||
Optional Packages: ninja
|
||||
------------------------
|
||||
|
||||
brew install gperftools
|
||||
brew install ninja
|
||||
|
||||
# Build
|
||||
```bash
|
||||
cd lean
|
||||
mkdir -p build/release
|
||||
cd build/release
|
||||
cmake ../../src
|
||||
make
|
||||
```
|
||||
|
||||
@@ -1,77 +0,0 @@
|
||||
Preparing working environment on Ubuntu 12.04
|
||||
---------------------------------------------
|
||||
|
||||
### Install basic packages
|
||||
|
||||
sudo apt-get install git
|
||||
sudo apt-get install libgmp-dev
|
||||
sudo add-apt-repository ppa:kalakris/cmake -y
|
||||
sudo apt-get install cmake
|
||||
|
||||
sudo add-apt-repository ppa:ubuntu-toolchain-r/test -y
|
||||
sudo update-alternatives --remove-all gcc
|
||||
sudo update-alternatives --remove-all g++
|
||||
sudo apt-get update
|
||||
sudo apt-get install g++-4.8 -y
|
||||
sudo apt-get upgrade -y && sudo apt-get dist-upgrade -y
|
||||
|
||||
sudo ln -s /usr/bin/g++-4.8 /usr/bin/g++
|
||||
|
||||
### Optional packages
|
||||
|
||||
sudo apt-get install gitg
|
||||
sudo apt-get install valgrind
|
||||
sudo apt-get install doxygen
|
||||
sudo apt-get install kcachegrind
|
||||
|
||||
### Fork Lean on github : https://github.com/leanprover/lean
|
||||
|
||||
### Create a projects directory
|
||||
|
||||
cd ~
|
||||
mkdir projects
|
||||
cd projects
|
||||
|
||||
### Clone your fork
|
||||
|
||||
git clone https://github.com/[your-user-name]/lean.git
|
||||
|
||||
### Build Lean in debug mode
|
||||
|
||||
cd lean
|
||||
mkdir -p build/debug
|
||||
cd build/debug
|
||||
cmake -D CMAKE_BUILD_TYPE=Debug ../../src
|
||||
make
|
||||
|
||||
### If you are using Emacs, here are some basic configurations
|
||||
|
||||
(custom-set-variables
|
||||
'(c-basic-offset 4)
|
||||
'(global-font-lock-mode t nil (font-lock))
|
||||
'(show-paren-mode t nil (paren))
|
||||
'(transient-mark-mode t))
|
||||
|
||||
|
||||
(tool-bar-mode -1)
|
||||
(setq visible-bell t)
|
||||
(setq-default indent-tabs-mode nil)
|
||||
(setq visible-bell t)
|
||||
(column-number-mode 1)
|
||||
|
||||
;; Coding Style
|
||||
(setq auto-mode-alist (cons '("\\.h$" . c++-mode) auto-mode-alist))
|
||||
(defconst my-cc-style
|
||||
'("cc-mode"
|
||||
(c-offsets-alist . ((innamespace . [0])))))
|
||||
(c-add-style "my-cc-mode" my-cc-style)
|
||||
(add-hook 'c++-mode-hook '(lambda ()
|
||||
(c-set-style "my-cc-mode")
|
||||
(gtags-mode 1)
|
||||
))
|
||||
|
||||
;; C++ 11 new keywords
|
||||
(font-lock-add-keywords 'c++-mode
|
||||
'(("\\<\\(thread_local\\)\\>" . font-lock-warning-face)
|
||||
("\\<\\(constexpr\\)\\>" . font-lock-keyword-face)
|
||||
))
|
||||
@@ -1,35 +0,0 @@
|
||||
Install Packages on Ubuntu 12.04 LTS
|
||||
------------------------------------
|
||||
|
||||
Instructions for installing gperftools on Ubuntu
|
||||
|
||||
sudo add-apt-repository ppa:agent-8131/ppa
|
||||
sudo apt-get update
|
||||
sudo apt-get dist-upgrade
|
||||
sudo apt-get install libgoogle-perftools-dev
|
||||
|
||||
Instructions for installing gcc-4.8 (C++11 compatible) on Ubuntu
|
||||
|
||||
sudo add-apt-repository ppa:ubuntu-toolchain-r/test -y
|
||||
sudo update-alternatives --remove-all gcc
|
||||
sudo update-alternatives --remove-all g++
|
||||
sudo apt-get update
|
||||
sudo apt-get install g++-4.8 -y
|
||||
sudo apt-get upgrade -y && sudo apt-get dist-upgrade -y
|
||||
|
||||
Instructions for installing clang-3.3 (C++11 compatible) on Ubuntu
|
||||
|
||||
sudo add-apt-repository ppa:h-rayflood/llvm
|
||||
sudo apt-get update
|
||||
sudo apt-get dist-upgrade
|
||||
sudo apt-get install clang-3.3 clang-3.3-doc
|
||||
|
||||
Note that you [still need][clang_cxx_status] to have g++-4.8's C++
|
||||
runtime library to support some C++11 features that we are using.
|
||||
|
||||
You can specify the C++ compiler to use by using ``-DCMAKE_CXX_COMPILER``
|
||||
option. For example
|
||||
|
||||
cmake -DCMAKE_BUILD_TYPE=DEBUG -DCMAKE_CXX_COMPILER=clang++-3.3 ../../src
|
||||
|
||||
[clang_cxx_status]: http://clang.llvm.org/cxx_status.html
|
||||
@@ -1,22 +1,10 @@
|
||||
Installing Lean on Ubuntu 16.04
|
||||
---------------------------------------------
|
||||
-------------------------------
|
||||
|
||||
### Basic packages
|
||||
|
||||
sudo apt-get install git libgmp-dev cmake
|
||||
|
||||
### Optional packages
|
||||
### Optional Packages: ninja
|
||||
|
||||
sudo apt-get install gitg valgrind doxygen kcachegrind
|
||||
|
||||
### Clone Lean repository
|
||||
|
||||
git clone https://github.com/leanprover/lean.git
|
||||
|
||||
### Build Lean
|
||||
|
||||
cd lean
|
||||
mkdir -p build/release
|
||||
cd build/release
|
||||
cmake ../../src
|
||||
make
|
||||
sudo apt-get install ninja
|
||||
|
||||
Reference in New Issue
Block a user