Revert "Merge (#1099)"

This reverts commit 56a6f46.

.github/PULL_REQUEST_TEMPLATE.md

@@ -2,7 +2,7 @@ TO CONTRIBUTORS:
 
 Make sure you have:
 
-  * [ ] reviewed and applied the coding style: [coding](https://github.com/leanprover/mathlib/blob/master/docs/contribute/style.md), [naming](https://github.com/leanprover/mathlib/blob/master/docs/contribute/naming.md)
+  * [ ] reviewed and applied the coding style: [coding](https://github.com/leanprover/mathlib/blob/master/docs/style.md), [naming](https://github.com/leanprover/mathlib/blob/master/docs/naming.md)
   * [ ] for tactics:
      * [ ] added or adapted documentation in [tactics.md](https://github.com/leanprover/mathlib/blob/master/docs/tactics.md)
      * [ ] write an example of use of the new feature in [tactics.lean](https://github.com/leanprover/mathlib/blob/master/tests/tactics.lean)
@@ -11,4 +11,4 @@ Make sure you have:
 
 If this PR is related to a discussion on Zulip, please include a link in the discussion.
 
-For reviewers: [code review check list](https://github.com/leanprover/mathlib/blob/master/docs/contribute/code-review.md)
+For reviewers: [code review check list](https://github.com/leanprover/mathlib/blob/master/docs/code-review.md)

.gitignore

@@ -1,5 +1,3 @@
 *.olean
 /_target
 /leanpkg.path
-_cache
-__pycache__

.travis.yml

@@ -1,96 +1,62 @@
 language: c
 sudo: false
+go:
+- 1.11.x
 os:
     - linux
+addons:
+    packages:
+        - python3.4
 branches:
-  only:
-    - master
-  # except:
-  #   - /^lean-.*$/
-env:
-  global:
-  - secure: "HxnRtl6pMc+nbszQgDgvMuroMG5AuviULPb0MxPfEIZqYSwKALgc0ILXc89kJyf9rFfpsUdKGmtrGOytzXIp8Yuxvp+fnk/rtuuRyMLeWA0sJ75/Jn+l0BKVid6LNwl7bA4aMOSkjL85kaxU2e5HtlROUkiAgmdAcV10BoK7Vh7yC/S4Zl3kzyCQd8AGSxk0AbeQrb9vK7T1+gWVkEjUFtUsFJ3q5SGrO/j3825qLoRnYj/bKUgtYExQNKjTnTYMbeok+mKJEO1VbLeTk1ri8bLyO2x25lhGImaJSgdPOzuH905ALrf+EHkKm/FYvy5w+zERiuidwwFK5OqVOVWsD5W0G5rYKmDKpzSd39FNnrvb2Tzl2kCin70j6SDOXyZ+4k/iGJpBnOtx3+Ez4gsBDWLIba1c5EXvzhvPoycddgSLBY2LNz4EJI+YqbBTBxG7dVr4NmKKjPowFerVMLM10SgkH9ZZjbAVMxejUJTzp/4gxTanlWm/xds5uC0E0mraLY1H1yzGtwij/lVJN8RGbuhvW9jluLYQzfN7Hb/MReBXTKwdVo5SnsZzv9GEM56IsQXgIhzRoHAuDHd8rS1rfXGaOVfsbYK7pBjtx9j+Pq3BNSPlIL5u4j2JXH6QVJSNaK1npCq81S21dIBfYTP49ft28bhgVE0czkD7kl3fCCk="
+  except:
+    - /^lean-.*$/
 
 cache:
   directories:
     - $TRAVIS_BUILD_DIR/test/
     - $TRAVIS_BUILD_DIR/src/
     - $HOME/.elan
 
+before_install:
+  - python3.4 -m venv .venv --without-pip
+  - curl -s https://bootstrap.pypa.io/get-pip.py -o get-pip.py
+  - .venv/bin/python get-pip.py
+
 install:
+  - .venv/bin/python -m pip install toml
+  - export LEAN_VERSION=`.venv/bin/python scripts/lean_version.py`
   - |
     if [ ! -d "$HOME/.elan/toolchains/" ]; then
       curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
     fi
   - source ~/.elan/env
   - mkdir $HOME/scripts || echo ""
   - export PATH="$HOME/scripts:$PATH"
-  - export OLEAN_RS=https://github.com/cipher1024/olean-rs/releases
-  - export latest=$(curl -sSf "$OLEAN_RS/latest" | cut -d'"' -f2 | awk -F/ '{print $NF}')
-  - curl -sSfL "$OLEAN_RS/download/$latest/olean-rs-linux" -o "$HOME/scripts/olean-rs"
-  - chmod +x $HOME/scripts/olean-rs
   - cp travis_long.sh $HOME/scripts/travis_long
   - chmod +x $HOME/scripts/travis_long
   - (git status | grep  -e "Changes not staged for commit:"); RESULT=$?
   - if [ $RESULT -eq 0 ]; then git checkout -f HEAD ; fi
   - git clean -d -f -q
   - ./purge_olean.sh
   - rm mathlib.txt || true
-  - export LEAN_VERSION=lean-`lean --run scripts/lean_version.lean`
 
 jobs:
   include:
     - stage: Pre-build-1
-      if: type != cron
-      env: TASK="check Lean proofs"
-      script:
-        - travis_long "timeout 2400 leanpkg test" | python scripts/detect_errors.py
-
-    - stage: Pre-build-1
-      env: TASK="check Lean proofs" LEAN="nightly"
-      if: type = cron
-      script:
-        - elan toolchain install leanprover-community/lean:nightly
-        - elan override set leanprover-community/lean:nightly
-        - find . -name *.olean -delete
-        - travis_long "timeout 2400 leanpkg test" | python scripts/detect_errors.py
-
-    - stage: Pre-build-2
-      if: type != cron
-      env: TASK="check Lean proofs"
       script:
-        - travis_long "timeout 2400 leanpkg test" | python scripts/detect_errors.py
+        - travis_long "timeout 2400 leanpkg test" || true
 
     - stage: Pre-build-2
-      env: TASK="check Lean proofs" LEAN="nightly"
-      if: type = cron
       script:
-        - elan toolchain install leanprover-community/lean:nightly
-        - elan override set leanprover-community/lean:nightly
-        - travis_long "timeout 2400 leanpkg test" | python scripts/detect_errors.py
+        - travis_long "timeout 2400 leanpkg test" || true
 
     - stage: Test
-      env: TASK="check Lean proofs"
-      if: type != cron
       script:
-        - travis_long "leanpkg test"
+        - leanpkg test
         - lean --recursive --export=mathlib.txt src/
-        - travis_long "leanchecker mathlib.txt"
+        - leanchecker mathlib.txt
         - sh scripts/deploy_nightly.sh
 
-    - stage: Test
-      env: TASK="check Lean proofs" LEAN="nightly"
-      if: type = cron
-      script:
-        - elan toolchain install leanprover-community/lean:nightly
-        - elan override set leanprover-community/lean:nightly
-        - travis_long "leanpkg test"
-        - lean --recursive --export=mathlib.txt src/
-        - travis_long "leanchecker mathlib.txt"
-
-  # allow_failures:
-  #   - env: TASK="check Lean proofs" LEAN="nightly"
-
 notifications:
   webhooks:
     - https://leanprover.zulipchat.com/api/v1/external/travis?stream=travis&topic=build-status&api_key=SwF1QzwUWol76dCxsYgwHbI6giN3cxGn

README.md

@@ -1,54 +1,68 @@
-# Lean mathlib
+# mathlib
 
 [![Build Status](https://travis-ci.org/leanprover-community/mathlib.svg?branch=master)](https://travis-ci.org/leanprover-community/mathlib)
-[![Mergify Status][mergify-status]][mergify]
-[![Build status](https://ci.appveyor.com/api/projects/status/y0dfsknx5h4iq7pj/branch/master?svg=true)](https://ci.appveyor.com/project/cipher1024/mathlib/branch/master)
 
-[mergify]: https://mergify.io
-[mergify-status]: https://gh.mergify.io/badges/leanprover-community/mathlib.png?style=cut
+## Lean standard library
 
-Mathlib is a user maintained library for the [Lean theorem prover](https://leanprover.github.io). 
-It contains both programming infrastructure and mathematics, as well as tactics that use the former and allow to develop the later.
-
-## Installation
-
-You can find detailed instructions to install Lean, mathlib, and supporting tools:
-* On [Debian-derived Linux](docs/install/debian.md) (Debian, Ubuntu, LMDE...)
-* On [other Linux](docs/install/linux.md) distributions
-* On [MacOS](docs/install/macos.md)
-* On [Windows](docs/install/windows.md)
-
-## Documentation
-
-Besides the installation guides above and [Lean's general
-documentation](https://leanprover.github.io/documentation/), the documentation
-of mathlib consists of:
+Besides [Lean's general documentation](https://leanprover.github.io/documentation/), the documentation of mathlib consists of:
 
+- A [guide](docs/elan.md) on installing Lean and mathlib with elan.
 - A description of [currently covered theories](docs/theories.md),
   as well as an [overview](docs/mathlib-overview.md) for mathematicians.
-- A couple of [tutorials](docs/tutorial/)
-- Some [extra Lean documentation](docs/extras.md) not specific to mathlib
 - A description of [tactics](docs/tactics.md) introduced in mathlib,
   and available [hole commands](docs/holes.md).
-- Documentation for people who would like to [contribute to mathlib](docs/contribute/index.md)
+- An explanation of [naming conventions](docs/naming.md) that is useful
+  to find or contribute definitions and lemmas.
+- A [style guide](docs/style.md) for contributors
+- An outline of [how to contribute](docs/howto-contribute.md) to mathlib.
+- A tentative list of [work in progress](docs/wip.md) to make sure
+  efforts are not duplicated without collaboration.
+
+This repository also contains [extra Lean documentation](docs/extras.md)
+not specific to mathlib.
+
+## Obtaining binaries
+
+### Install the `update-mathlib` script
+
+*Linux/OS X/Cygwin/MSYS2/git bash*: run the following command in a terminal:
+
+``` shell
+curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/remote-install-update-mathlib.sh -sSf | sh
+```
+
+*Any platform*: in the release section of this page, download
+`mathlib-scripts-###-###-###.tar.gz`, expand it and run `setup-update-mathlib.sh`.
+
+### Fetch mathlib binaries
+
+In a terminal, in the directory of a project depending on mathlib, run
+the following:
+
+``` shell
+update-mathlib
+```
+
+The existing `_target/deps/mathlib` will be rewritten with a compiled
+version of mathlib.
+
+### Automatic update of the binaries
+
+The following command, run on each project, sets up an automatic
+update of the mathlib binaries after every `git checkout`.
 
-Much of the discussion surrounding mathlib occurs in a 
-[Zulip chat room](https://leanprover.zulipchat.com/). Since this
-chatroom is only visible to registered users, we provide an 
-[openly accessible archive](https://leanprover-community.github.io/archive/) 
-of the public discussions. This is useful for quick reference; for a
-better browsing interface, and to participate in the discussions, we strongly
-suggest joining the chat. Questions from users at all levels of expertise are
-welcomed.
+``` shell
+echo \#! /bin/sh > .git/hooks/post-checkout
+echo update-mathlib >> .git/hooks/post-checkout
+chmod +x .git/hooks/post-checkout
+```
 
-## Maintainers:
+## Maintainers (topics):
 
 * Jeremy Avigad (@avigad): analysis
 * Reid Barton (@rwbarton): category theory, topology
 * Mario Carneiro (@digama0): all (lead maintainer)
-* Johan Commelin (@jcommelin): algebra
-* Sébastien Gouëzel (@sgouezel): topology, calculus
 * Simon Hudon (@cipher1024): all
-* Chris Hughes (@ChrisHughes24): group theory, ring theory, field theory
+* Chris Hughes (@ChrisHughes24): group_theory, ring_theory, field_theory
 * Robert Y. Lewis (@robertylewis): all
-* Patrick Massot (@patrickmassot): documentation, topology
+* Patrick Massot (@patrickmassot): documentation