jee...@sf.snu.ac.kr and jun...@sf.snu.ac.kr.| Due | Due (Delay) | Description | Points |
|---|---|---|---|
| Oct.3 23:59 | Oct.10 23:59 | Assignment 1 | 50 |
| Oct.10 23:59 | Oct.17 23:59 | Assignment 2 | 100 |
| Oct.17 23:59 | Oct.24 23:59 | Assignment 3 | 60 |
| Oct.24 23:59 | Oct.28 23:59 | Assignment 4 | 110 |
| Oct.31 23:59 | Nov.07 23:59 | Assignment 5 | 80 |
| Nov.07 23:59 | No delay | Assignment 6 | 130 |
| Nov.30 23:59 | No delay | Assignment 7 | 170 |
| No delay | Assignment 8~12 | 200(total) |
Exams: 75%70% (mid-term 35% 30% and final 40%)
Assignments: 20% 25%
S.S * (1 - f(N)).Attendance: 5%
Use Coq 8.5pl2. DO NOT use other versions.
Install Coq.
Installer (OS X / Windows)
Cygwin For Windows
make).
bash and make (in Select packages). Installation may take a long time.PATH variable.
~/.bashrc or ~/.bash_profile).C:\cygwin\home\[USER_ID].export PATH=$PATH:/cygdrive/c/Program\ Files\ \(x86\)/Coq/bin/ at the end of the file. The directory to add may be different for your environment.~/.bashrc.which coqc in the terminal. It should point to the coqc binary.OPAM (Linux / OS X)
Install necessary libraries.
OS X
# install brew (http://brew.sh/index.html)
brew install gtksourceview libxml2CentOS-like Linux
sudo yum install gtksourceview2-develDebian-like Linux
sudo apt-get install liblablgtksourceview2-ocaml-devInstall opam, and make sure you can use OCaml 4.03.0.
opam init --comp 4.03.0
opam install coqide.8.5.2
Test by coqc -v in the command line. Check your PATH variable if you get an error.
Run CoqIDE by coqide.
Use IDEs supporting Coq.
sf/ directory.assignments/$NAME directory is the assignment $NAME.
P??.v files. You should edit only P??.v. DO NOT TOUCH ANYTHING ELSE.E??_??.v files are for evaluation.make in the terminal to compile files so that IDE can understand them.P??.v files to do the assignment.make in the terminal to compile your submission. make eval in the terminal to grade your submission yourself. make and make eval SHOULD SUCCEED. If not, your score will be 0.make eval will check your submission.
P??.v files SHOULD NOT contain admit, Admitted, and anything in forbidden.txt.P??.v file contains string FILL_IN_HERE, then it will be scored 0.make submission to prepare your submission.
zip should be installed. Otherwise, you can just zip P??.v.http.SYSTEM ERROR or RUNNING for a long time, even after refreshing your web browser for several times, please ask the TA.If you run coqide from a terminal, you may get the following error message. But it is okay.
(process:16700): Gtk-WARNING **: Locale not supported by C library.
Using the fallback 'C' locale.If something bad happens, please download the most recent version of the assignments.
You may have to make before interacting with IDEs.
You can specify the CRLF handling strategy in Git (cf). In Windows, some strategies may break the Makefile. Please just use the linebreaks as in the repository.
When running CoqIDE in OS X for the first time, you may see an error message saying Failed to load coqtop. Then click No, and then find /Applications/CoqIDE_8.4pl5.app/Contents/Resources/bin/coqtop and open for once. Then goto CoqIDE > Preferences > Externals. And then change coqtop into /Applications/CoqIDE_8.4pl5.app/Contents/Resources/bin/coqtop.
Your submission file should have alphanumeric characters only.
If cygwin complains like ./check.sh: line 2: $'\r': command not found, please:
dos2unix in Cygwin.dos2unix check.shIf you use Coquille (on Vim) and your terminal is hidden by some message (warning (some rule has been masked)), please edit ~/.vim/.../coquille/autoload/coquille.py's restart_coq as follows (NOTE: stderr = subprocess.PIPE):
def restart_coq(*args):
global coqtop
if coqtop: kill_coqtop()
try:
coqtop = subprocess.Popen(
["coqtop", "-ideslave"] + list(args),
stdin = subprocess.PIPE,
stdout = subprocess.PIPE,
stderr = subprocess.PIPE,
preexec_fn = ignore_sigint
)
except OSError:
print("Error: couldn't launch coqtop")Thank you for reporting, @indiofish