Skip to content

Conversation

@mans0954
Copy link
Contributor

@mans0954 mans0954 commented Jul 24, 2024

The original markdown package is unmaintained [1]. There is apparently a replacement, but it is still in alpha [2]. rustup (from which elan was forked) switched to using pulldown-cmark [3] five years ago.

I am the Debian package maintainer for elan[4] and rust-markdown[5]. I've been asked [6] if elan can please drop the dependency on markdown in order that rust-markdown can be removed from Debian.

This PR is a port of [3a-d] to elan.

N.B. I am not a rust developer, but I have checked that this PR compiles.

[1] https://rustsec.org/advisories/RUSTSEC-2022-0044.html
[2] https://github.com/wooorm/markdown-rs
[3a] rust-lang/rustup#2009
[3b] rust-lang/rustup#3071
[3c] rust-lang/rustup#3662
[3d] rust-lang/rustup#3838
[4] https://packages.debian.org/sid/elan
[5] https://packages.debian.org/source/sid/rust-markdown
[6] https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1040514#25

@Kha
Copy link
Member

Kha commented Jul 31, 2024

Thanks! Unfortunately, the line wrapping and indentation is a bit wonky with this change.

$ export ELAN_INIT_SKIP_PATH_CHECK=yes; (curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh)
info: downloading installer

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/sebastian/.elan/bin

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

  /home/sebastian/.profile
  /home/sebastian/.zprofile

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
^C
$ 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/sebastian/.elan/bin

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

  /home/sebastian/.profile
/home/sebastian/.zprofile

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
^C

@mans0954
Copy link
Contributor Author

@Kha sorry for the long delay in getting back to this. I think I've fixed it now. How does this look?

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
3 

info: aborting installation

(N.B. I've added in bullet points for the list, which were missing before.)

@mans0954
Copy link
Contributor Author

Post install message before:

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

Post install message now:

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

@Kha
Copy link
Member

Kha commented Sep 17, 2025

Great, thank you!

@Kha Kha merged commit 87552c2 into leanprover:master Sep 17, 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