Introducing a minimal devcontainer (for codespaces) #2998
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds the
.devcontainer
directory with a specification for how to create an F* devcontainer. This devcontainer is what's used to generate a 'codespace', which is just a devcontainer running on Github's servers.The container is based on a Dockerfile that installs our usual dependencies, and will also run
make
as part of the creation process. Also, it automatically installs the F* vscode extension, so starting a codespace will give a usable F* out of the box.The container can also be run locally within vscode by just using the "Reopen in container" command. VS Code will in fact automatically suggest that when opening the workspace.
I tried to base this container on top of Github's codespace image (instead of a plain Ubuntu image), but I got different behaviors when running locally and on codespaces.. so I dropped that idea for now.
Note: when someone creates a codespace from the F* repo, the resource consumption (/ billing) runs on their tab. Having this file here should not use any resources from the FStarLang org.