Lean Lang Learning Notes

Elan (version manager)

What is Elan

• Elan is version manager for Lean
• It can install and update Lean.
• I recommend using elan to install Lean.

Install Elan

see

• https://github.com/leanprover/elan

on Microsoft Windows, by default it is installed at

c:/Users/xah/.elan/bin

  elan.exe
  lake.exe
  leanc.exe
  leanchecker.exe
  lean.exe
  leanmake.exe
  leanpkg.exe

on Microsoft Windows , it also adds the lean path to HKEY_CURRENT_USER/Environment/PATH 〔see Windows: Registry Tutorial〕

basic elan commands

• elan self update
• elan default leanprover/lean4:stable

• elan self uninstall

Lake (package manager)

lake is package manager

• lake init x → initialize a Lean package x in the current directory.
• lake help → help

Directory structure of package

if a package is named xxx, the structure is

lakefile.lean  → package config
lean-toolchain → specifies the lean version to use
Xxx.lean       → main file, import via `import Xxx`
Xxx/
 A.lean       → further files, import via e.g. `import Xxx.A`
 A/...        → further nesting
.lake/         → `lake` build output directory

after a build, output is at

./.lake/build/bin/xxx

Lean Command Line Options

lean --help
Lean (version 4.18.0, x86_64-w64-windows-gnu, commit 11ccbced7964, Release)
Miscellaneous:
  -h, --help             display this message
      --features         display features compiler provides (eg. LLVM support)
  -v, --version          display version information
  -V, --short-version    display short version number
  -g, --githash          display the git commit hash number used to build this binary
      --run              call the 'main' definition in a file with the remaining arguments
  -o, --o=oname          create olean file
  -i, --i=iname          create ilean file
  -c, --c=fname          name of the C output file
  -b, --bc=fname         name of the LLVM bitcode file
      --stdin            take input from stdin
      --root=dir         set package root directory from which the module name
                         of the input file is calculated
                         (default: current working directory)
  -t, --trust=num        trust level (default: max) 0 means do not trust any macro,
                         and type check all imported modules
  -q, --quiet            do not print verbose messages
  -M, --memory=num       maximum amount of memory that should be used by Lean
                         (in megabytes)
  -T, --timeout=num      maximum number of memory allocations per task
                         this is a deterministic way of interrupting long running tasks
  -j, --threads=num      number of threads used to process lean files
  -s, --tstack=num       thread stack size in Kb
      --server           start lean in server mode
      --worker           start lean in server-worker mode
      --plugin=file      load and initialize Lean shared library for registering linters etc.
      --load-dynlib=file load shared library to make its symbols available to the interpreter
      --json             report Lean output (e.g., messages) as JSON (one per line)
  -E  --error=kind       report Lean messages of kind as errors
      --deps             just print dependencies of a Lean input
      --src-deps         just print dependency sources of a Lean input
      --print-prefix     print the installation prefix for Lean and exit
      --print-libdir     print the installation directory for Lean's built-in libraries and exit
      --profile          display elaboration/type checking time for each definition/theorem
      --stats            display environment statistics
      -D name=value      set a configuration option (see set_option command)

Lean Tutorials

• lean tutorials