Assignment 08 Status - Githubissues

jeehoonkang commented 9 years ago

Hi all,

Assignment 08 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 08.
- Do your homework by editing sf/Assignment08_??.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

AdamBJ commented 9 years ago

What section in the text does this homework go up to? Also, when is it due? Since it was released a bit later than usual, will we have some extra time to finish it?

jeehoonkang commented 9 years ago

@AdamBJ Due is written in the README. The assignment is issued slightly later than usual, but the due will be the same: 14:00 Thr.

AdamBJ commented 9 years ago

@jeehoonkang When I click the link for the README I get a 404 error. Is the coverage of the assignment written in the README too? It helps to have it for planning purposes.

jeehoonkang commented 9 years ago

Readme is here: https://github.com/snu-sf/pl2015
I am not quite sure how much this assignment covers in the material.

jeehoonkang commented 9 years ago

@AdamBJ It seems the assignment covers Imp.v.

SungMinCho commented 9 years ago

Problem 08_05 suggests us to change the behavior of s_execute when it meets SPlus, SMinus or SMult when the stack has less than two elements. Are we allowed to change 08_00 in order to do so?

sanha commented 9 years ago

Compiling the Assignment8_00.v file takes very long time and not end, even though I already compiled the SfLib.v and compiling other files do not makes any problem. And a few students encounter similar problem. What should I do?

jeehoonkang commented 9 years ago

@SungMinCho I think the issue is related to #101 . Would you please discuss there? @sanha I think the issue is related to #99 . Would you please discuss there?