Support devcontainer.json in repo2docker

[yuvipanda]

Problem Statement

As a user of a language ecosystem that has decided to use devcontainers as the primary way to build interactive environments using that language ecosystem (such as Lean4), I want to use mybinder.org (or my own binderhub instance) to build & launch such environments well. This allows me to not just launch from sources like GitHub, but also from published academic sources (like zenodo, dataverse, etc). I want to simply use the norms already present in my community, rather than learn something specific just for mybinder.org

Proposed Solution

Implement support for devcontainers.json in repo2docker.

Proposed Implementation

Dev Containers has a spec that is decently documented. We will pick a specific community to enable, find users in that community, and implement the parts of it that are necessary to make that community feel like a first class citizen on mybinder.org. We can repeat this with multiple communities over time.

How will this fit in the ecosystem?

This expands the set of languages and ecosystems that can be used on mybinder.org, without us having to explode the scope of the specific tools we support.

Endorsements

[cboettig]

Thanks @yuvipanda! I think having any file-based spec for repo2docker would be great, and it makes sense to build on the existing standard. In particular I think devcontainer.json defines a reasonable way to start with a Dockerfile/docker image and modify. Currently using a Dockerfile in repo2docker means basically giving up most of what repo2docker does for us and just owning the whole onion.

Personally I would be quite fine if repo2docker supported some subset of the devcontainer spec. I think the spec itself is a bit over-engineered and I still find the best way to move between devcontainer systems and jupyter systems any anything else is merely to have an appropriate dockerfile :-).