gbenm/pintos repository overview

⁠PintOS

Environment ready to run PintOS project.

⁠Use

⁠Preconfigured

Visit this page⁠.

⁠Volumes

• /pintos here you should mount your pintos code
• /host allows you to change .bashrc config and share other files

⁠Users

• root if you don't specify a user with docker flag -u USER
• pintos (-u pintos) has UID=1000 and GID=1000
  • groups: pintos, sudo
  • run passwd to set a password for this user

⁠Symbolic links

• /root/host -> /host
• /root/pintos -> /pintos
• /home/pintos/host -> /host
• /home/pintos/pintos -> /pintos

⁠Standalone

docker run --rm -it -v ~/pintos:/pintos -v ~/pintos/pintos-docker:/host  gbenm/pintos:latest /bin/bash

Inside of container run (if you use root user)

source bash-config

Inside of container run (if you use pintos user)

sudo bash-config
source ~/.bashrc
sudo chown pintos.pintos ~/.bashrc # change de ownership (optional)

After executing the previous command, .bashrc will be copied in /host , that is, inside the mounted volume.

• Note: /pintos must contain the PintOS source code, or you will need to add the path of scripts (pintos, Pintos.pm, etc) to .bashrc manually.