Full 'minimize' run on set.mm

[Norman Megill]

We are ready to do a full 'minimize' run on set.mm.  So you can fire up your high-end gaming rigs for some serious work and help make the world a better place through shorter proofs.  :)

With the help of Saveliy's script mentioned at https://groups.google.com/d/msg/metamath/djIdTu2Wq-I/mgs4MD7YDAAJ, I partitioned the minimize run for all of set.mm into 60 scripts called job101.cmd through job160.cmd.  They are contained in the file http://us2.metamath.org/downloads/min2020-jobs.zip

If you want to help out, let me know which scripts you want to commit to.  Until we have a better way of doing this, maybe it's easiest to handle it informally and respond here with the job(s) you plan to work on so others won't repeat the effort.  (GitHub might not be the best way to track this since not everyone has an account there.)  If you don't want to post here, email me privately and I'll update the public list.

The purpose of these runs is to discover what minimizations will happen; you won't be changing set.mm directly.  When finished, you would send me (say by email for now) the job*.log file for each job you ran.  I will use the log files to create the final 'minimize' run and also to collect run time statistics to help improve future estimates.


Instructions
------------

You should use yesterday's set.mm which is at https://github.com/metamath/set.mm/commit/59bd588e52523db5238db18241e518941112ea34 (click "..." in the set.mm row, then select "View file", then select "Download").

Assuming the 60 job*.cmd files (from the zip file above), set.mm, and metamath[.exe] are in the same directory, you would type:

Unix/Linux/Cygwin terminal 1:
./metamath 'read set.mm' 'open log job101.log' 'submit job101.cmd/silent' exit
Unix/Linux/Cygwin terminal 2:
./metamath 'read set.mm' 'open log job102.log' 'submit job102.cmd/silent' exit
...
(etc. until for example cores or hyperthreads are filled up.)

In a Windows Command Prompt you would type:
metamath "read set.mm" "open log job101.log" "submit job101.cmd/silent" exit

On Linux, you can use 'tail -f job101.log' on a different terminal to monitor the progress.  In the Windows Command Prompt, you can omit "/silent" to monitor progress on the screen.


job101.cmd through job132.cmd
-----------------------------

job101.cmd through job132.cmd each minimize around 1000 theorems and should each take roughly the same amount of time (maybe around a day).  Within a given .cmd file, the theorems are sorted starting from shortest estimated run times, and the last theorem in each .cmd file is expected to have the longest run time.

If a job, say job101.cmd, seems to be taking too long and you run out of patience, you can abort the job and send me the partial job101.log, which I can still use.  I will then create job101b.cmd for the proofs that are left, and someone else can continue with it.


job133.cmd through job160.cmd
-----------------------------

job133.cmd through job160.cmd each minimizes a single big proof. job133.cmd is expected to take roughly the same time as the entire job132.cmd run.  As the job numbers go up, the proofs get larger and larger, and the expected run times will increase, until job160.cmd which might take orders of magnitude longer, who knows.  To help avoid frustration, you should start with the lower job numbers first.

The biggest proofs may be infeasible unless we break up the 'minimize' run into small ranges of statements and/or break up the proof into smaller lemmas.  We'll have to see how it goes with experience.

Norm

[Alexander van der Vekens]

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?

Alexander

[Norman Megill]

On Tuesday, February 11, 2020 at 4:20:57 PM UTC-5, Alexander van der Vekens wrote:

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.

Thanks.

That makes our status:  job101 assigned to AV, job102-job160 unassigned.
 

By the way, PRs for set.mm should not be placed as long as the minimization is running, should they?

They should be OK as long as they don't have (many) renames, which is why I waited until David's "rng" renaming.   Worst case, all that will happen is that a few minimizations might not get applied and will get processed in next year's full run.  The final scripts I will use should be robust enough so they will just skip a theorem not found and other errors, and in any case I will be reviewing the log for the final run.  So don't worry about it too much.

Norm

[heiph...@wilsonb.com]

I only have a 10 year old laptop, so for now I picked up job102 and will
contribute more if it seems reasonable.

Happy minimizing!

[David Starner]

I've got a decent desktop sitting around because it's crashing when
the GUI is running; I'll try 103 through 111 (an 8-core system).

> --
> 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/3ONE57KGXFOW3.33VH46N97A16O%40wilsonb.com.



--
Kie ekzistas vivo, ekzistas espero.

[David Starner]

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.

[Alexander van der Vekens]

On Wednesday, February 12, 2020 at 10:00:42 AM UTC+1, David Starner wrote:

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.

I think ~axdc must be tagged with "(Proof modification is discouraged.)", so that minimize will not touch its proof. This is not an error of the minimize command. 

[Norman Megill]

David is right, there is something very wrong here.  While ~axdc should be tagged with "(Proof modification is discouraged.)" but isn't, in any case 'minimize' should not be bringing in the new axiom ~ax-dc.

We should hold off on any more runs until I determine what is happening and fix the program.  Based on what I find, the jobs may have to be restarted.

Thanks, David, this was a good observation.

Norm

[Norman Megill]

This bug first appeared in version 0.179.  I am still working on it; all I know so far is that somewhere it is incorrectly marking ax-dc as already used by the acdc proof.

Anyway, we will have to discard the jobs already started.  If any of them finished, it would still be useful to post how long they ran, to give us an idea of the run times we can expect for the others.  Alexander told me job101 took about 20 hr.  BTW the first theorem in each job file always ~3atlem4, which I will use to calibrate run times for CPU differences; in his case 3atlem4 took 31 sec.

I apologize for the work wasted and am very grateful to David Starner for finding this before we got too deep into the job runs.

Norm

[David Starner]

All my jobs but 103 completed overnight.

--

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.

[David A. Wheeler]

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

My suggested setup is slightly different, see the comments below.

I share this in the hopes it'll be useful. I have access to an 8 CPU 128GB
machine that should help in this little quest.

I'll probably eventually propose a variant like this for the "scripts/" directory.
If people have comments, let me know.

--- David A. Wheeler


============== File "jobs" ========================
#!/bin/sh

# Run set of Metamath minimization jobs from $1 (start) through $2 (end).

# Recommended setup:
# git clone https://github.com/metamath/set.mm.git
# cd set.mm
# scripts/download-metamath
# scripts/build-metamath
# git checkout 59bd588e52523db5238db18241e518941112ea34
# git checkout -b jobs

set -e -u
die () {
printf '%s\n' >&2
exit 1
}

command -v metamath || die 'Metamath program not on path'
[ "$#" = 2 ] || die 'Requires exactly 2 parameters, the start and end job #s'
first="$1"
last="$2"

# Download jobs if not already downloaded
test -f min2020-jobs.zip || \
wget http://us2.metamath.org/downloads/min2020-jobs.zip

# unzip if not already unzipped
test -d metamathjobs || unzip min2020-jobs.zip

for num in `seq $first $last`; do
logfile="metamathjobs/job${num}.log"
echo "Starting job $num. View with: tail -c +0 -f ${logfile}"
# Instead of using Metamath 'open log', use redirection to capture everything
nohup time metamath 'read set.mm' "submit 'metamathjobs/job${num}.cmd'" \
quit > "$logfile" 2>&1 &
done

echo
echo 'Run "killall metamath" to kill all processes.'
echo

[David Starner]

On Wed, Feb 12, 2020 at 2:10 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:
>
> 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.

Thanks for the script. I fat-fingered one of my commands last night,
so it would certainly come in handy.

> I share this in the hopes it'll be useful. I have access to an 8 CPU 128GB
> machine that should help in this little quest.

Is anybody hitting memory limits on this thing? A quick and dirty test
shows it taking 250 MB; unless there's memory leaks or large swings,
most 8-core machines should have plenty of memory. Even if those are
multiple core CPUs, that's still huge levels of headroom.

In retrospect, I accidentally ran job 103 twice in a row, so all of
them, 103-111, took about 8 hours on my system.

[David A. Wheeler]

I'm not hitting memory limits so far, I expect this to be CPU limited not memory limited.

I may create a new version of this script using GNU make. GNU make has built-in mechanisms to maximally run as many jobs as reasonable, and starts next jobs as each one completes. If you're only running as many jobs as there are CPUs that won't matter, but if you plan to process more jobs than that, that approach might improve the throughput of the jobs.
--- David A.Wheeler

[Norman Megill]

On Wednesday, February 12, 2020 at 5:10:34 PM UTC-5, David A. Wheeler wrote:

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

I'm not sure how often it will happen, but I anticipate that the jobs may not always be in order.  In particular, jobs 133-160 are almost certainly going to take very large and unpredictable amounts of time, and with some users giving up on some of them, there are bound to be gaps.  Even 101-132 might run into unexpectedly long runtimes where a user gives up in the middle, and someone else will need to run say job130b.cmd to finish the rest of it.

Aside from that, thanks for putting this together!

Norm

[Norman Megill]

The bug is fixed, and I updated the metamath program to version 0.181.  It has been updated on us2 http://us2.metamath.org/index.html#mmprog and github.  I will post about restarting the job runs in a separate post.  We might as well start from the most recent set.mm, and I will re-create the job files for it (after I have some dinner).

Per request of Giovanni (see https://groups.google.com/d/msg/metamath/uSa8Q0fWKeM/9dDcUM-DCwAJ ) I also did the following.  I assume this is still desired?

       git commit -m'Release version 0.181.'
       git tag v0.181
       git push
       git push --tags



Here is a description of the bug and its impact.

In November (version 0.179 29-Nov-2019) I changed 'minimize' to use the MM-PA proof in progress instead of the saved proof.  This was done to avoid the need to 'save new_proof' before running 'minimize'.

To speed up 'minimize', the (relatively slow) trace_back algorithm is called only when it is needed to test whether a proposed minimization match uses a new axiom.  The results of this trace_back call are saved so that it will be done at most once during a 'minimize' run.

As a result of the November mod, when the trace_back algorithm is called, it is now handed the proof in progress instead of the saved proof.  The mistake was that I overlooked that the proof in progress was modified by the proposed minimization at that point, and instead I should have handed trace_back an earlier saved version of the proof in progress.

Therefore, any 'minimize' runs done between 29-Nov-2019 and now are suspect.  For most proofs it shouldn't matter, but for ones such as axdc that study axiomatizations, it was a serious bug.  If you ran 'minimize' on one of these, you probably want to check that the axioms being used are the ones you wanted.  Note the following:

When the bug was present, a theorem using a new axiom would be brought into the proof if and only if it was the *first* statement matched by 'minimize'.  The second and later matches, if any, would not bring in new axioms.  So if, for example, 'minimize' on axdc first matched syl5eq, it would then later correctly reject ax-dc.

In other words, sometimes a new axiom would be accepted and other times it wouldn't, depending on the order in which the match occurred.

Norm

[heiph...@wilsonb.com]

Woke up this morning to a finished job102. Here is the data relevant to
runtime:

$ lscpu | grep '^Model name'
Model name: AMD Phenom(tm) II N830 Triple-Core Processor
$ grep '^MemTotal' /proc/meminfo
MemTotal: 3774096 kB
$ head -1 job102.log
The log file "job102.log" was opened 12-Feb-2020 8:46 AM.
$ echo ${tstart:=$(date +%s --date='12-Feb-2020 8:46 AM')}
1581464760
$ echo ${tend:=$(stat -c %Y job102.log)}
1581519472
$ dc -e "3k $tend $tstart - 3600/ p"
15.197

So it took a tad over 15 hours to run as a single job on old laptop. Also, in
case it happens to be useful, I am attaching job102.log.zip.

Hope it turns to to be an easy fix!

[Norman Megill]

The job files have been updated for today's set.mm.  The new job files are available at http://us2.metamath.org/downloads/min2020-jobs.zip

The instructions at the beginning of this thread (https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/1lURYnVcFwAJ) still apply, except that you should use today's set.mm at https://github.com/metamath/set.mm/commit/87bc05d4155014c9bc7b8f4f05435347b628b7f0

Make sure you are running metamath version 0.181.

As I mentioned, all previous runs should be discarded.  We are starting from scratch.

Thank you!
Norm

[David A. Wheeler]

On Wed, 12 Feb 2020 17:57:39 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> The job files have been updated for today's set.mm. The new job files are
> available at http://us2.metamath.org/downloads/min2020-jobs.zip

Thanks!

I've quickly cobbled together an updated script & corresponding makefile
(scripts/jobs and scripts/jobs.makefile) for Linux/Unix below.
You can stick them in their respective places and run "chmod a+x scripts/jobs".

Then if you want to process jobs 120 through 130 (inclusive), run:
scripts/jobs 120 130

It'll run simultaneous processes (by default the number of CPU processors,
set the environment variable NPROC if you want something different).
Once a task is done, it'll run the next one, until all is done.

You can run a single job easily enough:
scripts/jobs 120 120

This is fresh out of my fingers, and not well tested yet. Feedback welcome.
My plan is to eventually put this in the shared scripts directory
so it'll be easier to do next time.

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...!

--- David A. Wheeler


===== scripts/jobs ================

#!/bin/sh

# Run set of Metamath minimization jobs from $1 (start) through $2 (end).

# The number of jobs is the environment variable NPROC if set, else # CPUs

# Recommended setup:
# git clone https://github.com/metamath/set.mm.git
# cd set.mm
# scripts/download-metamath
# scripts/build-metamath

# # check out the version we want to analyze
# git checkout 87bc05d4155014c9bc7b8f4f05435347b628b7f0 # or whatever

# git checkout -b jobs

set -e -u
die () {

printf '%s\n' "$1" >&2
exit 1
}

command -v metamath > /dev/null || die 'Metamath program not on path'

[ "$#" = 2 ] || die 'Requires exactly 2 parameters, the start and end job #s'
first="$1"
last="$2"

# Download jobs if not already downloaded
test -f min2020-jobs.zip || \
wget http://us2.metamath.org/downloads/min2020-jobs.zip

# unzip if not already unzipped
test -d metamathjobs || unzip min2020-jobs.zip

master_log='metamathjobs/master.log'

echo
echo 'Starting jobs. View job NUM with: tail -c +0 -f metamathjobs/jobNUM.log'
echo "View overall state with: tail -c +0 ${master_log}"
echo

# We use "nproc" to find the number of CPUs if NPROC is not set.

nohup make --jobs "${NPROC:-$(nproc)}" -r -f scripts/jobs.makefile \
first="$first" last="$last" > "$master_log" 2>&1 &

echo
echo 'Run "killall make metamath" to kill all processes.'
echo



===== scripts/jobs.makefile =============
# Makefile to minimize Metamath proofs. Requires GNU make.

all: alljobs
echo 'DONE.'

LOG_LIST := \
$(foreach num, $(shell seq $(first) $(last)), metamathjobs/job$(num).log)

$(info LOG_LIST is $(LOG_LIST))

metamathjobs/job%.log: metamathjobs/job%.cmd
echo "Running job $*"
metamath 'read set.mm' "submit 'metamathjobs/job$(*).cmd'" quit \
> "metamathjobs/job$(*).log" 2>&1

alljobs: $(LOG_LIST)

# Delete what's generated if a program returns a nonzero (error) result.
# This can be annoying for debugging, but it means that we can simply re-run
# make if a process is stopped.
ifndef KEEP_ON_ERROR
.DELETE_ON_ERROR:
endif

[Norman Megill]

Interesting.  BTW the run time for 3atlem4 in your log was 67 sec, compared to 31 sec in Alexander's log.  So your 15 hours would likely correspond to about 7 hours on Alexander's computer.  (I chose 3atlem4 arbitrarily as a reference was because it was the first one I saw that was neither too fast nor too slow and also had no minimizations.)

Norm

[Norman Megill]

On Wednesday, February 12, 2020 at 9:14:32 PM UTC-5, David A. Wheeler wrote:

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...!

The beginning and end will be a little different.  An advantage of the log is that it shows the start and end times.  My scripts to build the final minimize run have been tested on the log format, although I don't expect any problems.  Is there a reason not to use the log, though, in order to keep things consistent?  People running on Windows will be using the log format.

In the line commented "Download jobs if not already downloaded", note that min2020-jobs.zip was updated with the same name, so make sure that the old one is deleted.

Norm
 

[David Starner]

Given about 8 hours a run for me, I'll take two batches of 8; 103-111 and 135 to 143.

--

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.

[heiph...@wilsonb.com]

You work fast!
Does metamath-program.zip reflect the executable update? I am getting the same
hash as 0.180.

Cheers,

> <http://www.google.com/url?q=http%3A%2F%2Fus2.metamath.org%2Fdownloads%2Fmin2020-jobs.zip&sa=D&sntz=1&usg=AFQjCNEjjy5wsEd2bpGzg30AHa2IqJ4KEg>

[Norman Megill]

On Wednesday, February 12, 2020 at 10:05:48 PM UTC-5, David Starner wrote:

Given about 8 hours a run for me, I'll take two batches of 8; 103-111 and 135 to 143.

That would be great.

Just be aware that some or many of 133 and above (with 1 theorem each) are expected to take much more than 8 hrs, possibly weeks.  We just don't know, although roughly the run times are expected to increase as the job number goes up.  Basically you are exploring new territory above 132.

For jobs that are taking, say, more than a week (or however long your patience lasts), you may want to abort them, and we can investigate alternate approaches (ranging from running 'minimize' on small statement ranges to breaking up the proof into lemmas - I would prefer breaking up the proof to benefit future runs but that's hard work).  If a job is aborted, we can still apply any minimizations it did find.

Norm

[Norman Megill]

It was only updated on us2, the us server normally gets updated a day or so later.  However, I just put the new one on the us server by hand, so try it again.

Norm

On Wednesday, February 12, 2020 at 10:37:39 PM UTC-5, heiphohmia wrote:

You work fast!
Does metamath-program.zip reflect the executable update? I am getting the same
hash as 0.180.

Cheers,

[heiph...@wilsonb.com]

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

[Alexander van der Vekens]

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):

http://us.metamath.org/metamath/metamath.exe
http://us.metamath.org/downloads/metamath.zip

http://us2.metamath.org/metamath/metamath.exe
http://us2.metamath.org/downloads/metamath.zip
http://us2.metamath.org/downloads/metamath.tar.gz

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...

[Norman Megill]

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):

http://us.metamath.org/metamath/metamath.exe
http://us.metamath.org/downloads/metamath.zip

http://us2.metamath.org/metamath/metamath.exe
http://us2.metamath.org/downloads/metamath.zip
http://us2.metamath.org/downloads/metamath.tar.gz

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.

On the us server, except for metamath-program.zip (which I transferred by hand), the files won't be updated for a day or so.
 

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

This puzzles me.  I just downloaded and unzipped this, and line 31 of the file "metamath.c" says "0.181 12-Feb-2020".  What does yours say?
 
Norm

[Alexander van der Vekens]

On Thursday, February 13, 2020 at 6:33:20 AM UTC+1, Norman Megill wrote:

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):

http://us.metamath.org/metamath/metamath.exe
http://us.metamath.org/downloads/metamath.zip

http://us2.metamath.org/metamath/metamath.exe
http://us2.metamath.org/downloads/metamath.zip
http://us2.metamath.org/downloads/metamath.tar.gz

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.

OK, at least via http://us2.metamath.org/downloads/metamath.zip I've got version 0.181 now...

Alexander

[heiph...@wilsonb.com]

Thank you, Norm. I am now seeing the 0.181 in metamath-program.zip.

[heiph...@wilsonb.com]

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.

[Alexander van der Vekens]

On Thursday, February 13, 2020 at 7:22:58 AM UTC+1, heiph...@wilsonb.com wrote:

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.

 

I plan to run job101 again today, so you should start with 102, please.

[David A. Wheeler]

On February 12, 2020 9:42:15 PM EST, Norman Megill <n...@alum.mit.edu> wrote:
>On Wednesday, February 12, 2020 at 9:14:32 PM UTC-5, David A. Wheeler
>wrote:
>>
>> 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...!
>>
>
>The beginning and end will be a little different. An advantage of the
>log
>is that it shows the start and end times. My scripts to build the
>final
>minimize run have been tested on the log format, although I don't
>expect
>any problems. Is there a reason not to use the log, though, in order
>to
>keep things consistent?

Avoiding the use of log made sense in the first version, before I used make. The idea was to capture everything. But now that I'm using make, I could certainly switch to using log.


--- David A.Wheeler

[heiph...@wilsonb.com]

Thanks. I was unsure whether stakes on runs from the previous false start also
applied here. Either way, I am running 102 now. Will take another tomorrow once
this completes.

[David Starner]

"bisymOLD" says "Obsolete theorem as of 27-May-2019." Unfortunately,
it's not marked as discouraged, and bj-bisym is now changing to be a
copy of it. Not a stop-the-world issue--a bug in set.mm, not
metamath--but bj-bisym should probably manually not be changed and
bisymOLD be marked as discouraged, unless other things start to depend
on bisymOLD.

[Giovanni Mascellani]

Hi,

Il 13/02/20 01:13, Norman Megill ha scritto:

> Per request of Giovanni (see
> https://groups.google.com/d/msg/metamath/uSa8Q0fWKeM/9dDcUM-DCwAJ ) I
> also did the following.  I assume this is still desired?
>
>        git commit -m'Release version 0.181.'
>        git tag v0.181
>        git push
>        git push --tags

Thank you, that seems to be correct. For the record, this means that
release v0.181 is visible on the dedicated GitHub page[1].

[1] https://github.com/metamath/metamath-exe/releases

As soon as I have some time I will update the Debian package and also
contribute some processing power to the minimization effort.

Thanks, Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[Norman Megill]

Here are the current commitments:

101 Alexander
102 heiphohmia
103-111 David Starner
125-132 David A. Wheeler
135-143 David Starner
144-151 David A. Wheeler

Norm

[Benoit]

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 ?

Thanks,

Benoît

[Norman Megill]

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.

I don't think it's worth restarting the jobs at this point, nor use an updated set.mm for new jobs, because I'd prefer everything be based on a stable set.mm.  There shouldn't be many cases, and I can address them individually for the final minimize run.  In the meantime, we can update set.mm independently - that will automatically "fix" some of them for the final run, since 'prove' will not allow discouraged theorems by default, and my final script will tolerate that rejection.  The ones that have to be addressed manually are those where a *OLD/ALT was used to minimize a proof.

Norm

[Alexander van der Vekens]

On Thursday, February 13, 2020 at 5:06:27 PM UTC+1, Norman Megill wrote:

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.

I think the *OLD theorems are no problem, they will be removed anyway sooner or later. But with the *ALT theorems we should be careful. E.g. ~nnindALT and ~nn0indALT have neither of the discouragement tags. Or ~ccat2s1fvwALT with "New usage is discouraged." only, which has a shorter proof than ~ccat2s1fvw (but occurs before the ALT-version!), but is requiring an additional definition. It would not harm (and would even be desirable) if the proof could be shortened further.

 I would propose that a list of all *ALT theorems not having both discouragement tags is created and provided for review (preferably in a separate thread).

 

[Norman Megill]

Here is an update of current commitments as of Feb. 13, 17:30 EST :

101 Alexander
102 heiphohmia
103-111 David Starner

112 David A. Wheeler
113-124 UNASSIGNED
125-132 David A. Wheeler
133-134 UNASSIGNED

135-143 David Starner
144-151 David A. Wheeler

152-160 UNASSIGNED

Thierry has volunteered starting next week.

David S., you mentioned "batches of 8" but your ranges have 9 each.  Do you want to adjust them or keep them as is?

Norm

[David A. Wheeler]

I've just posted an updated "jobs" system if you want to do
big-scale minimization, especially if you're using a number of cores.

This version supports disjoint sets of jobs, e.g., you can now say:
scripts/jobs 112 125-132 144-151
That means the API has changed, but I think it's for the better.
Also, the log files it produces should be exactly what Norm expects
(if it's not, please let me know so I can fix it).

It's merged into the "develop" branch. A minor complication is that
Norm wants the actual work to be done on an earlier commit
(87bc05d41550). It's not complicated, git makes that easy,
but only if you know how :-). Below is an example of how to do that with git.

Let me know of any problems. It *seems* to work ;-).

--- David A. Wheeler

=========================================
# Set up
git clone https://github.com/metamath/set.mm.git # if you don't have it
cd set.mm
git pull # Make sure you have the current version!
# Ensure metamath is up-to-date
scripts/download-metamath
scripts/build-metamath

# check out the version we want to analyze

git checkout 87bc05d4155014c9bc7b8f4f05435347b628b7f0 # go back in time
git checkout -b my_minimization # create a branch name for where you'll work

# Extract the *current* version of the jobs scripts from develop branch
git checkout develop -- scripts/jobs scripts/jobs.makefile

# We're ready! Now plug in your JOB_NUMBERS, e.g.:
# scripts/jobs 112 125-132 144-151
scripts/jobs JOB_NUMBERS

# Wait a while. You can follow progress by running:
tail -c +0 -f metamathjobs/master.log
# You can stop tailing at any time with control-C; that won't stop work.

# You'll eventually have a bunch of files named metamathjobs/jobNUMBER.log
# You send those in.

# When you're all done:
git checkout develop

===========================================

> --
> 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/67a1e124-4dc2-443d-89f2-d71e34793052%40googlegroups.com.

[heiph...@wilsonb.com]

For what it's worth, there's a bit of git-fu that lets you grab a file from a
commit without having to do a checkout:

$ git -C /path/to/metamath/repo show 87bc05d4:set.mm >/where/to/save/set.mm

See git-show(1) for details, but that's the essence. This makes it easy to do
the jobs in a temporary directory, without interfering with repo usage at all,
so you can essentially keep working as normally if need be.

[heiph...@wilsonb.com]

Job 102 just finished. Attached is the log. Runtime looks to be 16.5 hours:

$ echo ${tstart:=$(sed -n '1s/.*opened \(.*\)\./\1/p' job102.log | xargs -I{} date +%s -d '{}')}
1581577740
$ echo ${tend:=$(sed -n '$s/.*closed \(.*\)\./\1/p' job102.log | xargs -I{} date +%s -d '{}')}
1581637740

$ dc -e "3k $tend $tstart -3600/p"

16.666

I will take the 12 jobs 113-124, anticipating it to take about 2 weeks in total
given my hardware.

[David Starner]

I noticed that afterwards, but that wasn't a problem. 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.

[Mario Carneiro]

I'm trying out 123 and 124 for now using AWS. I might be able to scale up depending on the results.

--
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.

[heiph...@wilsonb.com]

Okay, I will hold off on 123 and 124.

[Norman Megill]

On Thursday, February 13, 2020 at 7:27:44 PM UTC-5, heiphohmia wrote:

I will take the 12 jobs 113-124, anticipating it to take about 2 weeks in total
given my hardware.

Well, the way things are going we may be able to complete this before 2 weeks.  If you are running 1 job at a time @ 16.6 hrs, it might be better to commit to 4 jobs or ~66 hrs at a time.  So I'm committing you to 113-116 for now, is that ok?  If you have already started a job outside of that range let me know. (Also, Mario is running 123 and 124.)

Here is an update of current status, under that assumption:

101 Alexander (in progress)
*102 heiphohmia (complete)
*103-111 David Starner (complete)
112 David A. Wheeler  (in progress)
113-116 heiphohmia (in progress)
117-122 UNASSIGNED
123-124 Mario (in progress)
125-132 David A. Wheeler (in progress)
133-135 David Starner (in progress)
*136 David Starner (complete)
137 David Starner (in progress)
*138-143 David Starner (complete)
144-151 David A. Wheeler  (in progress)
152-155 David Starner (in progress)
156-160 UNASSIGNED

As a reminder, here are the current instructions: https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/aI3Xc8w2BAAJ that point to the set.mm version we should use (and see David A. Wheeler's post https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/CJSwJ7p8BAAJ if you want to use his script).

Norm

[heiph...@wilsonb.com]

Wow. People are rushing to donate computer time. Love this community.
Sure, I am running 113 now, will commit to 113-116 for now.

[Norman Megill]

On Thursday, February 13, 2020 at 7:51:53 PM UTC-5, David Starner wrote:

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.

The non-reproducible segfaults are pretty disturbing.  If anyone else sees a segfault, let me know.  I hope we can pin it down.

Norm

[David A. Wheeler]

David S.: what kind of computer are you using? Some laptop temperature sensors do not work properly, and in general laptops are not designed to sustain computation at maximum for a long time. It is possible that the segfaults are Hardware problems, not software problems.

You might want to simultaneously record the CPU temperature. If the problem is Hardware, temperature and or overclocking are two of the most likely culprits.

Of course, if the problem is software, that won't help.
--- David A.Wheeler

[David Starner]

On Thu, Feb 13, 2020 at 6:47 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:
> David S.: what kind of computer are you using? Some laptop temperature sensors do not work properly, and in general laptops are not designed to sustain computation at maximum for a long time. It is possible that the segfaults are Hardware problems, not software problems.
>
> You might want to simultaneously record the CPU temperature. If the problem is Hardware, temperature and or overclocking are two of the most likely culprits.
>
> Of course, if the problem is software, that won't help.
> --- David A.Wheeler

It's not a laptop; it's a desktop, with a package liquid cooling
system. 'sensors' is telling me the CPU (tdie temperature, on an AMD
Ryzen 7 1700X) is running at 47.0°C, which seems low for running at a
load of 8.00. It has unfixed issues where loading a GUI will crash it
pretty quickly, even after switching out GPU, so there are known
issues.

[Norman Megill]

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'.  Here's how it compares so far, normalized to a CPU taking about 30 sec for the 3atlem4 minimization.  I'll keep this updated as the logs come in. Looking at the last few, let's hope my theory is wrong... 
(updated Feb14 10:10AM EST)  (updated Feb 14 8:45PM EST)  (updated Feb 14 10:10PM EST) (updated Feb 16 11:00AM EST) (updated Feb 16 2:55PM EST) (updated Feb 17 9:20AM EST) (updated Feb 20 11:10AM EST) (updated Feb 21 1:40PM EST) (updated Feb 27 6:30PM EST)

                              est.    actual hours
job133.cmd: fourierdlem54     0.8      4.4
job134.cmd: icccncfext        1.6      8.4
job135.cmd: fourierdlem91     2.6      8.9
job136.cmd: fourierdlem49     3.0      3.5
job137.cmd: fourierdlem50     3.3      7.3
job138.cmd: fourierdlem93     3.4      4.3
job139.cmd: midexlem          3.6      2.8
job140.cmd: miriso            3.9      1.8
job141.cmd: fourierdlem89     4.2      6.5
job142.cmd: tgbtwnconn1lem3   4.7      2.9
job143.cmd: fourierdlem42     6.3      6.4
job144.cmd: fourierdlem48    10.1     13.5
job145.cmd: fourierdlem112   14.1     27.3
job146.cmd: fourierdlem64    20.3     22.4
job147.cmd: fourierdlem65    24.6     93.3*
job148.cmd: fouriersw        29.5     28.2
job149.cmd: fourierdlem73    31.2     17.0*
job150.cmd: fourierdlem76    35.0     57.0*
job151.cmd: ioodvbdlimc1lem1 40.4     30.0*
job152.cmd: ioodvbdlimc1lem2 35.5     23.3
job153.cmd: ioodvbdlimc2lem  38.6     22.2
job154.cmd: fourierdlem45    40.3     15.2
job155.cmd: fourierdlem111   46.4     64.9*
job156.cmd: fourierdlem81    47.9     21.2
job157.cmd: fourierdlem104   61.3     60.4*
job158.cmd: fourierdlem103   91.0     51.5
job159.cmd: footex          268.8     71.8
job160.cmd: mideulem        404.4    200.7*

The job status page is https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ

* 3atlem4 took ~45s for these jobs but ~35s for DAW's other jobs on the same computer.  I am assuming 35s for the normalization.

Norm

[Giovanni Mascellani]

Hi,

first of all, Norm, could you please allocate 113-124 to me? Thanks. I
am running them on a couple of 8-threads server-class machines.

Il 14/02/20 00:19, David A. Wheeler ha scritto:

> # We're ready! Now plug in your JOB_NUMBERS, e.g.:
> # scripts/jobs 112 125-132 144-151
> scripts/jobs JOB_NUMBERS

Here it complains that the metamath executable is not in the path. I
fixed by adding this command:

$ export PATH=metamath:$PATH

Ah, I notice now that the metamath executable is copied in ~/bin. But
not every system has that in the PATH by default. Users that do not have
it might end up calling the system-installed metamath executable if
there is one. Maybe hardcoding the path in the script might be beneficial.

Also, I prepended the scripts/jobs command with nice, so that other
processes running on the same machine are not adversely affected. It
should not disturb the computation. Other users might want to do the same.

[heiph...@wilsonb.com]

Giovanni,

Currently, Norm has me assigned to the 113-116. Last email I saw, there were
still several other ranges open, however. If that's changed and all slots are
allocated, I certainly don't mind sharing my batch.

Cheers,

[Giovanni Mascellani]

Hi,

Il 14/02/20 11:04, heiphohmia via Metamath ha scritto:

> Currently, Norm has me assigned to the 113-116. Last email I saw, there were
> still several other ranges open, however. If that's changed and all slots are
> allocated, I certainly don't mind sharing my batch.

Oh, my bad, I looked at the wrong email. Please reduce my batch to
117-122, if that's still free.

[Norman Megill]

Here is the current status, Feb 14 7:25AM EST (updated Feb. 14 10:10AM EST) (updated Feb. 14 1:45PM EST) (updated Feb. 14 8:30PM EST) (updated Feb. 15 10:40AM EST) (updated Feb. 15 5:20PM EST) (updated Feb. 16 11:00AM EST) (updated Feb. 16 3:05PM EST) (updated Feb. 20 11:10AM EST) (updated Feb. 21 1:40PM EST)

*101 Alexander (complete)

*102 heiphohmia (complete)

*103-111 David Starner (complete)

*112 David A. Wheeler  (complete)

*113-115 heiphohmia (complete)

*116 Norm (complete)

*117-122 Giovanni (complete)

*123-124 Mario (complete)

*125-132 David A. Wheeler (complete)

*133-143 David Starner (complete)

*144-151 David A. Wheeler (complete)

*152-155 David Starner (complete)

*156 Mario (complete)

*157 David A. Wheeler (complete)

*158 Mario (complete)

*159 David A. Wheeler (complete)

160  David A. Wheeler (was Mario) (in progress)

Note:  Thierry may break up the theorems in 159 and 160 into smaller lemmas.

Here are the current instructions: https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/aI3Xc8w2BAAJ that point to the set.mm version we should use.
See David A. Wheeler's post https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/CJSwJ7p8BAAJ if you want to use his script.
Here are my (possibly wrong) time guesstimates for jobs 133-160: https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/WmovUJiKBAAJ

Norm

[Thierry Arnoux]

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?

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

[Norman Megill]

On Friday, February 14, 2020 at 8:01:47 AM UTC-5, Thierry Arnoux wrote:

If ~ footex and ~ mideulem are too long, I may split them into smaller lemmas, and then run minimize on the smaller lemmas.

That would be the preferred thing to do, because it means that we won't have the problem in the future.  As a rule of thumb, the time for 'save proof .../compressed/time' should ideally be less than roughly 10 sec.  There is definitely some faster-than-linear growth in time vs. proof length going on (even for just 'save proof../compressed'), which I'm trying to understand the cause of, but I don't think I will be able to speed it up before this 'minimize' project is done.
 

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 can specify a single statement range in the 'minimize' argument e.g. 'minimize ax-1~ax-ac /a * /n ax-*' (multiple ranges separated by commas aren't implemented yet, it's on my todo list).  The minimization can thus be done in several pieces.  Although this won't account for interactions due to scan order (i.e. the difference between the forward scan and reverse scan), they typically aren't that great and not worth worrying about in individual cases like this.

That said, if you could break up those proofs, it would be great.

Norm

[David A. Wheeler]

> Il 14/02/20 00:19, David A. Wheeler ha scritto:
> > # We're ready! Now plug in your JOB_NUMBERS, e.g.:
> > # scripts/jobs 112 125-132 144-151
> > scripts/jobs JOB_NUMBERS

On Fri, 14 Feb 2020 10:07:56 +0100, Giovanni Mascellani <g.masc...@gmail.com> wrote:
> Here it complains that the metamath executable is not in the path. I
> fixed by adding this command:
> $ export PATH=metamath:$PATH
>
> Ah, I notice now that the metamath executable is copied in ~/bin. But
> not every system has that in the PATH by default. Users that do not have
> it might end up calling the system-installed metamath executable if
> there is one. Maybe hardcoding the path in the script might be beneficial.

I want to make sure that people can choose which metamath executable they run.
Appending to the existing PATH, to increase the likelihood of getting the right one
if it's not already on the PATH, seems like the better solution.

> Also, I prepended the scripts/jobs command with nice, so that other
> processes running on the same machine are not adversely affected. It
> should not disturb the computation. Other users might want to do the same.

Good idea.

I have completed 10 jobs & 8 more are in progress.
I intent to wait for them to complete before I change my "jobs" script.
Below are the changes I plan to make to jobs script.
I plan to integrate the basics of those ideas, and also change the makefile
so that on failure the log file will stick around.

--- David A. Wheeler

==========================

diff --git a/scripts/jobs b/scripts/jobs
index 045a57ca..b928d4de 100755
--- a/scripts/jobs
+++ b/scripts/jobs
@@ -43,6 +43,10 @@ find_work_list () {
done
}

+# If metamath is *already* on the PATH, that one will be used.
+# If not, increase the likelihood of finding a working "metamath" command
+PATH="$PATH:${PWD}/metamath:${HOME}/bin"
+
command -v metamath > /dev/null || die 'Metamath program not on path'
[ "$#" -gt 0 ] || die 'Requires parameters, e.g., 112 118-140'

@@ -58,13 +62,17 @@ master_log='metamathjobs/master.log'
# Generate expanded list of space-separated job numbers
work="$(find_work_list "$@" | tr '\r\n' ' ')"

-echo 'Starting jobs. View job NUM with: tail -c +0 -f metamathjobs/jobNUM.log'
-echo "View overall state with: tail -c +0 -f ${master_log}"
+echo 'Starting jobs.'
+echo "View overall (master) state log with: tail -c +0 -f ${master_log}"
+echo 'View job NUM log with: tail -c +0 -f metamathjobs/jobNUM.log'
+echo 'Print number of completed jobs with: ls metamathjobs/*.done | wc -l'
echo

+# Use GNU make to run jobs in parallel. We use GNU make, not GNU parallel,
+# to simplify skipping jobs we've already completed (which have .done files).
# We use "nproc" to find the number of CPUs if NPROC is not set.

-nohup make --jobs "${NPROC:-$(nproc)}" -r -f scripts/jobs.makefile \
+nohup nice make --jobs "${NPROC:-$(nproc)}" -r -f scripts/jobs.makefile \
work="$work" > "$master_log" 2>&1 &

echo
diff --git a/scripts/jobs.makefile b/scripts/jobs.makefile
index c5d12fbc..d5234e3c 100644
--- a/scripts/jobs.makefile
+++ b/scripts/jobs.makefile
@@ -4,21 +4,20 @@
all: alljobs
@echo 'DONE.'

-LOG_LIST := \
- $(foreach num, $(work), metamathjobs/job$(num).log)

[David A. Wheeler]

On Thu, 13 Feb 2020 19:33:14 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> 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'. ...
> job160.cmd: mideulem 404.4

That's less than 17 days, or only about 2 1/2 weeks.
No big deal. I've had other (non-metamath) process executions take longer.
Computer time is *way* cheaper than human time.

That said, if we could reasonably break up that proof into smaller components
instead of its current 334 steps, it would probably be easier to *understand*

--- David A. Wheeler

[David A. Wheeler]

(Replying to myself)

Sorry, I didn't copy the entire set of propose changes
for jobs and jobs.makefile (they got cut off).
So I tweaked it further, and here's the entire set of diffs.
Suggestions welcome.

--- David A. Wheeler

====================================
diff --git a/scripts/jobs b/scripts/jobs
index 045a57ca..3a0f9b8e 100755

--- a/scripts/jobs
+++ b/scripts/jobs
@@ -43,6 +43,10 @@ find_work_list () {
done
}

+# If metamath is *already* on the PATH, that one will be used.
+# If not, increase the likelihood of finding a working "metamath" command
+PATH="$PATH:${PWD}/metamath:${HOME}/bin"
+
command -v metamath > /dev/null || die 'Metamath program not on path'
[ "$#" -gt 0 ] || die 'Requires parameters, e.g., 112 118-140'

@@ -58,13 +62,17 @@ master_log='metamathjobs/master.log'
# Generate expanded list of space-separated job numbers
work="$(find_work_list "$@" | tr '\r\n' ' ')"

-echo 'Starting jobs. View job NUM with: tail -c +0 -f metamathjobs/jobNUM.log'
-echo "View overall state with: tail -c +0 -f ${master_log}"

+echo "Starting jobs at $(date)"

+echo "View overall (master) state log with: tail -c +0 -f ${master_log}"
+echo 'View job NUM log with: tail -c +0 -f metamathjobs/jobNUM.log'
+echo 'Print number of completed jobs with: ls metamathjobs/*.done | wc -l'
echo

+# Use GNU make to run jobs in parallel. We use GNU make, not GNU parallel,
+# to simplify skipping jobs we've already completed (which have .done files).
# We use "nproc" to find the number of CPUs if NPROC is not set.

-nohup make --jobs "${NPROC:-$(nproc)}" -r -f scripts/jobs.makefile \
+nohup nice make --jobs "${NPROC:-$(nproc)}" -r -f scripts/jobs.makefile \
work="$work" > "$master_log" 2>&1 &

echo
diff --git a/scripts/jobs.makefile b/scripts/jobs.makefile

index c5d12fbc..dcf6a78c 100644
--- a/scripts/jobs.makefile
+++ b/scripts/jobs.makefile
@@ -2,23 +2,24 @@
# "work" is a list of simple numbers.

all: alljobs
+ @echo 'Completion time: $(date)'
+ @echo

@echo 'DONE.'

-LOG_LIST := \
- $(foreach num, $(work), metamathjobs/job$(num).log)

+DONE_LIST := \
+ $(foreach num, $(work), metamathjobs/job$(num).done)

-metamathjobs/job%.log: metamathjobs/job%.cmd
- @echo "Running job $*"
- @rm -f "metamathjobs/job$(*).log"
+metamathjobs/job%.done: metamathjobs/job%.cmd
+ @echo 'Running job $(*)'
+ @rm -f 'metamathjobs/job$(*).log'
time metamath 'read set.mm' \
"open log 'metamathjobs/job$(*).log'" \
"submit 'metamathjobs/job$(*).cmd' /silent" quit 2>&1
+ @touch 'metamathjobs/job$(*).done'

-alljobs: $(LOG_LIST)
+alljobs: $(DONE_LIST)

-# Delete what's generated if a program returns a nonzero (error) result.
-# This can be annoying for debugging, but it means that we can simply re-run
-# make if a process is stopped.
-ifndef KEEP_ON_ERROR
+# Delete what we're creating on error.
+# NOTE: We do *NOT* delete partial logs, since they are not make targets.
+# Keeping logs around simplifies debugging.
.DELETE_ON_ERROR:
-endif

[Giovanni Mascellani]

Il 14/02/20 10:07, Giovanni Mascellani ha scritto:

> first of all, Norm, could you please allocate 113-124 to me? Thanks. I
> am running them on a couple of 8-threads server-class machines.

Oh no, that list was not up-to-date. It seems that that block reduced to
117-122. I'm taking those, then.

[Mario Carneiro]

123 and 124 completed, in about 12 and 13 hours respectively. I'm running 156 and 160 now.

Mario

--
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.

[David A. Wheeler]

On Fri, 14 Feb 2020 09:45:40 -0800, Mario Carneiro <di....@gmail.com> wrote:
> 123 and 124 completed...

I have completed these 9 jobs: 112 125-132
Their respective start/stop times are below (from the first/last lines of the log).

The results (.log files) of these jobs are here:
https://dwheeler.com/temp/results1.zip

Norm: Please download these results when you get a chance, it's 1,008,004 bytes.

I am currently running jobs 144-151.

--- David A. Wheeler

====

The log file "metamathjobs/job112.log" was opened 13-Feb-2020 3:45 PM.
The log file "metamathjobs/job112.log" was closed 13-Feb-2020 11:47 PM.

job125.log
The log file "metamathjobs/job125.log" was opened 13-Feb-2020 3:45 PM.
The log file "metamathjobs/job125.log" was closed 13-Feb-2020 11:29 PM.

job126.log
The log file "metamathjobs/job126.log" was opened 13-Feb-2020 3:45 PM.
The log file "metamathjobs/job126.log" was closed 13-Feb-2020 11:12 PM.

job127.log
The log file "metamathjobs/job127.log" was opened 13-Feb-2020 3:45 PM.
The log file "metamathjobs/job127.log" was closed 13-Feb-2020 11:07 PM.

job128.log
The log file "metamathjobs/job128.log" was opened 13-Feb-2020 3:45 PM.
The log file "metamathjobs/job128.log" was closed 14-Feb-2020 12:31 AM.

job129.log
The log file "metamathjobs/job129.log" was opened 13-Feb-2020 3:45 PM.
The log file "metamathjobs/job129.log" was closed 13-Feb-2020 10:25 PM.

job130.log
The log file "metamathjobs/job130.log" was opened 13-Feb-2020 3:45 PM.
The log file "metamathjobs/job130.log" was closed 13-Feb-2020 11:56 PM.

job131.log
The log file "metamathjobs/job131.log" was opened 13-Feb-2020 3:45 PM.
The log file "metamathjobs/job131.log" was closed 13-Feb-2020 11:53 PM.

job132.log
The log file "metamathjobs/job132.log" was opened 13-Feb-2020 10:25 PM.
The log file "metamathjobs/job132.log" was closed 14-Feb-2020 7:59 AM.

[Norman Megill]

On Friday, February 14, 2020 at 12:45:53 PM UTC-5, Mario Carneiro wrote:

123 and 124 completed, in about 12 and 13 hours respectively. I'm running 156 and 160 now.

Thanks.  Rather than send a new email for every status update, I'm editing it directly here:

https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ

Be aware that 160 may be a tough one: https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/WmovUJiKBAAJ and also Thierry may break up its proof (his last message at 8:01AM EST).  But if my estimate turns out to be too big, that would be good news.

Norm

[David A. Wheeler]

On Thu, 13 Feb 2020 06:25:42 -0800 (PST), Benoit <benoit...@gmail.com> wrote:
> Actually, most *OLD and *ALT should probably have both discouragement tags
> as well, it seems ?

I looked at the .log files I have so far. Once I "cd" into metamathjobs/ ...

I have no proposed minimizations involving "OLD":
grep 'decreased' *.log | grep OLD

But I do have some proposed minimizations involving "ALT":
grep 'decreased' *.log | grep ALT | uniq

The list:
job129.log:Proof of "dral1ALT" decreased from 81 to 16 bytes using "dral1".
job129.log:Proof of "dveeq2ALT" decreased from 41 to 15 bytes using "dveeq2".
job132.log:Proof of "ax16nfALT" decreased from 45 to 16 bytes using "ax16nf".

I don't think we want to apply these minimizations :-).

As a first cut, we might just skip anything involving ALT or OLD, then look more carefully.

At the least, we shouldn't use THEOREMT to prove THEOREMTALT.

--- David A. Wheeler

[Benoit]

Thanks David.  I looked at the corresponding MPE webpage (http://us2.metamath.org/mpeuni/mmtheorems21.html) and the following, and indeed

aevALT

ax16nfALT

dral1ALT

dveeq2ALT

sbequ8ALT

equsb3ALT

should have the "(Proof modification is discouraged.)" tag.  They already, and correctly, have the "(New usage is discouraged.)" tag.

This is probably due to Wolf and I moving around a few theorems (mainly Wolf reducing dependencies and moving theorems earlier, and me insisting to keep as *ALT versions shorter proofs using more axioms). This phenomenon is concentrated in this part of set.mm.

Benoît

[Norman Megill]

On Friday, February 14, 2020 at 4:15:56 PM UTC-5, David A. Wheeler 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.

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:

# Download jobs if not already downloaded

test -f min2020-jobs.zip || \

  wget http://us2.metamath.org/downloads/min2020-jobs.zip

Unfortunately these jobs will have to be rerun.  The theorems in job133.cmd through job160.cmd were not changed so those runs shou OK.

Norm

[Norman Megill]

On Friday, February 14, 2020 at 6:11:58 PM UTC-5, Norman Megill wrote:

...

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:

I mean my post https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/aI3Xc8w2BAAJ

[David Starner]

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.

> 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.

[heiph...@wilsonb.com]

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?

[Norman Megill]

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:
> 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, it is correct, but we normally don't have 1-step proofs for substitution instances because it wastes set.mm file space.  This is telling us we should delete hashssle and use hashss instead.

 

> 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.

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.

Norm

[Norman Megill]

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?

I don't mind getting them one at a time since I can do some preliminary analysis before everything is complete.  If you want to email them directly to me to save cluttering the thread, that's fine with me; some people are doing that.  Since I'm already collecting them, if anyone wants the intermediate collection of the logs we have so far, let me know.

Norm

[Norman Megill]

On Friday, February 14, 2020 at 6:41:14 PM UTC-5, Norman Megill wrote:

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.

If you have free cores, you could start 157 and 158 that haven't been assigned.  You could also start 159 if you'd like, but Thierry indicated he might break the 159 theorem into smaller lemmas.

Norm

[David A. Wheeler]

On February 14, 2020 7:14:42 PM EST, Norman Megill <n...@alum.mit.edu> wrote:
>On Friday, February 14, 2020 at 6:41:14 PM UTC-5, Norman Megill wrote:
>>
>> 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.

I will just restart and rerun my assignments, and simply consider the previous stuff a dry run. The newer scripts are better anyway.

I think what happened is that I still had the zip file around, so it simply reused the zip file. If I delete the zip file and the generated directory, I think it should be fine.


--- David A.Wheeler

[David Starner]

On Fri, Feb 14, 2020 at 4:14 PM Norman Megill <n...@alum.mit.edu> wrote:
> If you have free cores, you could start 157 and 158 that haven't been assigned. You could also start 159 if you'd like, but Thierry indicated he might break the 159 theorem into smaller lemmas.

After the ones currently running complete, I'm going to take it
offline and run a memory checker. But 155 has run for 24 hours and
hasn't hit the halfway mark (I assume backwards takes about the same
amount of time as forwards does), so I would have time to run
something that would take eight hours, but not something that might
well be slower than what I'm running now.

[Norman Megill]

I checked all the log files I have:

101-111 good

112 bad

113 good

114-122 unknown (jobs not finished)

123-124 good

125-132 bad

So 112 and 125-132 have to be redone.

For the jobs not finished, a quick way to check that you have the updated min2020-jobs.zip is to make sure that "dral1ALT" is in job124 and not in job129:

$ grep dral1ALT job*.cmd

job124.cmd:prove dral1ALT

Note that jobs 133 to 160 are not affected, because the theorems in them didn't change.

Norm

On Friday, February 14, 2020 at 8:01:10 PM UTC-5, David A. Wheeler wrote:

[David Starner]

On Fri, Feb 14, 2020 at 5:16 PM David Starner <prosf...@gmail.com> wrote:
> After the ones currently running complete, I'm going to take it
> offline and run a memory checker. But 155 has run for 24 hours and
> hasn't hit the halfway mark (I assume backwards takes about the same
> amount of time as forwards does), so I would have time to run
> something that would take eight hours, but not something that might
> well be slower than what I'm running now.

And whoops, 155 crashed and I didn't notice because I was just looking
at the log file. I've sent the log files for 152-154 to Norm, and will
give job 155 back for now.

[David A. Wheeler]

On Fri, 14 Feb 2020 15:16:37 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> > We have a more serious problem though. ~dral1ALT is not in job129.cmd, it
> > is in job124.cmd.

Thanks for letting me know! This is a good reason to provide incremental progress,
in case it's not actually progress :-).

While unfortunate, it's really no big deal. Running computers for a number of days
is not a problem, and I haven't been running it for very long.
In some ways this is nice, because my latest script improvements
are definitely improvements and now I can use them without complications.

I've already restarted my assigned jobs:
scripts/jobs 112 125-132 144-151

I also verified that this time "dral1ALT" is in job124.cmd where it's supposed to be :-).

--- David A. Wheeler

[Norman Megill]

On Friday, February 14, 2020 at 8:30:51 PM UTC-5, David A. Wheeler wrote:
> I've already restarted my assigned jobs:
> scripts/jobs 112 125-132 144-151

You didn't have to restart 144-151. Jobs 133 and above are not affected.

If any of 144-151 had already finished, do you have the logs for them? The previous log has a ~1 filename suffix so it might be salvageable - if the last line says the log closed, then it will be fine. I'm eager to fill in my estimate chart. :)

For everyone, I updated the schedule:
https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ
and the time estimate chart:
https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/WmovUJiKBAAJ

Norm

[David A. Wheeler]

On Fri, 14 Feb 2020 18:01:32 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> On Friday, February 14, 2020 at 8:30:51 PM UTC-5, David A. Wheeler wrote:
> > I've already restarted my assigned jobs:
> > scripts/jobs 112 125-132 144-151
>
> You didn't have to restart 144-151. Jobs 133 and above are not affected.

True, but it's also complicated to manage systems with different scripts.
The jobs only ran for a little over a day, which is nothing.
Besides, the newer scripts are much better. In particular, if
you stop a job with the old scripts, any partial log files disappeared,
and that's annoying for debugging.

For my own sanity (& to reduce the likelihood of future mistakes)
I wanted to "keep it simple" by just restarting the whole thing.

If we wanted to something far more sophisticated I could use slurm-llnl
or similar systems for managing parallel workloads. But I think those
are more complex for "getting started".

> If any of 144-151 had already finished, do you have the logs for them?

> ... I'm eager to fill in my estimate chart. :)

Sure! I finished 144 and 149. I posted them here:
https://dwheeler.com/temp/job144.log
https://dwheeler.com/temp/job149.log

Here are their timings (first/last line of each file):
The log file "metamathjobs/job144.log" was opened 13-Feb-2020 11:07 PM.
The log file "metamathjobs/job144.log" was closed 14-Feb-2020 12:40 PM.

The log file "metamathjobs/job149.log" was opened 13-Feb-2020 11:57 PM.
The log file "metamathjobs/job149.log" was closed 14-Feb-2020 6:50 PM.

> For everyone, I updated the schedule:
> https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ
> and the time estimate chart:
> https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/WmovUJiKBAAJ

--- David A. Wheeler

[David A. Wheeler]

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

[Mario Carneiro]

It may minimize with the statement, then later minimize the statement away. I wouldn't be worried unless "idi" appears in the minimized proof.

--
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.

[Alexander van der Vekens]

In January 2020 I had a case where ~idi was *not* removed after minimize had finished, see Github issue #1426. I performed minimize again today, and it seems that the new version 0.181 12-Feb-2020 of metamath.exe does not add ~idi anymore! Let's wait for the end of the current global minimization action if new cases come up.

Actually, there are currently 12 proofs in set.mm using ~idi (~dummylink is not used at all), but all of them are in mathboxes. They should be removed by our global minimization, shouldn't they?

On Saturday, February 15, 2020 at 3:37:39 AM UTC+1, Mario Carneiro wrote:

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.

[Alexander van der Vekens]

On Saturday, February 15, 2020 at 12:28:58 AM UTC+1, David Starner wrote:

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).

[David A. Wheeler]

I have completed jobs 112 and 125-131. Their logs are posted in
https://dwheeler.com/temp/results3.zip

My system is currently working on jobs 132 and 144-150;
151 will start once any one of them finish.
I realize I already sent 144 and 149, but the redo is nearly complete
so I may as well let it finish (we can check that the answers are the same).

--- David A. Wheeler

[Norman Megill]

The occasional temporary use of dummylink and idi during a 'minimize' run is normal, but they should always disappear from the proof by the end of the run.

I just responded to this on the issue page, which breaks down step by step what is going on and shows how to debug this.

Sorry for the delay in answering the issue.  I had a large number of emails that day and somehow this got overlooked.

Norm

[Norman Megill]

Thanks.  I updated the status of your and Giovanni's runs.

https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ

Norm

[Benoit]

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).

Regarding: ~bj-abf: it is the same statement as ~abf but it is proved from ~bj-abfal, which is the corresponding closed form.  In my opinion, ~bj-abfal should be moved to main (as ~abfal or ~abft ?) and ~abf shoud be proved from it.

Benoît

[David A. Wheeler]

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.

That would leave 157-159 unassigned.
I could work on those once more jobs finish, but
I don't know how long the current jobs will take.

--- David A. Wheeler

[Norman Megill]

On Saturday, February 15, 2020 at 2:56:18 PM UTC-5, David A. Wheeler wrote:

An update: Now I've also finished job 132, available here:
https://dwheeler.com/temp/job132.log

Thanks.  The status is updated.  https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ 

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.

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.

Norm

[David A. Wheeler]

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

[Norman Megill]

On Saturday, February 15, 2020 at 9:35:05 PM UTC-5, David A. Wheeler wrote:

...

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?

OK, I'll assign 157 to you. 

Norm

[Mario Carneiro]

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/88673fc3-7d62-4ecb-8140-4e413c381476%40googlegroups.com.

[Thierry Arnoux]

Hi Norm,

How do I best submit the change to break down those theorems/lemma?
I may be able to provide something for ~mideulem soon, breaking it into 3.

BR,
_
Thierry

[fl]

156 is done (after 31.8 hours), starting 158. 160 is still running.

31.8 hours ! Gosh ! And set.mm has been divided into 60 parts !

-- 

FL

[Norman Megill]

Thanks.  I updated the status: https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ
with 158 assigned to you.

[Norman Megill]

I would suggest that you run the minimizations on your pieces (calling them say job160a, job160b, job160c for mideulem).  Before my final minimize run I will use your logs from these 3 new jobs to extract the minimizations, after you do a PR for the break down.  Since all other jobs are using a fixed set.mm, there should be no conflict with them.  (I would still like to see the run times for the original 159 (David W.) and 160 (Mario) if they ever complete.)

Norm

[Mario Carneiro]

158 is done (after 62.8 hours), starting 159. 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.

[Norman Megill]

Thanks.  Note that per the status post below (that I keep updated without emailing the group), DAW is currently running 159.  While I think it is a good idea to run another in parallel given the unreproducible segfaults on 2 computers, I'm just letting you know.

It would also be interesting to compare the run times.  DAW has seen varying run times from 35s to 46s for 3atlem4 on the same computer, and I see that your jobs 123,124,156,158 took 48s,49s,45s,36s resp.  I am using those times to normalize the run times in my estimates post.  I am curious, though, were these jobs on the same computer or different ones?

The metamath program uses the clock() function in C to measure the run time.  In metamath.exe, the lcc compiler uses elapsed time for clock().  I think gcc is supposed to use "processor time" per the C spec although it's not clear to me precisely what that means because it can vary significantly from run to run.  Are you using metamath.exe on Windows or a gcc compilation?  Did anyone else use metamath.exe for their job runs?

As a reminder, here are the posts that I keep updated:

status: https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ

estimates: https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/WmovUJiKBAAJ

Norm

On Tuesday, February 18, 2020 at 1:53:13 PM UTC-5, Mario Carneiro wrote:

158 is done (after 62.8 hours), starting 159. 160 is still running.