# This file:
#   http://anggtwu.net/LEAN/2025-install.sh.html
#   http://anggtwu.net/LEAN/2025-install.sh
#          (find-angg "LEAN/2025-install.sh")
# Author: Eduardo Ochs <eduardoochs@gmail.com>
# See: (find-es "lean" "install-2025")

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)

du -ch  ~/.elan/
rm -Rfv ~/.elan/

rm -Rfv /tmp/elan-install/
mkdir   /tmp/elan-install/
cd      /tmp/elan-install/
wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
sh elan-init.sh --verbose --no-modify-path -y

find     ~/.elan/
ls -lAF  ~/.elan/
ls -lAF  ~/.elan/bin/
du -chd2 ~/.elan/
# ^ Output: 
#   13M   total

cat ~/.elan/env
export PATH="$HOME/.elan/bin:$PATH"
cd /tmp/elan-install/
cat > test1.lean <<'%%%'
  def main := IO.println "Hello"
%%%
lean --run test1.lean
# ^ Output:
#   info: downloading https://releases.lean-lang.org/lean4/v4.19.0/lean-4.19.0-linux.tar.zst
#   info: installing /home/edrx/.elan/toolchains/leanprover--lean4---v4.19.0
#   Hello

du -chd2 ~/.elan/
# ^ Output:
#   1.6G   total

cat > test2.lean <<'%%%'
  #check List.map
%%%
lean test2.lean



# Local Variables:
# coding:  utf-8-unix
# End: