search

project-everest / everest

https://project-everest.github.io/
Apache License 2.0
193 stars 29 forks source link

config file should be .profile if .bash_profile does not exist #84

Closed tahina-pro closed 3 years ago

tahina-pro commented 3 years ago

I tried to compile Everest on a fresh Ubuntu 18.04 LTS machine, by manually installing and initializing opam before running ./everest check. It turns out that, on such a fresh machine, .bash_profile initially does not exist, so opam init modifies .profile instead. But then, ./everest creates and modifies .bash_profile, which results in bash skipping .profile at the next login; thus, the opam environment is no longer properly set. To solve this issue, I make ./everest modify .profile by default if .bash_profile does not exist.

Context: I am trying to write detailed instructions to compile EverParse on Linux, and I believe that asking the user to manually set EVEREST_ENV_DEST_FILE to account for this case is not user-friendly. We recently received feedback from a new user trying to compile EverParse on Ubuntu 18.04 LTS because they could not run our binary package, which works only with Ubuntu 20.04 because of glibc (that has been corrected since, and we reuploaded a binary package built on Ubuntu 18.04 instead), and they failed because of that issue.

msprotz commented 3 years ago

I guess there's no way to enforce that bash_profile contains source $HOME/.profile? that seems the most sensible choice, then... thanks for fixing that quirk!

tahina-pro commented 3 years ago

I guess there's no way to enforce that bash_profile contains source $HOME/.profile?

Alas, we can't assume or enforce anything like that. I tested myself on a VM and that's how I reproduced the issue.