Skip to content

feat: Added an auto generated status update page - #3

Draft
Alex-Zughaid wants to merge 20 commits into
Kernel-Science:mainfrom
Alex-Zughaid:feat-monthly-status-update
Draft

feat: Added an auto generated status update page #3
Alex-Zughaid wants to merge 20 commits into
Kernel-Science:mainfrom
Alex-Zughaid:feat-monthly-status-update

Conversation

@Alex-Zughaid

Copy link
Copy Markdown
Contributor

Runs a github action on the first of every month to generate a paper-style PDF which has the names of all commit authors and every new definition added.

Alex-Zughaid and others added 20 commits July 29, 2026 10:10
Shows a table of Physlib contributors, lines changed, and a link to a
plain-text diff for each month since January 2026. Data is fetched from
monthly-diffs/index.json in the Alex-Zughaid/physlib fork, which a
scheduled workflow there populates at the end of each month.
…g defects

Report layout:
- Split the byline into Contributors and Reviewers. Contributors are ordered
  by lines changed (summed per author from git, merges excluded) rather than
  commit count; reviewers are everyone who submitted a review dated within
  the month, overlapping contributors by design.
- Show GitHub profile display names instead of usernames, falling back to the
  username when a profile has no name set.
- Shorten declaration headings to the fewest trailing name components that
  still distinguish them within their file section.
- Report whole files added/removed alongside the line counts.
- Exclude declarations merely moved between files from "new declarations":
  the base comparison now spans every file the diff touched, not just the
  declaration's own file (78 of 1496 entries for June).

PDF correctness fixes:
- Non-ASCII characters were typeset out of order by `listings` unless
  preceded by a space, so `f <0, by simp>` printed as `f <0, by >simp` and
  `x_0` as `_0x`. Route non-ASCII through an escapeinside escape wrapped in
  \texttt{}, which keeps the identical monospace glyph.
- The `literate=` table never applied: under XeLaTeX it only matches ASCII,
  so every multi-byte entry was a no-op and those glyphs typeset as nothing.
  Glyphs DejaVu lacks now fall back to math mode.
- Source links used the remote-tracking name (`origin/master`) and pointed at
  a moving branch tip, so they 404'd and their line anchors drifted. Resolve
  the real branch name and pin blob links to the month's head commit.
- Attach docstrings across a standalone modifier line (`noncomputable` on its
  own line above the declaration), which also keeps the modifier in the
  emitted signature.

Regenerates the June report.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Addresses a review of the monthly-updates pipeline. The theme is that the
failure paths were all warnings, so a broken run still looked green.

- Never publish a report without its PDF. The JSON was written before the
  LaTeX block, and a failed compile only warned, so the workflow committed a
  row whose download link 404'd and exited 0. Compile first, publish after,
  let failures propagate, and exit non-zero if any month failed. `pdfUrl` is
  set only once a PDF exists at that path, and the listing page no longer
  falls back to guessing the path when it is absent (that fallback meant
  omitting the field still rendered a dead link). A missing LaTeX engine is
  now an error rather than a silent JSON-only publish.

- Keep the LaTeX log. The temp dir was removed in a `finally` that also runs
  on the throw path, leaving only a 25-line stdout tail of a 200-page
  document. Copy the log next to the .tex, and upload that directory as a CI
  artifact on failure - both files are gitignored, so a CI-only failure was
  previously unreproducible locally.

- Refuse to publish blank characters. Missing glyphs only warned, and the
  failure mode is a theorem statement silently missing a symbol. Validate
  every non-ASCII codepoint in the emitted LaTeX against the font's own cmap
  before compiling, and treat log-reported missing glyphs as fatal. The
  cmap reader is verified against the compiler's own diagnostics: it agrees
  on all 13 glyphs XeLaTeX reported missing, with no false positives.

- Deduplicate `pdfauthor`. Contributors and reviewers overlap by design in
  the byline, where the groups are labeled, but the metadata field is a flat
  list where the repetition is just a name printed twice (7 in June).

- Harden the GitHub layer: retry 5xx/429/secondary-limit responses honouring
  retry-after, catch per pull request so one bad response costs one PR rather
  than emptying the whole reviewers section, and cache profile lookups at
  module scope so a backfill resolves each person once.

- Harden the workflow: pin setup-tectonic to a commit SHA (the job holds
  contents:write and MIRROR_PAT), fetch-depth 0 so the rebase works, a
  60-minute timeout, and guard the mirror step on the credential existing.

Verified by forcing each failure path: no engine, a failing compile, and
--no-pdf all behave as intended.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…matter

Content changes to the generated report.

Typography, in rough order of how often it showed:

- Render Markdown code spans in docstrings as \texttt. Backticks were passed
  through to LaTeX, where ` opens a single quote, so `Foo` set as ‘Foo‘ - an
  opening quote at both ends. 486 of 735 docstrings contain a code span, so
  this was on nearly every page. An unpaired backtick now prints as one
  rather than opening a quotation that never closes.

- Head anonymous instances with their type. 76 declarations were titled
  «instance@8aef359a», Lean's generated name, in both the heading and the
  three-page table of contents; they now read `instance T2Space
  ConfigurationSpace`, taken from the signature that was already printed
  underneath.

- Stop \texttt headings from splitting identifiers. texEscape maps Unicode
  into \ensuremath, and a math box inside \texttt carries its own spacing, so
  `β_toReal` set as `β _toReal`. Headings now keep any character the mono
  font can draw, and only fall back to math for the glyphs it genuinely
  lacks.

- Widen the TOC number column: subsection numbers pass 2.99 in a busy month
  and collided with the title.

Front matter:

- Lead with the period covered (1--30 June 2026) rather than the build date,
  which moves to small print - a citation refers to the June report, not to
  whenever it was typeset.
- Expand the abstract from three lines of provenance to say what Physlib is,
  what period this covers, and what happened in it, for a reader arriving
  from a DOI resolver with no context.
- Order the byline alphabetically. A credit list should not rank the people
  in it; the tables below still answer who did how much.

Tables and text:

- Add New/Deleted file columns to the modified-subfolders table.
- Drop the "declarations that were only edited, golfed or moved are
  excluded" sentence from the introduction, and the notes in 1.1/1.2 about
  the two lists overlapping.

Regenerates the June report.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Added a way to recognise first time contributors
also added carousel on home page
commit 599fa7d
Author: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com>
Date:   Wed Aug 12 16:12:51 2026 +0100

    reworked layout

    also added carousel on home page

commit f26baf0
Author: Gabriele Battimelli <info@gabrielebattimelli.com>
Date:   Tue Aug 11 09:01:54 2026 -0400

    fix(ci): skip the mirror job outside the canonical repo

    The mirror copies .github/ as well, so the personal mirror ran this
    workflow against itself and failed authentication on the MIRROR_PAT
    secret it does not have. Guard the job on github.repository, matching
    the guard already used by the docs workflow.

commit 2de6f5a
Author: Gabriele Battimelli <info@gabrielebattimelli.com>
Date:   Tue Aug 11 08:56:08 2026 -0400

    fix(ci): rewrite commit authorship on the personal mirror

    Vercel's Hobby plan refuses to build any commit whose author is not the
    account owner, so every contributor commit since 2026-07-27 has been
    blocked. Mirror the full history with the author and committer rewritten
    to the account owner, and push all branches and tags with --prune so
    deletions propagate.

    The rewrite is deterministic, so mirrored commit hashes stay stable
    across runs. The canonical repo keeps real authorship; the mirror is
    only a deploy artifact.

commit 86446f8
Merge: c22d55d b49e1f5
Author: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date:   Tue Aug 11 13:27:36 2026 +0100

    Merge pull request Kernel-Science#4 from Alex-Zughaid/contribution-guide-improvements

    feat: Added a single place for all information about contributing via GitHub

commit b49e1f5
Author: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com>
Date:   Fri Jul 31 15:12:49 2026 +0100

    changes discussed in meeting

commit b36a521
Author: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com>
Date:   Thu Jul 30 12:46:46 2026 +0100

    few extra bits about names and alpha

commit 030ac9e
Author: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com>
Date:   Wed Jul 29 09:47:32 2026 +0100

    changes inspired by MathLib website

commit 956e163
Author: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com>
Date:   Wed Jul 29 09:19:00 2026 +0100

    improved github description and changed wording of PR triage

commit 069a30a
Author: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com>
Date:   Tue Jul 28 17:52:07 2026 +0100

    improved look

commit 5bf212e
Author: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com>
Date:   Tue Jul 28 12:47:19 2026 +0100

    improved layout and added trend trackers

commit d186de7
Author: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com>
Date:   Mon Jul 27 18:14:41 2026 +0100

    added trend indicator

commit d2c0f20
Author: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com>
Date:   Mon Jul 27 18:10:14 2026 +0100

    Update github-summary.tsx

commit 2252550
Author: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com>
Date:   Mon Jul 27 18:01:49 2026 +0100

    added the reviewer load stuff (uses the same webhook as bot)
loadScript() treated an existing <script src=...> tag as proof the script
had finished loading. Under React Strict Mode's dev-only mount/unmount/
remount cycle, the remount's call sees the tag from the first mount
already in the DOM and resolves immediately, racing ahead to call
.graphviz() before d3-graphviz has actually finished executing - causing
"window.d3.select(...).graphviz is not a function". Cache the load
promise itself so repeat calls await the same real completion.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant