|
Warning: this is an htmlized version!
The original is across this link, and the conversion rules are here. |
####### # # E-scripts on the Lean theorem prover / proof assistant. # # Note 1: use the eev command (defined in eev.el) and the # ee alias (in my .zshrc) to execute parts of this file. # Executing this file as a whole makes no sense. # An introduction to eev can be found here: # # (find-eev-quick-intro) # http://angg.twu.net/eev-intros/find-eev-quick-intro.html # # Note 2: be VERY careful and make sure you understand what # you're doing. # # Note 3: If you use a shell other than zsh things like |& # and the for loops may not work. # # Note 4: I always run as root. # # Note 5: some parts are too old and don't work anymore. Some # never worked. # # Note 6: the definitions for the find-xxxfile commands are on my # .emacs. # # Note 7: if you see a strange command check my .zshrc -- it may # be defined there as a function or an alias. # # Note 8: the sections without dates are always older than the # sections with dates. # # This file is at <http://angg.twu.net/e/lean.e> # or at <http://angg.twu.net/e/lean.e.html>. # See also <http://angg.twu.net/emacs.html>, # <http://angg.twu.net/.emacs[.html]>, # <http://angg.twu.net/.zshrc[.html]>, # <http://angg.twu.net/escripts.html>, # and <http://angg.twu.net/>. # ####### https://leanprover.github.io/ https://leanprover.github.io/tutorial/ https://leanprover.github.io/download/debian78.html * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # Dependencies sudo apt-get install libstdc++-4.8-dev libgmp-dev libmpfr-dev liblua5.2-dev ninja-build sudo dpkg -i /tmp/lean*.deb # (find-status "lean") # (find-vldifile "lean.list") # (find-udfile "lean/") # (find-sitelispfile "lean/") # (find-sitelispfile "lean/lean-mode.el") # (find-sitelispfile "lean/lean-mode.el" ";; Automatically use lean-mode for") # (find-sitelispfile "lean/load-lean.el") # (find-fline "/usr/lib/lean/") # (find-fline "/usr/lib/lean/hott/") # (find-fline "/usr/lib/lean/hott/book.md") # (find-fline "/usr/lib/lean/library/") # (find-fline "/usr/lib/lean/library/logic/logic.md") https://leanprover.github.io/documentation/ http://leanprover.github.io/presentations/20150123_lean-mode/lean-mode.pdf https://leanprover.github.io/tutorial/tutorial.pdf https://leanprover.github.io/tutorial/quickref.pdf https://github.com/leanprover/lean https://github.com/leanprover/lean/blob/master/doc/lean/tutorial.org https://github.com/leanprover/lean/blob/master/src/emacs/README.md # Local Variables: # coding: raw-text-unix # ee-delimiter-hash: "\n#*\n" # ee-delimiter-percent: "\n%*\n" # ee-anchor-format: "«%s»" # End: