A faster way to get modification dates

Makefile

@@ -114,33 +114,37 @@ meta-data/section.data: meta-data/annex-f meta-data/networking-section.data bin/
 
 dates: meta-data/dates
 
+optcmd = $(shell command -v $(1) || echo :)
+
 # Generate file with issue number and unix timestamp of last change.
-meta-data/dates: xml/issue[0-9]*.xml
+python := $(call optcmd,python)
+meta-data/dates: xml/issue[0-9]*.xml bin/make_dates.py
 	@echo "Refreshing 'Last modified' timestamps for issues..."
-	@for i in xml/issue[0-9]*.xml ; do \
-	  n="$${i#xml/issue}" ; n="$${n%.xml}" ; \
-	  grep -s -q "^$$n " $@ && test $$i -ot $@ && continue ; \
-	  echo $$i >&2 ; \
-	  git log -1 --pretty="format:$$n %ct%n" $$i ; \
-	done > [email protected]
-	@cat $@ [email protected] | sort -n -r | sort -n -k 1 -u > [email protected]
-	@rm [email protected]
-	@$(call update,$@)
-
+	@if [ "$(python)" = ":" ]; then \
+	  for i in xml/issue[0-9]*.xml ; do \
+	    n="$${i#xml/issue}" ; n="$${n%.xml}" ; \
+	    grep -s -q "^$$n " $@ && test $$i -ot $@ && continue ; \
+	    echo $$i >&2 ; \
+	    git log -1 --pretty="format:$$n %ct%n" $$i ; \
+	  done > [email protected]; \
+	  cat $@ [email protected] | sort -n -r | sort -n -k 1 -u > [email protected]; \
+	  rm [email protected]; \
+	  $(call update,$@); \
+	else \
+	  git whatchanged --no-show-signature --pretty=%ct | $(python) bin/make_dates.py > $@; \
+	fi
 
 new-papers:
 	rm -f meta-data/index.json meta-data/paper_titles.txt
 	$(MAKE) meta-data/paper_titles.txt
 
-optcmd = $(shell command -v $(1) || echo :)
-
-# If python is not installed then create an empty meta-data/paper_titles.txt
+# If curl is not installed then create an empty meta-data/paper_titles.txt
 meta-data/index.json:
 	$(call optcmd,curl) https://wg21.link/index.json > $@
 
 # If python is not installed then create an empty meta-data/paper_titles.txt
 meta-data/paper_titles.txt: | meta-data/index.json
-	$(call optcmd,python) bin/make_paper_titles.py $| > $@
+	$(python) bin/make_paper_titles.py $| > $@
 
 .PRECIOUS: meta-data/dates
 .PRECIOUS: meta-data/paper_titles.txt

bin/make_dates.py

@@ -0,0 +1,38 @@
+#!/usr/bin/python
+
+# usage: git whatchanged --no-show-signature --pretty=%ct | python bin/make_dates.py > dates
+
+import sys
+import re
+
+# The input looks like
+# 1728481670
+#
+# :100644 100644 02412851ac 9f5998ba82 M  xml/issue4159.xml
+# :100644 100644 fa2274aa17 74485b30c1 M  xml/issue4162.xml
+# :100644 100644 8023699cb9 d007f71c08 M  xml/issue4164.xml
+
+mtimes = {}
+current_mtime = ''
+for l in sys.stdin.readlines():
+    l = l.rstrip()
+    if not l:
+        # blank line
+        continue
+
+    # timestamp
+    if l[0] != ':':
+        current_mtime = l
+        continue
+
+    # last piece of line is the file name
+    file = l.split()[-1]
+    m = re.match('xml/issue(\\d+).xml', file)
+
+    if m: 
+        num = int(m[1])
+        if num not in mtimes:
+            mtimes[num] = current_mtime
+
+for (num, time) in sorted(list(mtimes.items())):
+    print(f'{num:04} {time}')