On Saturday, February 15, 2020 at 2:56:18 PM UTC-5, David A. Wheeler wrote: > > My computer is now busy on jobs 144-151. > > I could pick up one more soon. If no one else takes it up, > > I could work on 155 starting probably tomorrow.
On Sat, 15 Feb 2020 17:57:34 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote: > That would be great! I assigned 155 to you. David S.'s run of 155 didn't > complete (crashed), and I'm attaching his partial log in case you want to > compare his early progress. Very good! I've started job 155 as of 2020-02-15T21:21:58 US East Coast time. Of course, if the crash is due to a problem in metamath.exe code I am unlikely to get different results :-). If the problem was hardware, all should be well. So I'm kind of hoping David S. has a computer hardware problem (sorry! :-) ). It looks like the key is for my job 155 to get significantly beyond this line: > Proof of "fourierdlem111" decreased from 16553 to 16546 bytes using "picn". Just getting a *little* beyond that line tells us nothing; if output was buffered, David S.'s system might have gone much beyond that before crashing. I continue to run jobs 145-151. My (re)run of job144 completed and produced exactly the same technical results; the only differences were dates and exact run times. I didn't expect anything different, but it's good to occasionally check the basics. Based on the previous run I expect job 149 to complete tonight and also produce the same results as last time. Jobs 157-159 are unassigned. If they're still unassigned, I could take one (presumably 157) once 149 completes (presumably tomorrow AM). Can I snag 157 as well? That will leave 158-159 for someone. Volunteers welcome, but be prepared to run 158-159 for a while. --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1j39lv-0000SA-HJ%40rmmprod07.runbox.
