snu-sf-class/pl2015spring

Assignment 09 Status

jeehoonkang opened this issue · 6 comments

Hi all,

  • Assignment 09 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 09.
    • Do your homework by editing sf/Assignment09_??.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.
  • You are ALLOWED to use any tactics including: [tauto], [intuition], [firstorder], [omega].
  • Just leave [exact FILL_IN_HERE] for those problems that you fail to prove.
  • Do NOT add any additional Require Import/Export.

Sincerely,
Jeehoon

submissions are collected.

The grader does not work, with a following message.
grader.sh: 20: grader.sh: Syntax error: "(" unexpected

@fortunist what's your environment? OS, shell, ...

It failed in the martini.snucse.org server.
However, it works well in my notebook.

Delay submissions are collected.