This "development box" is a VM and a bundle of scripts that help make setting
up a build environment and getting all of the Robigalia repositories less of a
chore. This uses Vagrant and an increasingly gnarly
shell script (
bootstrap.sh) to automate setting up the VM.
First, install Vagrant and VirtualBox. Arch, Debian, etc have packages for it.
- Then, clone this repo. You should give the clone a better name than "devbox". rbg or robigalia are popular choices.
vagrant upand wait for the VM to finish initializing.
vagrant sshand you're done!
The devbox directory on the host will appear as
/vagrant in the VM, and is a
shared folder. We recommend using the VM only for building, and doing editing,
git, etc on the host. This keeps the VM relatively stateless, which is nice
If your system is memory constrained, or does not have hardware-assisted virtualization, you may want to set up your own build environment. You can also edit the Vagrantfile to change the number of cores or amount of memory dedicated to the VM.
Using the repo-management scripts
Because cmr thought it was too complex and nearly-worthless without Gerrit,
and for lack of an easy solution, we have our own simple scripts for managing
our large amount of repositories. There is a file,
.subrepos, which has the
list of repositories to be cloned from https://gitlab.com/robigalia.
./get_new_repos.sh will clone new repositories from
.subrepos that don't
already exist on the filesystem.
./add_remotes.sh will first rename the
origin remote to
then add a remote
origin which points to what would be your own fork of the
repository if you had it,
ssh://email@example.com/cmr/sel4-sys.git for example.
It will prompt you for your username, but you can also supply it as the first