Assignment 10 status

[jeehoonkang]

Hi all,

• Assignment 10 is issued. Please see the README for more details.
• Please read Homework.md to know how to fetch homework and submit your answer.
  • You have to run ./fetch-homework.sh to get assignment 10.
  • Do your homework by editing sf/Assignment10_??.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

[sanha]

I wonder why the due of HW 10 & 11 is 4th June. As you know, this week is very busy week because it is closer to the end of semester, so there are final exams and reports' due on it.

[AdamBJ]

@jeehoonkang Are both assignments due on the 4th? Or are you posting assignment 11 early?

Are these the last two assignments?

[qkr0990]

I Think nf_is_value is needed to solve 10_06.... and the lemma does not exist on Assignment_10_0.. so i import it, but also it needs strong_progress... Is there any other way to solve it without those Lemmas?

and good news is that I finally found the way not blocking the email!

[jeehoonkang]

• @sanha @AdamBJ Yes, the due of both assignments is 4th June. I am sorry that this course is a little bit demanding.
• @AdamBJ I will ask @gilhur .
• @qkr0990 If you need the lemmas, prove them in Assignment10_06.v and use it.

[jeehoonkang]

@qkr0990
너의 그 한 마디 말도 그 웃음도 / 나에겐 커다란 의미
너의 그 작은 눈빛도 쓸쓸한 그 뒷모습도 / 나에겐 힘겨운 약속
너의 모든 것은 내게로 와 / 풀리지 않는 수수께끼가 되네
슬픔은 간이역의 코스모스로 피고 / 스쳐 불어온 넌 향긋한 바람
나 이제 뭉게구름 위에 성을 짓고 / 널 향해 창을 내리 바람 드는 창을

[qkr0990]

@jeehoonkang I think that I remove the email from the spam list but... I didn't confirm it... I really apologize about that and I think that It would not happen again. Thanks.

[qkr0990]

Is it Possible to use 'exact FILL_IN_HERE for the lemmas that appears in SmallStep.v but it's prove is just Admit?
I mean If i want to use lemmas that don't exist on Assignment10_00, but i'm tired of proving them again, then can i use exact FILL_IN_HERE for that kinds of lemmas?

[jeehoonkang]

@AdamBJ @jaewooklee93 We will cover References.v at the end of this class. The last assignment will be issued 11 June.

[jeehoonkang]

@qkr0990 I am sorry for your inconvenience, but that will complicate my grading procedure. Please copy and paste things for some more assignments. Once more I am sorry, and thank you in advance.

Jeehoon

[alkaza]

I'm sorry, but giving 26 assignments during the final week is crazy... ㅠㅠ

[AdamBJ]

@jeehoonkang I agree with @alkaza that it's crazy to assign so much, especially considering that we're so close to finals. And not only do we have all the assignments to do, we also have to read all the chapters in the textbook that we're covered. I don't understand why we are rushing so much now when everyone is so busy with final week.

Regardless, if the last assignment is going to be issued June 11th, why are both A10 and A11 due on the 4th? Why not have A11 issued on June 5th or 6th or something like normal?

[alkaza]

Yes, if HW11 was dues June 11th it would help a lot!

On Sun, May 31, 2015 at 6:02 PM, AdamBJ notifications@github.com wrote:

@jeehoonkang https://github.com/jeehoonkang I agree with @alkaza
https://github.com/alkaza that it's crazy to assign so much, especially
considering that we're so close to finals. And not only do we have all the
assignments to do, we also have to read all the chapters in the textbook
that we're covered. I don't understand why we are rushing so much now when
everyone is so busy with final week.

Regardless, if the last assignment is going to be issued June 11th, why
are both A10 and A11 due on the 4th? Why not have A11 issued on June 5th or
6th or something like normal?

—
Reply to this email directly or view it on GitHub
#135 (comment).

[jeehoonkang]

For due date: #136

[jeehoonkang]

Here is the grader: http://sf.snu.ac.kr/jeehoon.kang/pl2015/Assignment10_grader.zip

[jeehoonkang]

Submissions are collected.