Hi Norm,I accidentally picked job101 and started it. It's (still) running. I'll send you the job101.log file after the job has finished.
By the way, PRs for set.mm should not be placed as long as the minimization is running, should they?
There might be an error in the minimize command; it found that axdc
has a much shorter proof using ax-dc, which is obviously true yet
defeats the purpose of the axdc theorem (
http://us.metamath.org/mpegif/axdc.html ) and uses new axioms for that
theorem.
--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/0b405e55-4212-4d6c-b0ec-ba7ea1ffd5b6%40googlegroups.com.
While we're waiting for the tweaks to metamath.exe to fix the
minimize bug, below is a quick shell script I wrote to do this for Linux/Unix.
If you store this as file "jobs" and make it executable ("chmod a+x jobs"),
you can run in parallel jobs 120 through 128 by running:
jobs 120 128
Note that I don't use the metamath "log" capability, and use the Linux/Unix
built-in redirection mechanisms instead. If that's a problem of some kind,
let me know...!
--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/06ad104d-1d7d-4d6e-9dac-706f5a4f4cc2%40googlegroups.com.
Given about 8 hours a run for me, I'll take two batches of 8; 103-111 and 135 to 143.
You work fast!
Does metamath-program.zip reflect the executable update? I am getting the same
hash as 0.180.
Cheers,
I also tried several URLs, but always get Version 0.180 (and tested it with minimizing axdc - the proof is always replaced by ax-dc, so the exe does not contain the bug fix):
So we have to wait for Norm (or the servers to be updated?)
Unfortunately, there is no exe in Github (https://github.com/metamath/metamath-exe), but it could be reproduced from there...On Thursday, February 13, 2020 at 5:23:30 AM UTC+1, heiph...@wilsonb.com wrote:Hrm. For some reason both us and us2 are giving me the 0.180 hash. Is this the
correct URL?
http://us2.metamath.org/downloads/metamath-program.zip
On Thursday, February 13, 2020 at 12:14:44 AM UTC-5, Alexander van der Vekens wrote:I also tried several URLs, but always get Version 0.180 (and tested it with minimizing axdc - the proof is always replaced by ax-dc, so the exe does not contain the bug fix):So we have to wait for Norm (or the servers to be updated?)
Sorry, I forgot to update metamath.exe. It should be in all of the us2 files above now which I just regenerated.
The source files should have been 0.181 all along, though.
The problem was on my end. The build system I was using ended up lying about
deleting the old zip. Manually removed and I see 0.181 now.
Are 101 and 102 still open now? If so, I will take them. Otherwise, my stake is
on the next two lowest ordinals.
David: yes, ~bisymOLD and ~bi3antOLD should have both discouragement tags. I'm away from my main computer... can you add them ?Actually, most *OLD and *ALT should probably have both discouragement tags as well, it seems ?
On Thursday, February 13, 2020 at 9:25:42 AM UTC-5, Benoit wrote:David: yes, ~bisymOLD and ~bi3antOLD should have both discouragement tags. I'm away from my main computer... can you add them ?Actually, most *OLD and *ALT should probably have both discouragement tags as well, it seems ?
I think so. This can be checked by making sure all *OLD and *ALT labels have both discouragements in the 'discouraged' file. There might be rare exceptions for *ALT although I can't remember - e.g. we don't necessarily want to prevent a shorter proof for a *ALT that occurs before the non-ALT. I should look at each *ALT case with a missing discouragement.
--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAMZ%3Dzj6o-F6AwFMeZcZOYGaKf84VYK4H6uBONcOhyjrhERDXpw%40mail.gmail.com.
I will take the 12 jobs 113-124, anticipating it to take about 2 weeks in total
given my hardware.
I had a couple
unexplained segmentation faults, on job105 and job135. I restarted
job105 and it ran to completion; I haven't tried restarting 135 yet.
I'll restart 135 and actually start 137, and take 133, 134, and
152-155, and send you the complete logs.
Le 14 févr. 2020 à 04:33, Norman Megill <n...@alum.mit.edu> a écrit :
I worked out an estimate (in hours) for jobs 133-160 based on the theory that the time to save a compressed proof is proportional to the run time of 'minimize'.
est. actual hours
job159.cmd: footex 268.8
job160.cmd: mideulem 404.4
Norm
If ~ footex and ~ mideulem are too long, I may split them into smaller lemmas, and then run minimize on the smaller lemmas.
Alternatively, since geometry is a rather closed domain, we know only the theorems from predicate logic and elementary geometry (and basic set theory) are needed to be considered. Is there a way to do that?
--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1j2crr-0001Mg-Tj%40rmmprod07.runbox.
123 and 124 completed, in about 12 and 13 hours respectively. I'm running 156 and 160 now.
We have a more serious problem though. ~dral1ALT is not in job129.cmd, it is in job124.cmd. When I checked, ~dral1ALT was in the old job129.cmd before the bug fix. In my post https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ I wrote that the min2020-jobs.zip file was updated, but it looks like your script kept the old version:
On Fri, Feb 14, 2020 at 3:12 PM Norman Megill wrote:
> A simple way to fix this is to add "(Proof modification is discouraged.)" to dral1ALT, etc. as they should have anyway. Then the final 'minimize' run will skip them. There are also a number of "suspicious" minimizations on non-ALT/OLD theorems as can be seen with "grep 'to [12]. bytes' job*.log" e.g.:
>
> job102.log:Proof of "bj-abf" decreased from 45 to 12 bytes using "abf".
> job103.log:Proof of "hashssle" decreased from 370 to 19 bytes using "hashss".
>
> When everything is done, we will need to analyze these and decide what to do.
That seems correct for hashssle; it takes a hypothesis in hashss 𝐴 ∈
𝑉 and turns it into 𝐴 ∈ Fin.
> Unfortunately these jobs will have to be rerun. The theorems in job133.cmd through job160.cmd were not changed so those runs shou OK.
Does that mean that 125-132 are open again? Since 155 hasn't started
running backwards yet, I might as well load up the rest of those
cores.
Job 113 results attached. Runtime is about 18.2 hours.
Should I keep sending job results piecemeal like this, or would it make it
easier to just wait until my current batch is done and send them all at once?
On Friday, February 14, 2020 at 6:28:58 PM UTC-5, David Starner wrote:On Fri, Feb 14, 2020 at 3:12 PM Norman Megill wrote:
Does that mean that 125-132 are open again? Since 155 hasn't started
running backwards yet, I might as well load up the rest of those
cores.Let's see what David W. wants to do. Also, this might affect anyone who used the script, so there might be other jobs to be redone.
--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1j2nAt-0005ZC-6n%40rmmprod07.runbox.
It may minimize with the statement, then later minimize the statement away. I wouldn't be worried unless "idi" appears in the minimized proof.
On Fri, Feb 14, 2020 at 6:27 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:
I just took a quick look at job144.log as posted on:
https://dwheeler.com/temp/job144.log
I noticed these... oddities:
Proof of "fourierdlem48" decreased from 18892 to 18864 bytes using "dummylink".
Proof of "fourierdlem48" decreased from 18864 to 18848 bytes using "idi".
I didn't expect that. This is using Metamath Version 0.181 12-Feb-2020.
Is this expected behavior (and if so, why)?
--- 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 meta...@googlegroups.com.
On Fri, Feb 14, 2020 at 3:12 PM Norman Megill <n...@alum.mit.edu> wrote:
> A simple way to fix this is to add "(Proof modification is discouraged.)" to dral1ALT, etc. as they should have anyway. Then the final 'minimize' run will skip them. There are also a number of "suspicious" minimizations on non-ALT/OLD theorems as can be seen with "grep 'to [12]. bytes' job*.log" e.g.:
>
> job102.log:Proof of "bj-abf" decreased from 45 to 12 bytes using "abf".
> job103.log:Proof of "hashssle" decreased from 370 to 19 bytes using "hashss".
>
> When everything is done, we will need to analyze these and decide what to do.
That seems correct for hashssle; it takes a hypothesis in hashss 𝐴 ∈
𝑉 and turns it into 𝐴 ∈ Fin.
Yes, ~hashssle is a specialization of ~hashss and could be replaced (and removed afterwards). ~hashssle (and ~bj-abf), however, are in mathboxes. In my opinion, the owners of the mathboxes should be responsible for cleaning up such cases. But it would be great if a list of such cases was created and provided after the global minimize action (to be used by the mathbox owners).
An update: Now I've also finished job 132, available here:
https://dwheeler.com/temp/job132.log
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.
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?
--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/88673fc3-7d62-4ecb-8140-4e413c381476%40googlegroups.com.
156 is done (after 31.8 hours), starting 158. 160 is still running.
--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e6426693-a3be-4f07-92f7-7cc30979e49c%40googlegroups.com.
158 is done (after 62.8 hours), starting 159. 160 is still running.