-
-
Notifications
You must be signed in to change notification settings - Fork 663
Devcontainer: use devcontainer id as key for venv and build directory #40821
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: develop
Are you sure you want to change the base?
Conversation
... otherwise different devcontainers would try to reuse the same venv/build directory - which will not work as the underlying os of the devcontainer can be quite different.
please more background in the PR's description. What is a devcontainer? |
Documentation preview for this PR (built with commit 90f6c93; changes) is ready! 🎉 |
A devcontainer allows you to open the sagemath source in a different docker container and then use that as your dev env (more details at https://code.visualstudio.com/docs/devcontainers/containers). I use it to test the meson setup on different linux distros. It's also used for the github codespaces. Since, with devcontainers, you can open the same sagemath source in different os, their virtual env and build folders need to be distinguished - otherwise your archlinux devcontainer is trying to reuse build artifacts from ubuntu. With the changes here, everything is tied to an id that is unique for the particular config. |
I know that one can review PRs in codespace. |
OK - in which scenarios one can have different devcontainers in one SAGEROOT? This would need some kind of overlay filesystem? (perhaps it's how Docker works, I just don't know) |
Not with the codespaces on github, of course. But there is a "Devcontainer" extension in vs code that allows you to reopen an arbitrary folder in a given devcontainer. So in particular you can have SAGEROOT open in multiple devcontainers at the same time, all with the same shared code. |
Thanks! |
... otherwise different devcontainers would try to reuse the same venv/build directory - which will not work as the underlying os of the devcontainer can be quite different.
📝 Checklist
⌛ Dependencies