search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Is long compile time ok? #83

Closed jaewooklee93 closed 9 years ago

jaewooklee93 commented 9 years ago

When I solved Assignment07_02.v, I used several number of try omega, but it seems that omega takes relatively longer time than others tactics. So now compilation takes almost 10 seconds at my machine. I guess that this phenomenon will continue to appear as the complexity of proof increases. Thus, I want to clarify whether such long compile time is available or not, at this point.

jeehoonkang commented 9 years ago

10 seconds would be fine. 10 minutes will be a problem.

Jeehoon

jaewooklee93 commented 9 years ago

Thank you. It's quite weird that even Qed took several seconds.

jeehoonkang commented 9 years ago

@jaewooklee93 That's because Qed re-checks the proof term. For some times, Qed alone takes more time than the proof between Proof and Qed.

Jeehoon