|
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: