search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Claim on Attendance, Assignment & Exam #165

Open jeehoonkang opened 9 years ago

jeehoonkang commented 9 years ago

On Claim

jeehoonkang commented 9 years ago

Results of Assignments 6-8 are announced.

jaewooklee93 commented 9 years ago

What's wrong with my assignment 7-1?

jeehoonkang commented 9 years ago

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

fortunist commented 9 years ago

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

seohongpark commented 9 years ago

Would you please check my Assignment08_05?

hyunjinjeong commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

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

jeehoonkang commented 9 years ago
jeehoonkang commented 9 years ago

Final exam result is announced.

dormant09 commented 9 years ago

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

SungMinCho commented 9 years ago

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 commented 9 years ago

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

jeehoonkang commented 9 years ago

All claims are answered.

rhs0266 commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

All claims are answered so far.

amityaffliction commented 9 years ago

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

rhs0266 commented 9 years ago

image

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

seohongpark commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

@fortunist

jeehoonkang commented 9 years ago

@rhs0266

jeehoonkang commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

@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 commented 9 years ago

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

jeehoonkang commented 9 years ago

@jaewooklee93 acknowledged & updated.

fortunist commented 9 years ago

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

jeehoonkang commented 9 years ago

@fortunist I updated your score.

jeehoonkang commented 9 years ago

I regraded 6-8.

jeehoonkang commented 9 years ago

Now no more claims will be acknowledged.