My latest minimize status

46 views
Skip to first unread message

David A. Wheeler

unread,
Feb 16, 2020, 9:54:09 AM2/16/20
to metamath
I looked at my status this AM; these jobs are done:
112, 125, 126, 127, 128, 129, 130, 131, 132, 144, 146, 149

Jobs 146 & 149 are newly done as of this AM, and are available as:
https://dwheeler.com/temp/job{146,149}.log

I found these jobs running (6 jobs, I can run 8 at a time):
145, 147, 148, 150, 151, 155.

It's not yet known if my run of job 155 will have the same problems as David S.
My run of job 155 has only gotten up to this line:
> Proof of "fourierdlem111" decreased from 17615 to 17592 bytes using "mp3an12".
David S.'s job had problems sometime after this line:
> Proof of "fourierdlem111" decreased from 16553 to 16546 bytes using "picn".
I guess we'll see.

Mario is running 160 and started 158.

I started job 157, as assigned.

That left one more of my 8 CPUs not doing anything.
So I decided to also start doing job 159, since no one else had
said they were doing it (as far as I know). I hope that's okay.
With that, every job is assigned.
If my job 159 is thrown away because it's being split up,
or someone else ends up doing it, no big deal.
But if we might want to use job 159, someone
has to start it :-).

--- David A. Wheeler

David A. Wheeler

unread,
Feb 16, 2020, 10:32:56 AM2/16/20
to metamath
(Replying to myself)

My job 145 just finished. It's posted as:
https://dwheeler.com/temp/job145.log

I have a spare CPU available if it might be useful for another job.

--- David A. Wheeler

Norman Megill

unread,
Feb 16, 2020, 11:19:26 AM2/16/20
to Metamath
On Sunday, February 16, 2020 at 10:32:56 AM UTC-5, David A. Wheeler wrote:
(Replying to myself)

My job 145 just finished. It's posted as:
 https://dwheeler.com/temp/job145.log

I have a spare CPU available if it might be useful for another job.

heiphohmia's job115 died in the middle of minimizing the last proof.  I finished the last proof myself, so the job is complete, but I'm concerned about all the mysterious crashing problems. As a test, could you run 115 on your end to see if it completes OK?

Norm

David A. Wheeler

unread,
Feb 16, 2020, 12:27:36 PM2/16/20
to metamath, Metamath
On Sun, 16 Feb 2020 08:19:26 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> heiphohmia's job115 died in the middle of minimizing the last proof. I
> finished the last proof myself, so the job is complete, but I'm concerned
> about all the mysterious crashing problems. As a test, could you run 115 on
> your end to see if it completes OK?

Will do.

I'm currently running these jobs:
115
147
148
150
151
155
157
159

No telling when they'll be done :-).

It's hard to know why a job would crash on one system & not another.
Overclocked systems are especially prone to this.
Windows is more crash-y (especially depending on the device drivers).
Otherwise the hardware seems likely; hardware *should* just run
forever, but this-busy this-long causes a lot more thermal stress than
most computers normally undergo, and if a component is marginal
it might temporarily fail. That's true for RAM, CPU, etc.

--- David A. Wheeler

fl

unread,
Feb 16, 2020, 12:34:42 PM2/16/20
to Metamath
but this-busy this-long causes a lot more thermal stress than
most computers normally undergo


In my experience, the thermal stress is mostly due to using all your available cores.
Reduce the number of working cores. Your cooling device will appreciate.

-- 
FL
Reply all
Reply to author
Forward
0 new messages