Skip to content

Conversation

@mans0954
Copy link
Contributor

@mans0954 mans0954 commented Oct 4, 2025

@mans0954
Copy link
Contributor Author

mans0954 commented Oct 4, 2025

Installation:

ELAN_INIT_SKIP_PATH_CHECK=yes ./elan-init

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, lake, for editing files not 
belonging to any package.

It will add the lake, lean, and elan commands to Elan's bin directory, located 
at:

  /home/mans0954/.elan/bin 

This path will then be added to your PATH environment variable by modifying the
profile file located at:

  /home/mans0954/.profile 

You can uninstall at any time with elan self uninstall and these changes will 
be reverted.

Current installation options:

    *    default toolchain: stable
    * modify PATH variable: yes


1) Proceed with installation (default)
2) Customize installation
3) Cancel installation
1

info: default toolchain set to 'stable'

Elan is installed now. Great!

To get started you need Elan's bin directory ($HOME/.elan/bin) in your PATH 
environment variable. Next time you log in this will be done automatically.

To configure your current shell run source $HOME/.elan/env

Uninstall:

elan self uninstall


This will uninstall all Lean toolchains and data, and remove $HOME/.elan/bin 
from your PATH environment variable.

Continue? (y/N) y

info: removing elan home
info: removing elan binaries
info: elan is uninstalled

@Kha Kha merged commit 2a16e96 into leanprover:master Oct 6, 2025
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants