diff --git a/README.md b/README.md index efdbe523d3..5133aa5a8c 100644 --- a/README.md +++ b/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 ------------- diff --git a/doc/make/cmake_make.md b/doc/make/cmake_make.md deleted file mode 100644 index f50630e572..0000000000 --- a/doc/make/cmake_make.md +++ /dev/null @@ -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/ diff --git a/doc/make/cmake_ninja.md b/doc/make/cmake_ninja.md deleted file mode 100644 index b28d31826f..0000000000 --- a/doc/make/cmake_ninja.md +++ /dev/null @@ -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/ diff --git a/doc/make/fedora-19.md b/doc/make/fedora-19.md deleted file mode 100644 index 6ea028052a..0000000000 --- a/doc/make/fedora-19.md +++ /dev/null @@ -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 diff --git a/doc/make/index.md b/doc/make/index.md new file mode 100644 index 0000000000..f7562723d9 --- /dev/null +++ b/doc/make/index.md @@ -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) diff --git a/doc/make/msys2.md b/doc/make/msys2.md index a15d50fc06..83d3cd374e 100644 --- a/doc/make/msys2.md +++ b/doc/make/msys2.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 diff --git a/doc/make/osx-10.9.md b/doc/make/osx-10.9.md index 3fe6d5109f..41fd7daa34 100644 --- a/doc/make/osx-10.9.md +++ b/doc/make/osx-10.9.md @@ -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 -``` diff --git a/doc/make/ubuntu-12.04-detailed.md b/doc/make/ubuntu-12.04-detailed.md deleted file mode 100644 index f4d1d164d4..0000000000 --- a/doc/make/ubuntu-12.04-detailed.md +++ /dev/null @@ -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) - )) diff --git a/doc/make/ubuntu-12.04.md b/doc/make/ubuntu-12.04.md deleted file mode 100644 index 9e554588e7..0000000000 --- a/doc/make/ubuntu-12.04.md +++ /dev/null @@ -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 diff --git a/doc/make/ubuntu-16.04.md b/doc/make/ubuntu-16.04.md index 8fa21fc983..7c281da26a 100644 --- a/doc/make/ubuntu-16.04.md +++ b/doc/make/ubuntu-16.04.md @@ -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