From 626ba7247b3916473d5865451454e14bfefe337f Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Sat, 14 Sep 2013 21:18:05 -0700 Subject: [PATCH] Update docs, use 4-space indentation for code fragments --- doc/design.md | 56 ++++++++--------- doc/make/ccache.md | 10 ++-- doc/make/osx-10.8.md | 8 +-- doc/make/ubuntu-12.04-detailed.md | 99 +++++++++++++++---------------- 4 files changed, 86 insertions(+), 87 deletions(-) diff --git a/doc/design.md b/doc/design.md index a6407f7a8..f349d7a42 100644 --- a/doc/design.md +++ b/doc/design.md @@ -11,28 +11,28 @@ Building objects such as definitions and theorems without any form of automation 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 := _ + 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 + 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 := _ + 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 + 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`. @@ -46,15 +46,15 @@ When we provide an object with holes to the elaborator, one of the following out 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 := _ + 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 + 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). @@ -63,18 +63,18 @@ Users may react by filling some of the holes themselves, or realizing that it is 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) + (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 := _ + 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 index c7b401202..27b812219 100644 --- a/doc/make/ccache.md +++ b/doc/make/ccache.md @@ -7,20 +7,20 @@ if we are constantly switching between different branches. On Ubuntu, we can install ccache by executing - sudo apt-get install ccache + 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++ "$@" + #!/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 + 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 + cmake -D CMAKE_BUILD_TYPE=Debug -D CMAKE_CXX_COMPILER=~/bin/ccache-g++ -G Ninja ../../src diff --git a/doc/make/osx-10.8.md b/doc/make/osx-10.8.md index 4b5dbcf0f..86bc3e93e 100644 --- a/doc/make/osx-10.8.md +++ b/doc/make/osx-10.8.md @@ -6,13 +6,13 @@ We assume that you are using [homebrew][homebrew], "The missing package manager Instructions for installing gperftools on OS X 10.8 - $ brew install gperftools + brew install gperftools Instructions for installing gcc-4.8 (C++11 compatible) on OS X 10.8 - $ brew tap homebrew/versions - $ brew install gcc48 + 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 + 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 index f71631aac..24fe4ca73 100644 --- a/doc/make/ubuntu-12.04-detailed.md +++ b/doc/make/ubuntu-12.04-detailed.md @@ -3,76 +3,75 @@ 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 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 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++ + 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 + 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 + cd ~ + mkdir projects + cd projects ### Clone your fork - git clone https://github.com/[your-user-name]/lean.git + 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 + 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)) + (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) + (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) - )) + ;; 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) + ))