Zulip Chat Archive

Stream: new members

Topic: install elan in external hard drive

Esteban Estupinan (Jun 29 2021 at 21:56):

hi, how can i install lean in a external drive because the main drive is to small

Esteban Estupinan (Jun 29 2021 at 21:57):

imagen.png i dont want install in drive c

Esteban Estupinan (Jun 29 2021 at 22:04):

the error show that i cant change the path of lean in c drive, is correct uninstall lean, save my lean codes and install newly in the path to external drive? what you recommend?

Floris van Doorn (Jun 29 2021 at 22:04):

Does it give you the option if you select Customize installation? If not, @Sebastian Ullrich might know how to do this.

Esteban Estupinan (Jun 29 2021 at 22:08):

ok i will try uninstalling .lean

Esteban Estupinan (Jun 30 2021 at 00:29):

why cause this error? imagen.png

Wojciech Nawrocki (Jun 30 2021 at 01:01):

You may be able to select another location by setting the ELAN_HOME environment variable.

$ export ELAN_HOME=/abcd
$ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
[...]

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

  /abcd/bin

Sebastian Ullrich (Jun 30 2021 at 07:34):

Yes, that should work

Esteban Estupinan (Jun 30 2021 at 08:14):

thanks, elan is installed already in the external drive

Esteban Estupinan (Jun 30 2021 at 08:30):

but when I write in a terminal leanproject new ... there is an error "winError2 not file found"

Esteban Estupinan (Jun 30 2021 at 08:31):

maybe mathlib will be the problem now?

Last updated: Dec 20 2023 at 11:08 UTC