diff --git a/README.md b/README.md index 0e9f7ba65..d4deeb201 100644 --- a/README.md +++ b/README.md @@ -11,170 +11,40 @@ Windows, x86_64-w64-mingw32-g++-4.8.1 [build]: http://build.leanprover.net +About +----- + +- [Design](doc/design.md) +- [To Do list](doc/todo.md) +- [Authors](doc/authors.md) + Requirements -============ +------------ - C++11 compatible compiler -- GMP (GNU multiprecision library) - http://gmplib.org/ -- MPFR (GNU MPFR Library) - http://www.mpfr.org/ -- (optional) gperftools - https://code.google.com/p/gperftools/ -- cmake - http://www.cmake.org +- [CMake](http://www.cmake.org) +- [GMP (GNU multiprecision library)](http://gmplib.org/) +- [MPFR (GNU MPFR Library)](http://www.mpfr.org/) +- (optional) [gperftools](https://code.google.com/p/gperftools/) -Install Packages on Ubuntu 12.04 LTS ------------------------------------- +Installing required packages at +-------------------------------- -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 - -Install Packages on Fedora 19 ------------------------------ - -Instructions for installing git, cmake, mpfr, gmp, gperftools on Fedora - - sudo yum install -y git cmake mpfr-devel 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 - -Install Packages on OS X 10.8 ------------------------------ -We assume that you are using [homebrew][homebrew], "The missing package manager for OS X". - -[homebrew]: http://brew.sh - -Instructions for installing gperftools on OS X 10.8 - - $ brew install gperftools - -Instructions for installing gcc-4.8 (C++11 compatible) on OS X 10.8 - - $ brew tap homebrew/versions - $ brew install gcc48 - -Instructions for installing clang-3.3 (C++11 compatible) on OS X 10.8 - - $ brew install llvm --with-clang --with-asan - -Install Packages on Cygwin --------------------------- -Just run cygwin setup.exe (http://cygwin.com/install.html) and make sure that you have installed g++ 4.8.1 (or greater), cmake, gmp and libmpfr. -We have tested Lean using Cygwin for 64-bit versions of Windows. +- [Ubuntu 12.04](doc/make/ubuntu-12.04.md) +- [Ubuntu 12.04 (detailed)](doc/make/ubuntu-12.04-detailed.md) +- [Fedora 19](doc/make/fedora-19.md) +- [OS X 10.8](doc/make/osx-10.8.md) +- [Cygwin](doc/make/cygwin.md) Build Instructions -================== +------------------ -Using [CMake][cmake] + Make ---------------------- -Instructions for DEBUG build +- [CMake + Make](doc/make/cmake_make.md) +- [CMake + Ninja](doc/make/cmake_ninja.md) +- [Faster builds with ccache](doc/make/ccache.md) - mkdir -p build/debug - cd build/debug - cmake -DCMAKE_BUILD_TYPE=DEBUG ../../src - make +Miscellaneous +------------- -Instructions for RELEASE build - - mkdir -p build/release - cd build/release - cmake -DCMAKE_BUILD_TYPE=RELEASE ../../src - make - -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/ - -Instructions for Testing and Measuring Code Coverage -==================================================== - -To measure [code coverage][cover], compile TESTCOV build using g++: - - mkdir -p build/testcov - cd build/testcov - cmake -DCMAKE_BUILD_TYPE=TESTCOV -DCMAKE_CXX_COMPILER=g++-4.8 -G Ninja ../../src - ninja - -and run test cases: - - ctest - -and collect coverage data using [lcov][lcov] and [gcov][gcov]: - - lcov -c -b ../../src -d . -o cov.info --no-external --gcov-tool gcov-4.8 - -and generate HTML output: - - genhtml cov.info --output-directory lcov - -Note: make sure that the version of ``gcov`` matches with the one of -``g++``. Also try to use the latest ``lcov`` if you have a problem -with the existing one. - -[gcov]: http://gcc.gnu.org/onlinedocs/gcc/Gcov.html -[lcov]: http://ltp.sourceforge.net/coverage/lcov.php -[cover]: https://dl.dropboxusercontent.com/u/203889738/lcov/index.html - -Instructions for Building Doxygen Documentation -=============================================== - - doxygen src/Doxyfile +- [Testing and Code Coverage](doc/make/coverage.md) +- Building Doxygen Documentation: `doxygen src/Doxyfile` diff --git a/doc/authors.md b/doc/authors.md new file mode 100644 index 000000000..dd7a8de3c --- /dev/null +++ b/doc/authors.md @@ -0,0 +1,7 @@ +Authors +------- + +The Lean theorem prover is being developed by + +- [Leonardo de Moura](http://research.microsoft.com/en-us/um/people/leonardo) (Microsoft Research) +- [Soonho Kong](http://www.cs.cmu.edu/~soonhok) (CMU) diff --git a/doc/design.md b/doc/design.md new file mode 100644 index 000000000..a6407f7a8 --- /dev/null +++ b/doc/design.md @@ -0,0 +1,80 @@ +Design +------ + +In Lean, the main activity consists in building Environments containing: definitions, theorems, axioms and variable definitions. We *cannot* make a consistent environment *Env* inconsistent by adding definitions and/or theorems. This is guaranteed by the Lean Kernel. + +On the other hand, a user can make the environment inconsistent by adding axioms and variable definitions. +Regarding variable definitions, the inconsistency can be introduced when a user declares that an empty type is inhabited. Actually, variable definitions and axioms have the same status from the Lean Kernel point of view. There is no real difference. An command `Axiom H : a > 0` is conceptually identical to `Variable H : a > 0`. Similarly, a Theorem is just a definition. +The Kernel does not provide any form of automation. It is just doing "bookkeeping" and type checking. In Lean, _proof checking is type checking_. + +Building objects such as definitions and theorems without any form of automation is quite laborious. So, one of the main goals of the Lean project is to provide a lot of building blocks to automate the process of creating new definitions and theorems. + +In Lean, we allow users to provide partially specified objects such as definitions and theorems. A partially specified object is an object with **holes**. Holes mark the parts that must be automatically constructed by Lean. In a nutshell, Lean can be viewed as a system for synthesizing proofs, terms, types, etc. Here is a simple example: + + Variable a : Nat + Axiom a > 0 + Theorem T : a >= 1 := _ + +We use `_` to denote holes. In the simple example above, the "whole proof" must be automatically computed by Lean. Here is another simple example: + + Variable f : Pi (A : Type), A -> A -> A + Definition f00 : Nat := f _ 0 0 + +In this example, Lean will automatically fill the hole with `Nat` (the type of the natural numbers). +Here is another example with multiple holes. + + Variable g : Pi (A : Type), A -> A + Variable a : Nat + Variable b : Nat + Axiom H1 : a = b + Axiom H2 : (g _ a) > 0 + Theorem T1 : (g _ b) > 0 := _ + +Lean supports multiple frontends. The default frontend provides several features that automatically create holes for users. For example, we can write: + + Variable g {A : Type} (a : A) : A + +`g` is a function with two arguments. The curly braces are used to mark _implicit arguments_. +Then, whenever we write `g a`, the system automatically creates `g _ a`. + +The _Lean elaborator_ is the module responsible for filling the holes. Actually, it only manages the collection of tools and components that do all the hard work. +When we provide an object with holes to the elaborator, one of the following outputs is possible + +1) The elaborator succeeds and fill all the holes, and the Lean Kernel accepts the elaborated object without holes. + +2) The elaborator succeeds and fill all the holes, but the Lean Kernel rejects the elaborated object. The elaborator uses many different components. Some of these components may have bugs. The Lean Kernel is the last firewall that will prevent an ill-formed object from being included in the environment. + +3) The elaborator fails to fill the holes, and produces a new environment that demonstrates that it is impossible to fill the holes. We can view the new environment as a counter-example. Moreover, the new environment provides definitions and theorems for all user defined variables and axioms. Here is an example: + + Variable a : Nat + Axiom H : a > 0 + Theorem T : a >= 2 := _ + +In this example, the Lean elaborator will provide a new environment containing + + Definition a : Nat := 1 + Theorem H : a > 0 := Trivial + Theorem T : not a >= 2 := Trivial + +The `Trivial` denotes a proof by evaluation. That is, if we replace `a` with `1` in `a > 0` and evaluate we prove the theorem `a > 0`. The new environment does not contain any variables or axioms. Thus, it is trivially consistent. It also contains a proof for the negation of `a >= 2` (the theorem we were trying to prove). + +4) Finally, the elaborator may fail because of its own limitations. In this case, it produces a trace explaining why a particular hole could not be filled. It might still be possible to fill the whole, but the elaborator does not know how to do it. Note that, the trace may contain an environment that provides definitions for some of the variables and axioms in the user environment. This partial environment may help the user to understand why a particular hole could not be filled. +Users may react by filling some of the holes themselves, or realizing that it is indeed impossible to fill the holes. + +In Lean, we provide a frontend for the SMT 2.0 standard. It is very straightforward to map the SMT constructs into the framework above. For example, the SMT commands + + (declare-fun a () Int) + (declare-fun b () Int) + (assert (> a 0)) + (assert (< b a)) + (check-sat) + +are mapped to + + Variable a : Int + Variable b : Int + Axiom H1 : a > 0 + Axiom H2 : b < a + Theorem U : false := _ + +If Lean can prove `false`, then it produces a proof that demonstrates that the set of SMT assertions is unsatisfiable. If the set of assertions is satisfiable, then it produces a new environment that provides definitions for `a` and `b` and theorems for each assertion. Of course, as we discussed above, Lean may also fail and return a trace describing why it failed. diff --git a/doc/make/ccache.md b/doc/make/ccache.md new file mode 100644 index 000000000..c7b401202 --- /dev/null +++ b/doc/make/ccache.md @@ -0,0 +1,26 @@ +Using ccache +------------ + +[ccache](http://ccache.samba.org/manual.html) is available in many +systems, and can dramatically improve compilation times. In particular +if we are constantly switching between different branches. + +On Ubuntu, we can install ccache by executing + + sudo apt-get install ccache + +Then, we can create a simple script that invokes ccache with our +favorite C++ 11 compiler. For example, we can create the script +`~/bin/ccache-g++` with the following content: + + #!/bin/sh + ccache g++ "$@" + +Then, we instruct cmake to use `ccache-g++` as our C++ compiler + + cmake -D CMAKE_BUILD_TYPE=Debug -D CMAKE_CXX_COMPILER=~/bin/ccache-g++ ../../src + +We usually use Ninja instead of make. Thus, our cmake command +line is: + + cmake -D CMAKE_BUILD_TYPE=Debug -D CMAKE_CXX_COMPILER=~/bin/ccache-g++ -G Ninja ../../src diff --git a/doc/make/cmake_make.md b/doc/make/cmake_make.md new file mode 100644 index 000000000..f50630e57 --- /dev/null +++ b/doc/make/cmake_make.md @@ -0,0 +1,17 @@ +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 new file mode 100644 index 000000000..b28d31826 --- /dev/null +++ b/doc/make/cmake_ninja.md @@ -0,0 +1,25 @@ +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/coverage.md b/doc/make/coverage.md new file mode 100644 index 000000000..969a9756b --- /dev/null +++ b/doc/make/coverage.md @@ -0,0 +1,29 @@ +Instructions for Testing and Measuring Code Coverage +==================================================== + +To measure [code coverage][cover], compile TESTCOV build using g++: + + mkdir -p build/testcov + cd build/testcov + cmake -DCMAKE_BUILD_TYPE=TESTCOV -DCMAKE_CXX_COMPILER=g++-4.8 -G Ninja ../../src + ninja + +and run test cases: + + ctest + +and collect coverage data using [lcov][lcov] and [gcov][gcov]: + + lcov -c -b ../../src -d . -o cov.info --no-external --gcov-tool gcov-4.8 + +and generate HTML output: + + genhtml cov.info --output-directory lcov + +Note: make sure that the version of ``gcov`` matches with the one of +``g++``. Also try to use the latest ``lcov`` if you have a problem +with the existing one. + +[gcov]: http://gcc.gnu.org/onlinedocs/gcc/Gcov.html +[lcov]: http://ltp.sourceforge.net/coverage/lcov.php +[cover]: https://dl.dropboxusercontent.com/u/203889738/lcov/index.html diff --git a/doc/make/cygwin.md b/doc/make/cygwin.md new file mode 100644 index 000000000..008ae47c9 --- /dev/null +++ b/doc/make/cygwin.md @@ -0,0 +1,4 @@ +Install Packages on Cygwin +-------------------------- +Just run cygwin setup.exe (http://cygwin.com/install.html) and make sure that you have installed g++ 4.8.1 (or greater), cmake, gmp and libmpfr. +We have tested Lean using Cygwin for 64-bit versions of Windows. diff --git a/doc/make/fedora-19.md b/doc/make/fedora-19.md new file mode 100644 index 000000000..a91ac7ee4 --- /dev/null +++ b/doc/make/fedora-19.md @@ -0,0 +1,15 @@ +Install Packages on Fedora 19 +----------------------------- + +Instructions for installing git, cmake, mpfr, gmp, gperftools on Fedora + + sudo yum install -y git cmake mpfr-devel 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/osx-10.8.md b/doc/make/osx-10.8.md new file mode 100644 index 000000000..4b5dbcf0f --- /dev/null +++ b/doc/make/osx-10.8.md @@ -0,0 +1,18 @@ +Install Packages on OS X 10.8 +----------------------------- +We assume that you are using [homebrew][homebrew], "The missing package manager for OS X". + +[homebrew]: http://brew.sh + +Instructions for installing gperftools on OS X 10.8 + + $ brew install gperftools + +Instructions for installing gcc-4.8 (C++11 compatible) on OS X 10.8 + + $ brew tap homebrew/versions + $ brew install gcc48 + +Instructions for installing clang-3.3 (C++11 compatible) on OS X 10.8 + + $ brew install llvm --with-clang --with-asan diff --git a/doc/make/ubuntu-12.04-detailed.md b/doc/make/ubuntu-12.04-detailed.md new file mode 100644 index 000000000..f71631aac --- /dev/null +++ b/doc/make/ubuntu-12.04-detailed.md @@ -0,0 +1,78 @@ +Preparing working environment on Ubuntu 12.04 +--------------------------------------------- + +### Install basic packages + + sudo apt-get install git + sudo apt-get install libgmp-dev + sudo apt-get install libmpfr-dev + 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/leodemoura/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 new file mode 100644 index 000000000..9e554588e --- /dev/null +++ b/doc/make/ubuntu-12.04.md @@ -0,0 +1,35 @@ +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/todo.md b/doc/todo.md new file mode 100644 index 000000000..c0b3b3baf --- /dev/null +++ b/doc/todo.md @@ -0,0 +1,20 @@ +To Do List +---------- + +- ~~Add `cast : Pi (A B : Type) (H : A = B) (a : A) : B`, and implement "casting propagation" in the type checker.~~ +- ~~Modify the `let` construct to store the type of the value. The idea is to allow `let name : type := value in expr`. The type does not need to be provided by the user. However, the user may want to provide it as a hint for the Lean elaborator.~~ +- Refactor the elaborator code. The elaborator will be one of the main data-structures in Lean. The elaborator manager should be shared between different frontends. +- Reconsider whether meta-variables should be in `expr` or not. Metavariables (aka holes) are fundamental in our [design](design.md). +- ~~Improve Lean pretty printer for Pi's. For example, it produces `Var a : Pi (A : Type) (_ : A), A` instead of `Var a : Pi (A : Type), A -> A`.~~ +- Decide what will be the main technique for customizing Lean's behavior. The elaborator manager will have many building blocks that can be put together in many different ways. Possible solutions: + - We design our own configuration language. + - We use an off-the-shelf embedded language such as [Lua](http://www.lua.org). + - We use Lean itself. +- Module for reading OpenTheory proofs. +- Higher-Order unification and matching. +- Rewriter (and Rewriter Combinators). +- MCSat framework. +- Implement independent type checker using a different programming language (e.g., OCaml). +- Add `match` construct in `expr`. +- Add inductive datatype (families) in the environment. It will be a new kind of object. +- Add recursive function definition objects (low priority). It is another new kind of object.