Console.note from update_dot_profile can give erroneous or bad advice

[shonfeder]

While setting up a Dockerized OCaml environment, different builds of the container included these notes:

[NOTE] Make sure that ~/.bashrc is well sourced in your ~/.bashrc.

[NOTE] Make sure that ~/.profile is well sourced in your ~/.bashrc.

The first is guaranteed to lead directly to a seg fault from infinite sourcing, and the second is liable to do the same indirectly (see https://askubuntu.com/a/980143/503686).

A simplistic fix would be to add a check dot_profile <> ~/.bashrc && dot_profile <> ~/.profile to

opam/src/state/opamEnv.ml

Lines 590 to 596 in 6607da2

	let update_dot_profile root dot_profile shell =
	let pretty_dot_profile = OpamFilename.prettify dot_profile in
	let bash_src () =
	if shell = SH_bash || shell = SH_sh then
	OpamConsole.note "Make sure that %s is well %s in your ~/.bashrc.\n"
	pretty_dot_profile
	(OpamConsole.colorise `underline "sourced")

However, I suspect it's likely we just want a better way of of handling this sourcing, if one can be found.

[rjbou]

Indeed, sourcing .bashrc in .bashrc is quite an add advice.
Concerning sourcing .profile in .bashrc, it comes from the default config file chosen

opam/src/core/opamStd.ml

Lines 881 to 895 in 6607da2

	List.find Sys.file_exists [
	(* Bash looks up these 3 files in order and only loads the first,
	for LOGIN shells *)
	home ".bash_profile";
	home ".bash_login";
	home ".profile";
	(* Bash loads .bashrc INSTEAD, for interactive NON login shells only;
	but it's often included from the above.
	We may include our variables in both to be sure ; for now we rely
	on non-login shells inheriting their env from a login shell
	somewhere... *)
	]
	with Not_found ->
	(* iff none of the above exist, creating this should be safe *)
	home ".bash_profile")

The thing is, sometimes .bashrc is sourced in the .profile, which can lead to the infinite sourcing if it is done in the other way also. In the other hand, if non of these init files source .bashrc, added configuration is not integrated the user shell session.

You can find some related discussions in #533 & #1447

[cpitclaudel]

Relevant discussion: https://askubuntu.com/questions/432508/why-does-ubuntus-default-profile-source-bashrc

[rjbou]

Closing this issue. Feel free to reopen it if needed.
Thanks!