Skip to content

Troubleshooting ‐ Environment Setup

Jump to bottom
Haofan Zheng edited this page Apr 9, 2024 · 5 revisions

VSCode in General

  • VSCoq Legacy Extension Shows Error Message: Error: Cannot find a physical path bound to logical path Basics with prefix LF.

    • Please create a file named _CoqProject under the root of the git repo with the following content

      -Q ./lf/full  LF
-Q ./plf/full PLF

    • (it should look the same as: https://github.com/UCSC-CSE-210A/cse-210a-sf/blob/main/_CoqProject)

    • If you attempted fixing this issue by changing the settings of the extension, please remember to reset it to default, otherwise, this fix might not work

    • After this file is created and saved, fully restart VSCode, so that the VSCoq Legacy extension will load in this new file

    • Please also note that the functionality of the VSCoq extension depends on the compiled *.vo files, so please refer to Run make HW_filename Test.vo Command to compile the source of the previous homework.

When using Dev Container locally

  • [Common issue on Linux OS] Docker needs root or sudo permission to start
    • Docker in Linux OS (e.g., Ubuntu, CentOS, etc.) has two modes
      • rootful mode (which requires root privileges)
      • rootless mode (which don't requires root privileges)
    • In most of cases, the Linux installation of Docker uses rootful mode
    • The easiest way to test which mode your docker is running on is to run command docker ps and see what it prints
      • If it prints permission denied while trying to connect ..., that means your docker is in rootful mode
      • If it prints a list of containers (or an empty list), that means your docker is in rootless mode
    • When you open your repo in VSCode with Dev Container, VSCode will attempt to run docker commands with your user account privileges, which will cause "permission denied" issue if the docker is in rootful mode
    • To solve this issue, please follow the instructions in https://docs.docker.com/engine/install/linux-postinstall/ to enable managing docker for non-root users
  • [Common issue on Windows OS] Error message: You are not the owner of '/workspaces/.../'., or other error messages complaining about the owner of the file or file permission

    • You may receive this error message when devcontainer is running on Windows platform, due to the incompatible access control scheme used by Windows and Linux

    • To solve this issue, run the following command within the devcontainer, under the directory of /workspaces

      sudo chown -R $USER:$USER ./*
  • [Only applicable to MacOS] There are two versions of Docker Desktop for MacOS: Intel-chip version and Apple-chip version
    • If your Mac has an Intel CPU, please download and install the Intel-chip version
    • If your Mac has an Apple CPU (e.g., M1, M2, M3, etc.), please download and install the Apple-chip version

When using Dev Container on Codespaces

  • if you see error message: resource exhausted (No space left on device), or other error messages saying no space left on device/disk
    • When the Codespaces just being created, it still needs some time to get more storage spaces. Therefore, if you attempt to run commands right after the Codespaces has been created, it may show this error.
    • You can wait for a few minutes and retry your command.
    • In the future, when you start a new Codespaces, give it one minute before running any commands, because Codespaces needs to set up storage.

When installing Coq manually

  • Error message: Command 'coqc' not found, command not found: coqc, or Command 'coqtop' not found
    • After Coq is installed, the executables of coqc, coqtop, etc. are not in the PATH, so the OS doesn't know where are these executables.
    • By running the following command, coqc will be added to PATH in the current terminal, and you can run coqc --version without error; but if you open another terminal, the same error will happen 
      eval `opam config env`
    • Therefore, it's recommended to add the above command to the end of the following files (this is highly OS and configuration dependent, different OS and configurations need to use different file)
      • [for Linux OS] ~/.profile file
      • [for Linux OS, and if you use bash as default shell] ~/.bashrc file
      • [for MacOS] ~/.zprofile file
  • VSCoq Legacy extension error message: Could not start coqtop
    • Usually it's due to the same issue as mentioned above, so please following the steps above to add command eval `opam config env` to the end of profile file
    • Verify that in any newly opened terminals, you can run coqc --version directly without any issue
    • Now, it's very important to restart the VSCode
      • The VSCode was opened before coqc is added to PATH, so extensions in VSCode can't find coqc and coqtop yet
      • After restart VSCode, it will load in the latest PATH variable, and then extensions in VSCode and now find the coqc and coqtop
      • For Mac, closing the VSCode window is not enough, since VSCode process is still running in background, so it's required to right click VScode to quit the process
      • If you are not sure, reboot the computer will also help

Clone this wiki locally