fix(sandbox): `mount_dir` for ssh_box

[xingyaoww]

The default for WORKSPACE_MOUNT_PATH is None, which causes issues when try to map it into SSHBox. Right now, SSHBox first read for WORKSPACE_MOUNT_PATH then WORKSPACE_BASE.

Based on our README.md, it seems to me that both of these variable means the same thing. Can we merge them together into one variable (i.e., we keep WORKSPACE_MOUNT_PATH and remove WORKSPACE_BASE)?

...
    -e WORKSPACE_MOUNT_PATH=$WORKSPACE_BASE \
    -v $WORKSPACE_BASE:/opt/workspace_base \
...

[rbren]

I think it might be good to move this logic to config.py--if WORKSPACE_MOUNT_PATH is unset, set it to WORKSPACE_BASE

I believe the logic you have here only works if running outside docker--inside docker it would probably break (though both variables should be set in that case)

[xingyaoww]

Good point! I have moved the code to config.py!

[rbren]

Thanks!