search

leanprover / elan

The Lean version manager
Apache License 2.0
297 stars 34 forks source link

[Question] How to automatically use default installation (with no prompt) #60

Closed luiz00martins closed 2 years ago

luiz00martins commented 2 years ago

I'm using elan-init.sh to install elan, with the following command:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

It first prompts you for some customization or cancelling, which is great if you're installing manually. However, I'm running elan-init.sh inside a script.

Is there a way to avoid the prompt and use the default installation method?

Kha commented 2 years ago

Yes, you can pass additional arguments after -s --

$ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --help
elan-init 1.0.0 (408ed84 2017-02-11)
The installer for elan

USAGE:
    elan-init [FLAGS] [OPTIONS]

FLAGS:
    -v, --verbose           Enable verbose output
    -y                      Disable confirmation prompt.
        --no-modify-path    Don't configure the PATH environment variable
    -h, --help              Prints help information
    -V, --version           Prints version information

OPTIONS:
        --default-toolchain <default-toolchain>    Choose a default toolchain to install
        --default-toolchain none                   Do not install any toolchains