Claim on Attendance, Assignment & Exam

[jeehoonkang]

On Claim

• Due: 25th June 2015 (Thu) 18:00
• Channel: this issue & pl2015@sf.snu.ac.kr
• Score Boards
  • Attendance: Attendance #164
  • Assignments: https://docs.google.com/spreadsheets/d/1LzOLx22lF3N31D9RDS20Ec8ub_Rq6IA3utD8CNMk9CQ/edit#gid=1422302047
  • Midterm: https://docs.google.com/spreadsheets/d/1LzOLx22lF3N31D9RDS20Ec8ub_Rq6IA3utD8CNMk9CQ/edit#gid=1440146993
  • Final: https://docs.google.com/spreadsheets/d/1LzOLx22lF3N31D9RDS20Ec8ub_Rq6IA3utD8CNMk9CQ/edit#gid=45562073

Answers

• Now all scores are announced without exception.
• @qkr0990: your submissions for assignment 11 is regraded.
• @amoretspero: your submission for final is regraded. The anomaly happened because of your comments that contains FILL_IN_HERE.
• @rhs0266:
  • 6-8: grader should have pointed out that your submission is invalid, and I would like not to accept your claim.
  • 10-10: b'File "/tmp/tmp1qi08y3s/Assignment10_10.v", line 26, characters 8-19:\nError: The reference nf_is_value was not found in the current environment.\n'
  • 11-5: regraded.
• @artberryx: your submission for 8-5 is not well compiled:
  • b'File "/tmp/tmpliawa9b8/Assignment08_05_01.v", line 48, characters 45-47:\nError: The reference l0 was not found in the current environment.\n'
  • Did you use Coq 8.4pl5?
• @woong8556: Your commit: https://github.com/woong8556/pl2015/commit/59d1acae301d806b36dbcf8f30ebfafd88d49977 is authored 21th May, but the due and the delay due were 12th and 19th May.
• @jaewooklee93 @dormant09 @SungMinCho:
  I made a mistake in grading 7-1. I updated, and checked that the submissions from all three of you now got the full points. Sorry for inconvenience!
• @fortunist: you changed the signature of test_nostutter_1 in 6-7.
• @wonook: your submission for 6-8 is regraded.
  You changed the signature (X: Type) into {X: Type}. I think that the change is tolerable, so decided to give you the full points.
• @hyunjin95: Gil and I reviewed your case, and we decided to change your source code and re-evaluate. So the new result is: 0(CHECK), which means that your definition is wrong.
• @wonook: Yes, you exam score is max(midterm + final, 2*final).

[jeehoonkang]

Results of Assignments 6-8 are announced.

[jaewooklee93]

What's wrong with my assignment 7-1?

[jeehoonkang]

@jaewooklee93 I will look at it no later than today.

[fortunist]

What does the (CHECK) mean?
Would you review my assignment 6-7?

[seohongpark]

Would you please check my Assignment08_05?

[hyunjinjeong]

8th file of my midterm exam has compile error.
But I didn't use lemma defined in other files. I just didn't write 'Qed' of one problem after proof.
And my file is good in coqIDE.
Is it impossible to get some score about it? I proved two problems in the file.

[woong8556]

Please review my assignment 7 too. They can't be missing.

Also I think I have to visit you regarding my Assignment3,4 to look at what went wrong.

[wonook]

The exam scores are going to be max(midterm + final, 2*final) right? Just to be sure.

[jeehoonkang]

• Results of all assignments are announced.
• Those who claimed on the assignments: sorry I could not review your claims. I will do tomorrow..

[jeehoonkang]

Final exam result is announced.

[dormant09]

Please review my assignment 7-1. I guess there is the same issue with @jaewooklee93.

[SungMinCho]

For problem 1, I even proved that my definition is the weakest precondition as "Theorem test" in the same file. I completed the proof, and i don't understand how the proof could have been completed if my definition was wrong. Please check about that.

[jeehoonkang]

I claim that all claims are either answered or acknowledged in the comment above. If not, please let me know once more.

[jeehoonkang]

All claims are answered.

[rhs0266]

I used lemmas which is proved at 06_07 in 06_08, since I was not adapted new submit format.
Definitely, I passed 06_grader also. I can prove it through my comment in #69 !
Would you consider this problem and adjust it?
And also if you don't mind please check my 10_10 and 11_05?
Thank you.

[amoretspero]

I think I have used ADMIT on few problems, not on every problem except Prob1 in Final exam. I thought that there would be some score for first half of prob2, prob5 and some more. Or did I just left Prob2~Prob8 untouched? Please check about these.

[jeehoonkang]

All claims are answered so far.

[amityaffliction]

there is problem with my Assignment08_05. it runs well on coqide but it says i got 0 points

[rhs0266]

I thought this message meaning that I passed it. What's this meaning?

[seohongpark]

In Assignment08_05, I can't guess why compilation error happens, because I explicitly mentioned the variable l0 in my proof...
Additionally, it seems my proof runs well in my CoqIde 8.4.

[fortunist]

I had changed a example code of Assignment 6-7
from
Example test_nostutter_1: nostutter [3;1;4;1;5;6].
to
Example test_nostutter_1: nostutter [1; 2; 3; 4; 5; 6; 7; 8; 9; 0].
to check my definition of nostutter and I forgot to restore the original one.

My definition of nostutter works well with the original one nostutter [3;1;4;1;5;6].
Could I get score about that?

[jeehoonkang]

@fortunist

• I understand you fully understood the material and solved the problem well.
• But for grading, I cannot make an exception; test_nostutter_1 is a part of the problem.

[jeehoonkang]

@rhs0266

• I am not sure why your environment did not reject your submission.
• But even so, I believe it is better not to make an exception; sorry.

[jeehoonkang]

For 8-5:

@amityaffliction's solution got compile error:

b'File "/tmp/tmpu1yzdlw0/Assignment08_05_00.v", line 26, characters 50-62:\nError:\nFound no subterm matching "s_execute st ?1755 (p1 ++ ?1754)" in the current goal.\n'

@amityaffliction @artberryx I suspect your solutions are not compiled well since your were working on a previous version of s_execute.

[seohongpark]

I'm sorry for your inconvenience, but I don't think so...
To make sure of it, I copied and pasted Assignment08_00.v (recent version : https://github.com/snu-sf/pl2015/blob/master/sf/Assignment08_00.v) and my Assignment08_05.v in Imp.v, but I think my proof still compiles and works well.
This is what I copied from Assignment08_00.v and Assignment08_05.v : http://ideone.com/DyVPfW

[amityaffliction]

Im pretty sure i did on right version of s execute. I wish i could go to 302 but i cant make it today. It works on coqide on right assignment8 00.v file could you please check once more on coqide im sorry.

[jeehoonkang]

@artberryx @amityaffliction I manually inspected your codes in other machines, and realized that your solutions work in that case. I updated your scores.

Sorry for inconvenience.

[jaewooklee93]

I think my Assignment08_05.v has no problem, but score was taken off.
Could you check it again?

[jeehoonkang]

@jaewooklee93 acknowledged & updated.

[fortunist]

Why is my score of assignment 8-5 10 of 20? I think there is no fault.

[jeehoonkang]

@fortunist I updated your score.

[jeehoonkang]

I regraded 6-8.

[jeehoonkang]

Now no more claims will be acknowledged.