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