snu-sf-class/pl2015spring

Assignment 06 Status

jeehoonkang opened this issue · 7 comments

jeehoonkang commented

Hi all,

  • Assignment 06 is issued.

  • Please read Homework.md to know how to fetch homework and submit your answer.

    • You have to run ./fetch-homework.sh to get assignment 06.
    • Do your homework by editing sf/Assignment06_??.v.
    • Make sure make works without errors.
    • Commit and push to your GitHub repository.
    • Make sure https://github.com/$YOURID/pl2015 contains the change you made.

  • Stay tuned for README.md and this issue on the assignment.

  • You are NOT allowed to use the admit tactic
    because admit 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.

  • Do NOT add any additional Require Import/Export.

Sincerely,
Jeehoon

jeehoonkang commented

I will upload automated grader for evaluation purposes.

jaewooklee93 commented

In Assignment_06_07.v, proofs for Examples are already given in the comments, can we just use it? :)

jeehoonkang commented

@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

jeehoonkang commented

I made an automatic grader: http://sf.snu.ac.kr/jeehoon.kang/pl2015/Assignment06_grader.tar.gz

  • You have to use it with bash, and sed should be installed in your machine. You can use these programs in the martini.snucse.org and midori.snucse.org servers.
  • Place your Assignment06_??.v files in submission folder. NOTE: original folder should be intact.
  • Run by ./grader.sh.
  • If your submission has a compilation error, then an error message will be present.

Hope this grader will help you prepare a good submission.

Jeehoon

rhs0266 commented

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.

jeehoonkang commented

Submissions are collected.

jeehoonkang commented

Delay submissions are collected.