michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Create doc directory for documentation. Move wiki pages to doc. Reorganize README.md

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-13 10:01:40 -07:00
parent e4ab64299c
commit b92a3e482d
13 changed files with 381 additions and 157 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

184
README.md
View file

@ -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`

7
doc/authors.md Normal file
View file

@ -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)

80
doc/design.md Normal file
View file

@ -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.

26
doc/make/ccache.md Normal file
View file

@ -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

17
doc/make/cmake_make.md Normal file
View file

@ -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/

25
doc/make/cmake_ninja.md Normal file
View file

@ -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/

29
doc/make/coverage.md Normal file
View file

@ -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

4
doc/make/cygwin.md Normal file
View file

@ -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.

15
doc/make/fedora-19.md Normal file
View file

@ -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

18
doc/make/osx-10.8.md Normal file
View file

@ -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

78
doc/make/ubuntu-12.04-detailed.md Normal file
View file

@ -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)
))

35
doc/make/ubuntu-12.04.md Normal file
View file

@ -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

20
doc/todo.md Normal file
View file

@ -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.