Allow configuring used IDE Image per workspace

[svenefftinge]

Currently, in closed beta we allow users to provide a docker image, containing the IDE to run in their workspaces.
This currently can be set on the user settings and would effect all workspaces a user starts.
It might be useful to decide this on a per-repository basis, so that the whole team would get the correct IDE when starting and don't need to maintain or change the IDE setting globally.

To support that we should add a property to the .gitpod.yml where an image can be specified.
This setting should have precedence over user-setting level information. We can come up with a solution to disable this precedence once people ask for it with compelling use cases. Until then creating a branch where the property is removed from the .gitpod.yml should be a working (though inconvenient) workaround.

[csweichel]

How would that setting look like in the config.yaml?:

• for forcing Code on everyone:

  ide: code

• for picking a specific IDE image:

  ide: my-registry.com/some-docker/repo:latest

Do we ever want to configure things for the IDE other than its image (paths, env vars, ports)? If so, we could use this instead:

ide:
    image: docker/image:latest

[csweichel]

moved into march because of private beta of this feature. If we wanted to add this now we'd have to check for the IDE_CONFIG permission first

[adibhanna]

Hey! is this an option now?

[stale]

This issue has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. Thank you for your contributions.