Problem Sets for MIT 6.887 Formal Reasoning About Programs, Spring 2017
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
frap @ e9e8e6b
pset1
pset10
pset11
pset12
pset13
pset2
pset3
pset4
pset5
pset6
pset7
pset8
pset9
.gitmodules
README.md
configure_coqbin.sh

README.md

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.