Open jeehoonkang opened 9 years ago
I will upload automated grader for evaluation purposes.
In Assignment_06_07.v
, proofs for Example
s are already given in the comments, can we just use it? :)
@jaewooklee93 Yes you can. I believe the essence of the exercise is defining the nostutter
relation itself. Proving examples with the already-given comments looks good to me.
Jeehoon
I made an automatic grader: http://sf.snu.ac.kr/jeehoon.kang/pl2015/Assignment06_grader.tar.gz
bash
, and sed
should be installed in your machine. You can use these programs in the martini.snucse.org
and midori.snucse.org
servers.Assignment06_??.v
files in submission
folder. NOTE: original
folder should be intact../grader.sh
.Hope this grader will help you prepare a good submission.
Jeehoon
Thanks for uploading grader!
If someone have problem about using ./grader.sh
such as ~~ permissiong denied
, write chmod a+x *.sh
at directory which contains ./grader.sh
.
Submissions are collected.
Delay submissions are collected.
Hi all,
./fetch-homework.sh
to get assignment 06.sf/Assignment06_??.v
.make
works without errors.https://github.com/$YOURID/pl2015
contains the change you made.You are NOT allowed to use the
admit
tactic becauseadmit
simply admits any goal regardless of whether it is provable or not.But, you can leave
admit
for problems that you cannot prove. Then you will get zero points for those problems.You are NOT allowed to use the following tactics.
tauto
,intuition
,firstorder
,omega
.Require Import/Export
.Sincerely, Jeehoon