Problem Sets for MIT 6.887 Formal Reasoning About Programs

Simple instructions for all psets

Setting PATH for coqc

$ PATH=(your bin directory where coqc resides):$PATH
$ export PATH

• Where is my bin directory?
  • CoqIDE users
    • CoqIDE bundle already includes binaries, so we can use them.
    • Windows: the directory where coqide.exe is located. Make sure coqc.exe is also in there.
    • Mac: (Your CoqIDE app path)/Contents/Resources/bin
  • Users who installed Coq with Homebrew
    • The typical path is /usr/local/bin, but it may differ by Homebrew configuration.
  • All other users who manually installed Coq: just the location you gave during ./configure
• I recommend to embed above commands in your ~/.bashrc or ~/.zshrc.

Building problem sets

$ source configure_coqbin.sh # optional
$ git submodule init
$ git submodule update
$ make -C frap lib
$ make -C pset1

• Above procedure assumes PATH is set for detecting coqc (check with which coqc!).
• You should execute configure_coqbin.sh with source (or just .) in order to export the variable to the parent process.
• If you already set the COQBIN variable, you don't need to execute the script.