Editing code in your Workspace

Table of contents

1. Using the local files directly from the Workspace
2. Using VSCode’s remote SSH feature
   1. Instructions for Workspace setup
   2. VSCode C/C++ Extension Config

The Workspace gives you access to all the local files that you will need. This will allow you to edit code using text editors on your host and run git commands from inside the Workspace. These files are stored within the ./docker/.workspace directory in the Workspace This is the recommended way of working on code for this course.

Alternatively, if you use VSCode, you can use its remote ssh feature to connect to your Workspace quite easily. This process is detailed below.

These are two suggested ways to edit code in your Workspace, but you are free to do whatever suits you best. Another possibility is just using a non-graphical text editor in an SSH session.

Using the local files directly from the Workspace

1. Change into the directory where the Workspace is found. (i.e cd docker)

2. Change into the .workspace directory

3. Change into the code directory within .workspace

You should now be able to see the contents of the Workspace’s root directory. You can feel free to just edit the appropiate assignment files with any text editor you feel most comfortable with.

Using VSCode’s remote SSH feature

Instructions for Workspace setup

Follow these instructions if you chose Workspace setup. These instructions are for macOS, but the process should be very similar for other OSes.

1. Change into the directory of your Workspace: cd docker.

2. Make sure the Workspace is up and running: docker-compose up -d.

3. Change directories to your .ssh directory: cd ~/.ssh.

4. Generate a new ssh key by running: ssh-keygen -t ed25519 -f inst162.

5. Copy over your public key to the Docker Workspace by running ssh-copy-id -p 16222 -i inst162.pub vagrant@127.0.0.1.

6. Follow instructions 1 - 3 in Editing code on the instructional machines. If you plan to add the SSH configuration of the Workspace to your machine, one example can be:

Host workspace
  HostName 127.0.0.1
  Port 16222
  User vagrant
  PreferredAuthentications publickey
  IdentityFile "~/.ssh/inst162"

VSCode C/C++ Extension Config

To enable useful IDE features like code navigation and warning/error highlighting, first install the C/C++ Extension Pack within your Remote SSH VSCode instance.

For Pintos-based assignments, the following custom config will enable development that mirrors the build system we use:

1. Open the VSCode command palette and run the C/C++: Edit Configurations (JSON) command to open the config file.

2. Replace the existing contents with:

{
    "configurations": [
        {
            "name": "pintos",
            "includePath": [
                "${workspaceFolder}/**"
            ],
            "defines": [
                "USERPROG",
                "THREADS",
                "FILESYS"
            ],
            "compilerPath": "/usr/bin/gcc",
            "cStandard": "c11",
            "intelliSenseMode": "linux-gcc-x64",
            "configurationProvider": "ms-vscode.makefile-tools",
            "compilerArgs": [
                "-nostdinc",
                "-I../..",
                "-I../../lib",
                "-I../../lib/kernel",
                "-Wall",
                "-W",
                "-Wstrict-prototypes",
                "-Wmissing-prototypes",
                "-Wsystem-headers"
            ]
        }
    ],
    "version": 4
}

1. Save the file and enjoy!