Zulip Chat Archive

Stream: new members

Topic: fix problem


EDY SAUL CONDORHUANCA RIMACHI (Jan 12 2022 at 16:42):

EDY SAUL CONDORHUANCA RIMACHI11:27 AM
Hi. I have this problem to install. AFTER WRITE THIS echo 'PATH="$HOME/.elan/bin:$PATH"' >> $HOME/.profile. APPEAR THIS ERROR bash: $HOME/.profile.: ambiguous redirect
How to fix?

Kevin Buzzard (Jan 12 2022 at 16:45):

what OS are you on? What do echo $HOME and ls -l $HOME/.profile show?

EDY SAUL CONDORHUANCA RIMACHI (Jan 12 2022 at 16:45):

windows

Eric Rodriguez (Jan 12 2022 at 16:52):

(deleted)

Eric Rodriguez (Jan 12 2022 at 16:54):

sorry, I'm wrong. which of the two shells are you running this on?

EDY SAUL CONDORHUANCA RIMACHI (Jan 12 2022 at 16:55):

on git bash

Eric Rodriguez (Jan 12 2022 at 17:01):

can you type cat $HOME/.profile?

Eric Rodriguez (Jan 12 2022 at 17:01):

what does it output?

EDY SAUL CONDORHUANCA RIMACHI (Jan 12 2022 at 17:04):

this cat: /c/Users/EDY: No such file or directory
cat: SAUL/.profile: No such file or directory

Eric Rodriguez (Jan 12 2022 at 17:05):

oh! your username has a space

Eric Rodriguez (Jan 12 2022 at 17:06):

try echo 'PATH="$HOME/.elan/bin:$PATH"' >> "$HOME/.profile"

Eric Rodriguez (Jan 12 2022 at 17:06):

this should be fixed in the install instructions

EDY SAUL CONDORHUANCA RIMACHI (Jan 12 2022 at 17:08):

worked, thanks

Arthur Paulino (Jan 12 2022 at 17:12):

Kind of intriguing that nobody else had reported this issue before

Bryan Gin-ge Chen (Jan 12 2022 at 17:17):

Eric Rodriguez said:

this should be fixed in the install instructions

Do you mind opening a PR to fix the file here? Thanks!

Eric Rodriguez (Jan 12 2022 at 17:17):

was already on it! leanprover-community.github.io#242

EDY SAUL CONDORHUANCA RIMACHI (Jan 12 2022 at 23:41):

I´m using this video to install Lean. TI I have other problem. after write this "which python" appears this which: no python in (/c/Users/EDY SAUL/bin:/mingw64/bin:/usr/local/bin:/usr/bin:/bin:/mingw64/bin:/usr/bin:/c/Users/EDY SAUL/bin:/c/WINDOWS/system32:/c/WINDOWS:/c/WINDOWS/System32/Wbem:/c/WINDOWS/System32/WindowsPowerShell/v1.0:/c/WINDOWS/System32/OpenSSH:/cmd:/c/Users/EDY SAUL/.elan/bin:/c/Users/EDY SAUL/AppData/Local/Microsoft/WindowsApps:/usr/bin/vendor_perl:/usr/bin/core_perl)

EDY SAUL CONDORHUANCA RIMACHI (Jan 12 2022 at 23:44):

I have installed python

EDY SAUL CONDORHUANCA RIMACHI (Jan 13 2022 at 16:24):

i solved my problem


Last updated: Dec 20 2023 at 11:08 UTC