From 138fef02fa4fb1add4bbb432bdd91da1b6e5b7fe Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 3 Oct 2018 13:42:09 -0400 Subject: [PATCH] update README/usage --- README.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 6edc9a9..4e7465f 100644 --- a/README.md +++ b/README.md @@ -112,8 +112,9 @@ These projects are done + need to splice together LES's ## Usage and Contributing -- To compile this repository you will need a working version of Lean 2. Installation instructions for Lean 2 can be found [here](https://github.com/leanprover/lean2). -- We will try to make sure that this repository compiles with the newest version of Lean 2. -- Some notes on the Emacs mode can be found [here](https://github.com/leanprover/lean2/blob/master/src/emacs/README.md) (for example if some unicode characters don't show up, or increase the spacing between lines by a lot). +- To compile this repository you can run `linja` (or `path/to/lean2/bin/linja`) in the main directory. + + You will need a working version of Lean 2. Installation instructions for Lean 2 can be found [here](https://github.com/leanprover/lean2). + + We will try to make sure that this repository compiles with the newest version of Lean 2. +- The preferred editor for Lean 2 is Emacs. Notes on the Emacs mode can be found [here](https://github.com/leanprover/lean2/blob/master/src/emacs/README.md) (for example if some unicode characters don't show up, or increase the spacing between lines by a lot). - We try to separate the repository into the folders `algebra`, `homotopy`, `homology`, `cohomology`, `spectrum` and `colimit`. Homotopy theotic properties of types which do not explicitly mention homotopy, homology or cohomology groups (such as `A ∧ B ≃* B ∧ A`) are part of `homotopy`. - If you contribute, please use rebase instead of merge (e.g. `git pull -r`).