> 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.mascell...@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)
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/E1j2ck7-0000g2-I8%40rmmprod07.runbox.
