Warning: this is an htmlized version!
The original is here, 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/>. # ####### # «.zulip» (to "zulip") # «.regular-install-2021» (to "regular-install-2021") # «.lean-3.4.2» (to "lean-3.4.2") # «.vscode» (to "vscode") # «.elan» (to "elan") # «.lean4» (to "lean4") # «.lake» (to "lake") # «.lake-new-greeting» (to "lake-new-greeting") # «.cache-mathlib» (to "cache-mathlib") # «.axiom» (to "axiom") # «.constant» (to "constant") # «.lean4-mode» (to "lean4-mode") # «.lean-mode» (to "lean-mode") # «.topos» (to "topos") # «.diagram-chasing» (to "diagram-chasing") # «.tpinlean» (to "tpinlean") # «.theorem_proving_in_lean» (to "theorem_proving_in_lean") # «.prelude» (to "prelude") # «.rec_on» (to "rec_on") # «.nng4» (to "nng4") # «.natural-number-game» (to "natural-number-game") # «.real-number-game» (to "real-number-game") # «.mathsinlean» (to "mathsinlean") # «.mathzoo» (to "mathzoo") # «.mathlib» (to "mathlib") # «.mathlib4» (to "mathlib4") # «.mathlib4-greeting» (to "mathlib4-greeting") # «.mathlib-calculus» (to "mathlib-calculus") # «.tactics-in-ND» (to "tactics-in-ND") # «.vernacular» (to "vernacular") # «.fplean4» (to "fplean4") # «.structures» (to "structures") # «.check-fun» (to "check-fun") 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 https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/ *** https://xenaproject.wordpress.com/2020/02/09/lean-is-better-for-proper-maths-than-all-the-other-theorem-provers/ https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ https://xenaproject.wordpress.com/2020/04/30/the-invisible-map/ https://xenaproject.wordpress.com/2020/06/27/teaching-dependent-type-theory-to-4-year-olds-via-mathematics/amp/ https://xenaproject.wordpress.com/2021/01/21/formalising-mathematics-an-introduction/ pictures as eefective guides *** https://xenaproject.wordpress.com/2021/04/18/induction-on-equality/ ##### # # zulip # 2023jun24 # ##### # «zulip» (to ".zulip") # https://leanprover.zulipchat.com/ ##### # # regular-install-2021 (deleted!) # 2021jul05 # ##### # «regular-install-2021» (to ".regular-install-2021") # https://leanprover-community.github.io/get_started.html#regular-install # https://leanprover-community.github.io/install/debian.html ##### # # lean-3.4.2 (deleted!) # 2022dec22 # ##### # «lean-3.4.2» (to ".lean-3.4.2") # https://github.com/leanprover/lean/releases/download/v3.4.2/lean-3.4.2-linux.tar.gz ##### # # vscode (deleted!) # 2021jul05 # ##### # «vscode» (to ".vscode") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) aptrm code sudo apt-get autoremove ##### # # elan # 2023jun22 # ##### # «elan» (to ".elan") # https://github.com/leanprover/elan # https://proofassistants.stackexchange.com/questions/2/how-do-i-install-lean-4 # (find-git-links "https://github.com/leanprover/elan" "elan") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # (find-fline "/tmp/elan-install/") rm -Rv /tmp/elan-install/ mkdir /tmp/elan-install/ cd /tmp/elan-install/ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \ | sh -s -- --default-toolchain leanprover/lean4:nightly # (code-c-d "elan4lean" "~/.elan/toolchains/leanprover--lean4---nightly/src/lean/") # (find-elan4leanfile "") # (find-sh "find ~/.elan/ | sort") rm -Rfv ~/.elan/ elan elan show elan default lean4:nightly elan default nightly elan default leanprover/lean4:nightly w lake lake # Welcome to Lean! # # This will download and install Elan, a tool for managing different Lean # versions used in packages you create or download. It will also install a # default version of Lean and its package manager, leanpkg, for editing files not # belonging to any package. # # It will add the leanpkg, lean, and elan commands to Elan's bin directory, # located at: # # /home/edrx/.elan/bin # # This path will then be added to your PATH environment variable by modifying the # profile files located at: # # /home/edrx/.profile # /home/edrx/.zprofile # # You can uninstall at any time with elan self uninstall and these changes will # be reverted. # # Current installation options: # # default toolchain: leanprover/lean4:nightly # modify PATH variable: yes # # 1) Proceed with installation (default) # 2) Customize installation # 3) Cancel installation * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # rm -Rfv ~/usrc/elan/ cd ~/usrc/ git clone https://github.com/leanprover/elan cd ~/usrc/elan/ # (code-c-d "elan" "~/usrc/elan/") # (find-elanfile "") # (find-elanfile "elan-init.sh") # (find-fline "~/.elan/") # (find-fline "~/.profile") # (find-fline "~/.zprofile") ##### # # lean4 # 2023jun22 # ##### # «lean4» (to ".lean4") # https://github.com/leanprover/lean4 # https://www.reddit.com/r/haskell/comments/z55hha/review_of_lean_4/ * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # rm -Rfv ~/bigsrc/lean4/ cd ~/bigsrc/ git clone https://github.com/leanprover/lean4 cd ~/bigsrc/lean4/ * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) cd ~/bigsrc/lean4/ git clean -dfx git reset --hard find * | sort > .files wc .files export PAGER=cat git branch --list -a git for-each-ref git log --oneline --graph --all -20 # (find-fline "~/bigsrc/") # (find-fline "~/bigsrc/lean4/") # (find-gitk "~/bigsrc/lean4/") # (code-c-d "lean4" "~/bigsrc/lean4/") # (find-lean4file "") # (find-lean4file ".files") # (find-lean4file "doc/") # (find-lean4file "doc/quickstart.md") # (find-lean4file "doc/quickstart.md" "lake init foo") # (find-lean4file "doc/sections.md") Quickstart: https://github.com/leanprover/lean4/blob/master/doc/quickstart.md Walkthrough installation video: https://www.youtube.com/watch?v=yZo6k48L0VY Quick tour video: https://youtu.be/zyXtbb_eYbY Homepage: https://leanprover.github.io Theorem Proving Tutorial: https://leanprover.github.io/theorem_proving_in_lean4/ Functional Programming in Lean: https://leanprover.github.io/functional_programming_in_lean/ Manual: https://leanprover.github.io/lean4/doc/ Release notes: RELEASES.md Examples: https://leanprover.github.io/lean4/doc/examples.html FAQ: https://leanprover.github.io/lean4/doc/faq.html Setting Up Lean: https://leanprover.github.io/lean4/doc/setup.html https://github.com/leanprover/lean4/blob/master/doc/setup.md#basic-setup ##### # # lake # 2023jun25 # ##### # «lake» (to ".lake") # (find-angg ".emacs.papers" "fplean4") # https://github.com/leanprover/lake # (find-git-links "https://github.com/leanprover/lake" "lake") # (code-c-d "lake" "~/usrc/lake/") # (find-lakefile "") # (find-lakefile "README.md") ##### # # lake-new-greeting # 2023jun25 # ##### # «lake-new-greeting» (to ".lake-new-greeting") # (to "mathlib4-greeting") # (find-angg ".emacs.papers" "fplean4") # (find-fplean4page 75 "Starting a Project") # (find-fplean4text 75 "Starting a Project") # (find-fplean4page 76 "import «Greeting»") # (find-fplean4text 76 "import «Greeting»") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # (find-fline "/tmp/gr/") rm -Rfv /tmp/greeting/ rm -Rfv /tmp/gr/ mkdir /tmp/gr/ cd /tmp/gr/ lake new greeting cd /tmp/gr/greeting/ # lean --run Main.lean # lean --run Greeting.lean find * | sort | tee of0 lake build find * | sort | tee of1 comm of0 of1 laf find build | sort build/bin/greeting cp -v build/bin/greeting /tmp/greeting cd /tmp/ ./greeting # (find-fline "/tmp/gr/greeting/") # (find-fline "/tmp/gr/greeting/Main.lean") # (find-fline "/tmp/gr/greeting/build/bin/") w lake ##### # # cache-mathlib # 2023jun26 # ##### # «cache-mathlib» (to ".cache-mathlib") # (find-fline "~/.cache/mathlib/") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) du -c ~/.cache/mathlib/ find ~/.cache/mathlib/ laf ~/.cache/mathlib/ ##### # # axiom # 2023jun24 # ##### # «axiom» (to ".axiom") # (find-lean4grep "grep --color=auto -nRH --null -e axiom doc/*") # (find-lean4file "doc/declarations.md" "axiom c : α") # (find-es "agda" "postulates") ##### # # constant # 2023jun24 # ##### # «constant» (to ".constant") # (find-lean4grep "grep --color=auto -nRH --null -e constant doc/*") # (find-lean4file "doc/funabst.md" "constant f : Nat → Nat") # (find-lean4file "doc/simptypes.md" "The ``constant`` command") # (find-lean4file "doc/typeobjs.md" "constant α : Type") # (find-tpinleanpage 11 "constant m : nat") # (find-tpinleantext 11 "constant m : nat") (find-lean4file "doc/SUMMARY.md" "# Language Manual") ##### # # lean4-mode # 2023jun22 # ##### # «lean4-mode» (to ".lean4-mode") # https://github.com/leanprover/lean4-mode # (find-es "emacs" "package-vc-install") # (find-es "emacs" "lsp-mode") # (package-vc-install "https://github.com/leanprover/lean4-mode") # (find-epackage-links 'lean4-mode "lean4mode" t) # (find-epackages 'lean4-mode) # (find-epackage 'lean4-mode) # (code-c-d "lean4mode" "~/.emacs.d/elpa/lean4-mode/") # (find-lean4modefile "") # (find-lean4modefile "README.md" "hovering") # (find-lean4modefile "README.md" "C-c C-i" "toggle info view") # (find-lean4modefile "lean4-input.el" "(defcustom lean4-input-inherit") ##### # # lean-mode # 2021jul05 # ##### # «lean-mode» (to ".lean-mode") # (find-epackages 'lean-mode) # (find-epackage-links 'lean-mode) # (find-epackage 'lean-mode) # (code-c-d "leanmode" "~/.emacs.d/elpa/lean-mode-20210502.2049/") # (find-leanmodefile "") # (find-leanmodegrep "grep --color=auto -nH --null -e rootdir *.el") # (find-efunction 'lean-get-rootdir) 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 ##### # # topos # 2021jul05 # ##### # «topos» (to ".topos") # https://github.com/b-mehta/topos # (find-git-links "https://github.com/b-mehta/topos" "topos") # (code-c-d "topos" "~/usrc/topos/") # (find-toposfile "") # (find-toposfile "README.md") # (find-toposfile "src/") # (find-toposfile "src/applications/") # (find-toposfile "src/category/") ##### # # diagram-chasing # 2021jul05 # ##### # «diagram-chasing» (to ".diagram-chasing") # (find-books "__cats/__cats.el" "himmel") # (find-himmeldiagchpage 19 "3.2. A formal proof of the four lemma") # (find-himmeldiagchtext 19 "3.2. A formal proof of the four lemma") ##### # # Theorem Proving in Lean # 2021oct01 # ##### # «tpinlean» (to ".tpinlean") # «theorem_proving_in_lean» (to ".theorem_proving_in_lean") # (find-angg ".emacs.papers" "tpinlean") # https://github.com/leanprover/theorem_proving_in_lean # https://github.com/leanprover/theorem_proving_in_lean4 # (find-git-links "https://github.com/leanprover/theorem_proving_in_lean" "tpinlean") # (find-git-links "https://github.com/leanprover/theorem_proving_in_lean4" "tpinlean4") # (find-tpinlean4file "SUMMARY.md") # (code-c-d "tpinlean4" "~/usrc/theorem_proving_in_lean4/") # (find-tpinlean4file "") # (find-tpinlean4file "SUMMARY.md") # (find-tpinlean4file "introduction.md") # (find-tpinlean4file "dependent_type_theory.md") # (find-tpinlean4file "propositions_and_proofs.md") # (find-tpinlean4file "quantifiers_and_equality.md") # (find-tpinlean4file "tactics.md") # (find-tpinlean4file "tactics.md" "C-c C-g") # (find-tpinlean4file "interacting_with_lean.md") # (find-tpinlean4file "inductive_types.md") # (find-tpinlean4file "induction_and_recursion.md") # (find-tpinlean4file "structures_and_records.md") # (find-tpinlean4file "type_classes.md") # (find-tpinlean4file "conv.md") # (find-tpinlean4file "axioms_and_computation.md") ##### # # prelude # 2023jun29 # ##### # «prelude» (to ".prelude") # (find-tpinlean4file "inductive_types.md" "prelude") # (find-tpinlean4file "propositions_and_proofs.md" "Prelude.core") # (find-lean4prefile "") # (find-lean4prefile "") # (find-lean4prefile "Init/") # (find-lean4prefile "Init/Prelude.lean") # (find-lean4prefile "Lean/") ##### # # rec_on # 2023jul10 # ##### # «rec_on» (to ".rec_on") # (find-tpinleanpage 89 "nat.rec_on") # (find-tpinleantext 89 "nat.rec_on") # (find-tpinleanpage 102 "weekday.rec_on (also generated automatically)") # (find-tpinleantext 102 "weekday.rec_on (also generated automatically)") # (find-tpinleanpage 103 "renaming option") # (find-tpinleantext 103 "renaming option") https://github.com/leanprover/theorem_proving_in_lean4/blob/master/inductive_types.md inductive weekday : Type | sunday : weekday | monday : weekday | tuesday : weekday | wednesday : weekday | thursday : weekday | friday : weekday | saturday : weekday #check weekday.sunday #check weekday.monday #check weekday.rec #check weekday.casesOn weekday.casesOn.{u} {motive : weekday → Sort u} (t : weekday) (sunday : motive weekday.sunday) (monday : motive weekday.monday) (tuesday : motive weekday.tuesday) (wednesday : motive weekday.wednesday) (thursday : motive weekday.thursday) (friday : motive weekday.friday) (saturday : motive weekday.saturday) : motive t weekday.rec.{u} {motive : weekday → Sort u} (sunday : motive weekday.sunday) (monday : motive weekday.monday) (tuesday : motive weekday.tuesday) (wednesday : motive weekday.wednesday) (thursday : motive weekday.thursday) (friday : motive weekday.friday) (saturday : motive weekday.saturday) (t : weekday) : motive t @[reducible] inductive mynat : Type | zero : mynat | succ : mynat → mynat -- #check zero #check mynat.zero open mynat (renaming rec_on → rec_on) def add (m n : mynat) : mynat := mynat.rec_on n m (λ n add_m_n => succ add_m_n) #check add #check mynat #check mynat.rec #check mynat.rec_on #check succ zero #check add (succ zero) (succ (succ zero)) -- try it out #reduce add (succ zero) (succ (succ zero)) ##### # # nng4 # 2023jun27 # ##### # «nng4» (to ".nng4") # https://adam.math.hhu.de/ # https://github.com/leanprover-community/lean4game # https://github.com/PatrickMassot/NNG4 ##### # # natural-number-game # 2021oct06 # ##### # «natural-number-game» (to ".natural-number-game") # https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ # https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/FAQ.html # https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/FAQ.html#sourcecode # https://github.com/ImperialCollegeLondon/natural_number_game # https://github.com/mpedramfar/Lean-game-maker # (find-git-links "https://github.com/ImperialCollegeLondon/natural_number_game" "nng") # (find-git-links "https://github.com/mpedramfar/Lean-game-maker" "lgm") # (code-c-d "nng" "~/usrc/natural_number_game/") # (code-c-d "lgm" "~/usrc/Lean-game-maker/") # (find-nngfile "") # (find-nngfile "docs/technical.md") # (find-nngfile "docs/technical.md" "tactic monad") # (find-nngfile "src/tactic/") # (find-nngfile "src/tactic/modded.lean") # (find-nngfile "src/game/") # (find-nngfile "src/game/world2/") # (find-nngfile "src/game/world2/level1.lean") # (find-lgmfile "") https://www.ma.imperial.ac.uk/~buzzard/xena/ https://www.youtube.com/watch?v=9V1Xo1n_3Qw LftCM2020: Natural number game - Kevin Buzzard https://xenaproject.wordpress.com/2019/10/24/chalkdust-and-the-natural-number-game/ https://xenaproject.wordpress.com/2019/11/12/the-natural-number-game-an-update/ ##### # # real-number-game # 2021oct17 # ##### # «real-number-game» (to ".real-number-game") # https://github.com/ImperialCollegeLondon/real-number-game # (find-git-links "https://github.com/ImperialCollegeLondon/real-number-game" "rng") # (code-c-d "rng" "~/usrc/real-number-game/") # (find-rngfile "") ##### # # mathsinlean # 2023jun24 # ##### # «mathsinlean» (to ".mathsinlean") # (find-angg ".emacs.papers" "mathsinlean") # https://leanprover-community.github.io/mathematics_in_lean/ # https://github.com/leanprover-community/mathematics_in_lean (new) # https://github.com/leanprover-community/mathematics_in_lean3 (old) # (find-git-links "https://github.com/leanprover-community/mathematics_in_lean" "mathsinlean") # (code-c-d "mathsinlean" "~/bigsrc/mathematics_in_lean/") # (find-mathsinleanfile "") # (find-mathsinleanfile "lake-packages/") # (find-mathsinleanfile "MIL/") # (find-mathsinleanfile "MIL/C01_Introduction/") # (find-mathsinleanfile "MIL/C01_Introduction/S02_Overview.lean") # (find-mathsinleanpage) # (find-mathsinleantext) # (find-mathsinleanpage 5 "lake exe cache get") # (find-mathsinleantext 5 "lake exe cache get") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) rm -Rfv ~/bigsrc/mathematics_in_lean/ cd ~/bigsrc/ git clone https://github.com/leanprover-community/mathematics_in_lean cd ~/bigsrc/mathematics_in_lean/ lake exe cache get |& tee ole # (find-sh "lake help") # (find-sh "lake help exe") # (find-mathsinleanfile "") # (find-mathsinleanfile "ole") Another basic question... now I have a full copy of mathlib4 in ~/bigsrc/mathlib4/, and I tried to run this: rm -Rfv ~/bigsrc/mathematics_in_lean/ cd ~/bigsrc/ git clone https://github.com/leanprover-community/mathematics_in_lean cd ~/bigsrc/mathematics_in_lean/ lake exe cache get Apparently 1) this downloaded another full copy of mathlib4 in ~/bigsrc/mathematics_in_lean/lake-packages/mathlib/, and 2) if I create a project and I put a like like this require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master" in its lakefile.lean it will also download another full copy of mathlib4... is there a way to make these copies be shared? # Error: LSP :: Yasnippet is not installed, but `lsp-enable-snippet' is set to `t'. You must either install yasnippet, or disable snippet support. LSP :: Connected to [lean4-lsp:187121/starting /home/edrx/bigsrc/mathematics_in_lean]. [2 times] LSP :: Unable to autoconfigure company-mode. [2 times] LSP :: lean4-lsp:187121 initialized successfully in folders: (/home/edrx/bigsrc/mathematics_in_lean) LSP :: You can configure this warning with the `lsp-enable-file-watchers' and `lsp-file-watch-threshold' variables LSP :: Unable to autoconfigure company-mode. [2 times] info: [256/540] Building Aesop.Tree.UnsafeQueue info: [315/794] Building Aesop.Search.Queue info: [353/794] Building Mathlib.Data.ListM.Basic info: [538/794] Building Mathlib.Algebra.Order.Group.Defs error: external command `/home/edrx/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/lean` exited with code 139 `/home/edrx/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/lake print-paths Init Mathlib.Data.Nat.Basic Mathlib.Data.Nat.Parity Mathlib.Tactic` failed: stderr: info: [155/374] Building Qq.MetaM info: [218/540] Building Std.Data.String.Lemmas info: [256/540] Building Aesop.Tree.UnsafeQueue info: [315/794] Building Aesop.Search.Queue info: [353/794] Building Mathlib.Data.ListM.Basic info: [538/794] Building Mathlib.Algebra.Order.Group.Defs error: > LEAN_PATH=./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib LD_LIBRARY_PATH=./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib:./lake-packages/mathlib/build/lib /home/edrx/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/lean -DwarningAsError=true -Dpp.unicode.fun=true ./lake-packages/mathlib/././Mathlib/Algebra/Order/Group/Defs.lean -R ./lake-packages/mathlib/./. -o ./lake-packages/mathlib/build/lib/Mathlib/Algebra/Order/Group/Defs.olean -i ./lake-packages/mathlib/build/lib/Mathlib/Algebra/Order/Group/Defs.ilean -c ./lake-packages/mathlib/build/ir/Mathlib/Algebra/Order/Group/Defs.c error: external command `/home/edrx/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/lean` exited with code 139 Mark set ##### # # mathzoo # 2023jun24 # ##### # «mathzoo» (to ".mathzoo") # https://github.com/leanprover-community/mathzoo # (code-c-d "mathzoo" "~/usrc/mathzoo/") # (find-mathzoofile "") # (find-mathzoosh "find * | sort") ##### # # mathlib # 2023jun24 # ##### # «mathlib» (to ".mathlib") # https://github.com/leanprover-community/mathlib # (find-git-links "https://github.com/leanprover-community/mathlib" "mathlib") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) rm -Rfv ~/bigsrc/mathlib/ cd ~/bigsrc/ git clone https://github.com/leanprover-community/mathlib cd ~/bigsrc/mathlib/ # (code-c-d "mathlib" "~/bigsrc/mathlib/") # (find-mathlibfile "") # (find-mathlibfile "README.md") # https://leanprover-community.github.io/install/linux.html ##### # # mathlib4 # 2023jun24 # ##### # «mathlib4» (to ".mathlib4") # https://github.com/leanprover-community/mathlib4 # (find-git-links "https://github.com/leanprover-community/mathlib4" "mathlib4") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) rm -Rfv ~/bigsrc/mathlib4/ cd ~/bigsrc/ git clone https://github.com/leanprover-community/mathlib4 cd ~/bigsrc/mathlib4/ cd ~/bigsrc/mathlib4/ lake exe cache get cd ~/bigsrc/mathlib4/ git clean -dfx git pull elan self update lake build |& tee olb # (code-c-d "mathlib4" "~/bigsrc/mathlib4/") # (find-mathlib4file "") # (find-mathlib4sh "find * | sort") # (find-mathlib4file "README.md") # (find-mathlib4file "README.md" "lean_exe") # (find-mathlib4file "README.md" "elan self update") # (find-mathlib4file "README.md" "lake build") # (find-mathlib4file "" "lake") # (find-mathlib4file "lake-manifest.json") # (find-mathlib4file "lakefile.lean") # (find-mathlib4file "olb") # (find-mathlib4file "lakefile.lean" "package mathlib where") # (find-mathlib4file "Mathlib/Data/Set/") # (find-mathlib4file "Mathlib/Data/Set/Basic.lean") ##### # # mathlib4-greeting # 2023jun26 # ##### # «mathlib4-greeting» (to ".mathlib4-greeting") # (to "lake-new-greeting") # (find-mathlib4file "README.md" "require mathlib from git") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) rm -Rfv /tmp/gr/ mkdir /tmp/gr/ cd /tmp/gr/ lake new greeting cd /tmp/gr/greeting/ lake build lake update lake build # (find-fline "/tmp/gr/greeting/") ##### # # mathlib-calculus # 2022jul03 # ##### # «mathlib-calculus» (to ".mathlib-calculus") # https://github.com/leanprover-community/mathlib # https://leanprover-community.github.io/mathlib_docs/ # https://leanprover-community.github.io/mathlib_docs/analysis/calculus/deriv.html # https://leanprover-community.github.io/get_started.html * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # rm -Rfv ~/usrc/mathlib/ cd ~/usrc/ git clone https://github.com/leanprover-community/mathlib git clone git@github.com:leanprover-community/mathematics_in_lean.git cd ~/usrc/mathlib/ cd ~/usrc/mathlib/ In a terminal, navigate to the folder where you want to put a copy of the repository, and type git clone git@github.com:leanprover-community/mathematics_in_lean.git to fetch it from github. Navigate to mathematics_in_lean, and execute lake exe cache get to fetch a compiled version of the library, mathlib. Type code . to open the folder in VS Code. Alternatively, you can run VS Code and choose Open Folder from the File menu. Be sure to open the folder mathematics_in_lean, not any other folder. ;; <leanmathlib> ;; "The Lean Mathematical Library" ;; https://arxiv.org/abs/1910.09336 ;; https://arxiv.org/pdf/1910.09336.pdf (code-pdf-page "leanmathlib" "$S/https/arxiv.org/pdf/1910.09336.pdf") (code-pdf-text "leanmathlib" "$S/https/arxiv.org/pdf/1910.09336.pdf") ;; (find-leanmathlibpage) ;; (find-leanmathlibtext) # (find-anggsh "find . -mtime 0 | sort") # (find-fline "~/.config/Code/") # (find-fline "~/.local/pipx/logs/") # (find-fline "~/.elan/") # (find-fline "~/.local/pipx/") # (find-fline "~/.mathlib/") # (find-fline "~/.mathlib/url") # (find-fline "~/.vscode/") ##### # # tactics-in-ND # 2021oct14 # ##### # «tactics-in-ND» (to ".tactics-in-ND") # https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Natural.20Deduction/near/257611457 # https://leanprover-community.github.io/mathlib_docs/tactic/explode.html#tactic.explode ##### # # vernacular # 2021dec16 # ##### # «vernacular» (to ".vernacular") # https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista # https://www.youtube.com/watch?v=Dp-mQ3HxgDE#t=1h0m0s ##### # # fplean4 # 2023jun02 # ##### # «fplean4» (to ".fplean4") # (find-angg ".emacs.papers" "fplean4") # https://news.ycombinator.com/item?id=36107796 Functional Programming in Lean – a book on using Lean 4 to write programs (leanprover.github.io) # https://leanprover.github.io/functional_programming_in_lean/ # https://leanprover.github.io/functional_programming_in_lean/print.html # (code-pdf-page "fplean4" "$S/https/leanprover.github.io/Functional Programming in Lean.pdf") # (code-pdf-text "fplean4" "$S/https/leanprover.github.io/Functional Programming in Lean.pdf") # (find-fplean4page) # (find-fplean4text) ##### # # structures # 2023jun24 # ##### # «structures» (to ".structures") -- (find-fplean4page 18 "Structures") -- (find-fplean4text 18 "Structures") -- (find-fplean4page 24 "The function Point.modifyBoth") -- (find-fplean4text 24 "The function Point.modifyBoth") structure Point where x : Float y : Float deriving Repr structure Point3D where x : Float y : Float z : Float deriving Repr def origin3D : Point3D := { x := 0.0, y := 0.0, z := 0.0 } --#check { x := 0.0, y := 0.0 } -- err #check ({ x := 0.0, y := 0.0 } : Point) #check { x := 0.0, y := 0.0 : Point} ##### # # check-fun # 2023jun24 # ##### # «check-fun» (to ".check-fun") -- (find-fplean4page 12 "#eval (1 + 2 : Nat)") -- (find-fplean4text 12 "#eval (1 + 2 : Nat)") -- (find-fplean4page 13 "#check (1 - 2 : Int)") -- (find-fplean4text 13 "#check (1 - 2 : Int)") -- (find-fplean4page 54 "#check fun (x : Int) => x + 1") -- (find-fplean4text 54 "#check fun (x : Int) => x + 1") -- (find-fplean4page 55 "(· + 1)") -- (find-fplean4text 55 "(· + 1)") -- (find-lean4file "doc/functions.md") #check 1 #check 1 : Int -- bad #check (1 : Int) -- good #check Nat #check Nat -> Nat #check ((Nat -> Nat) : Type) #check ( Nat -> Nat : Type) #check fun x => x + 1 #check fun (x : Nat) => x + 1 #check ((fun (x : Nat) => x + 1) : (Nat -> Nat)) #check (· + 1) #check ((· + 1) : (Nat -> Nat)) # (find-fplean4page 76 "import «Greeting»") # (find-fplean4text 76 "import «Greeting»") Proposition world. A Proposition is a true/false statement, like 2 + 2 = 4 or 2 + 2 = 5. Just like we can have concrete sets in Lean like mynat, and abstract sets called things like X, we can also have concrete propositions like 2 + 2 = 5 and abstract propositions called things like P. Mathematicians are very good at conflating a theorem with its proof. They might say "now use theorem 12 and we're done". What they really mean is "now use the proof of theorem 12..." (i.e. the fact that we proved it already). Particularly problematic is the fact that mathematicians use the word Proposition to mean "a relatively straightforward statement which is true" and computer scientists use it to mean "a statement of arbitrary complexity, which might be true or false". Computer scientists are far more careful about distinguishing between a proposition and a proof. For example: x + 0 = x is a proposition, and add_zero x is its proof. The convention we'll use is capital letters for propositions and small letters for proofs. https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/FAQ.html https://github.com/ImperialCollegeLondon/natural_number_game https://github.com/mpedramfar/Lean-game-maker https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ Picking a basis and then pretending you didn’t https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/zulip.md https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Calling.20lean.20from.20command.20line https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.microsoft.com/en-us/research/uploads/prod/2020/11/perceus-tr-v1.pdf (find-books "__comp/__comp.el" "colton") https://leanprover.github.io/reference/ https://leanprover.github.io/reference/using_lean.html#using-lean-with-emacs https://lawrencecpaulson.github.io/2023/01/18/Sqrt2_irrational.html https://news.ycombinator.com/item?id=34437735 Formalising a new proof that the square root of two is irrational (lawrencecpaulson.github.io) *** https://news.ycombinator.com/item?id=35511152 What I've Learned About Formal Methods in Half a Year (jakob.space) ;; <schemesinlean> ;; https://arxiv.org/abs/2101.02602 ;; https://arxiv.org/pdf/2101.02602.pdf (code-pdf-page "schemesinlean" "$S/https/arxiv.org/pdf/2101.02602.pdf") (code-pdf-text "schemesinlean" "$S/https/arxiv.org/pdf/2101.02602.pdf") ;; (find-schemesinleanpage) ;; (find-schemesinleantext) https://proofassistants.stackexchange.com/questions/2153/type-theory-lean-3-to-lean-4 ;; <ullrichmhm> ;; https://arxiv.org/abs/2001.10490 ;; https://arxiv.org/pdf/2001.10490.pdf ;; Ullrich/Moura: "Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages" (code-pdf-page "ullrichmhm" "$S/https/arxiv.org/pdf/2001.10490.pdf") (code-pdf-text "ullrichmhm" "$S/https/arxiv.org/pdf/2001.10490.pdf") ;; (find-ullrichmhmpage) ;; (find-ullrichmhmtext) ;; <leanteach2020> ;; https://github.com/vaibhavkarve/leanteach2020 ;; https://vaibhavkarve.github.io/leanteach_report.pdf ;; https://wiki.illinois.edu/wiki/display/LT2020/LeanTeach+2020+Home ;; Dolcos/Kong/Zhao/Phillips/Karve: "Interactive Theorem Proving in Lean" (code-pdf-page "leanteach2020" "$S/https/vaibhavkarve.github.io/leanteach_report.pdf") (code-pdf-text "leanteach2020" "$S/https/vaibhavkarve.github.io/leanteach_report.pdf") (code-c-d "leanteach2020" "~/usrc/leanteach2020/") (code-video "leanteach2020video" "~/usrc/leanteach2020/igl_talk.mp4") ;; (find-leanteach2020page) ;; (find-leanteach2020text) # (find-git-links "https://github.com/vaibhavkarve/leanteach2020" "leanteach2020") # (find-leanteach2020file "") # (find-leanteach2020video) # (find-leanteach2020video "0:00") ;; <carneiro> https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf https://github.com/digama0/lean-type-theory/releases/download/v1.0/slides.pdf https://github.com/digama0/lean-type-theory/archive/refs/tags/v1.0.tar.gz https://www.youtube.com/watch?v=3sKrSNhSxik https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/ elaborator https://jiggerwit.wordpress.com/2019/06/20/an-argument-for-controlled-natural-languages-in-mathematics/ https://leanprover.github.io/papers/lean4.pdf # Local Variables: # coding: utf-8-unix # End: