Skip to content

Commit

Permalink
Update README
Browse files Browse the repository at this point in the history
  • Loading branch information
flypitch committed May 22, 2019
1 parent 26ed5de commit c39b2ac
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions README.org
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,9 @@ The Flypitch project aims to produce a formal proof of the [[https://en.wikipedi
** Documentation
A conventional human-readable account of the proof written in type-theoretic foundations, upon which some parts of the formalization will be based, is [[https://www.github.com/flypitch/flypitch-notes/][located here]].
** Compilation
To compile the Flypitch project, you will need [[https://leanprover.github.io/][Lean 3.4.2]]. The ~leanpkg.toml~ file points to a certain commit of ~mathlib~, which will be cloned into the project directory. After cloning the repository to ~flypitch~, navigate to ~flypitch~ and run
To compile the Flypitch project, you will need [[https://leanprover.github.io/][Lean 3.4.2]]. Installation instructions for Lean can be found [[https://github.com/leanprover-community/mathlib/blob/master/README.md][here]].

The ~leanpkg.toml~ file points to a certain commit of ~mathlib~, which will be cloned into the project directory. After cloning the repository to ~flypitch~, navigate to ~flypitch~ and run
#+BEGIN_SRC
leanpkg configure
leanpkg build
Expand All @@ -19,8 +21,6 @@ update-mathlib
leanpkg build
#+END_SRC

Installation instructions for Lean (using ~elan~) can be found [[https://github.com/leanprover-community/mathlib/blob/master/docs/elan.md][here]].

** Viewing and navigating the project
To view the project, we recommend the use of a Lean-aware editor like [[https://github.com/leanprover/lean-mode][Emacs]] or [[https://github.com/leanprover/vscode-lean][VSCode]]. Among other things, like type information, such editors can display the /proof state/ inside a tactic block, making it easier to understand how theorems are being proved.

Expand Down

0 comments on commit c39b2ac

Please sign in to comment.