Project infrastructure issues

Stream: FLT

[Kevin Buzzard]

I've just seen this today #general > Project dashboard @ 💬 which seems to indicate that we could be doing a couple of things better (but I don't really understand how to do them better). (I've been away for over a week but am back now)

[Kim Morrison]

Here's the relevant stuff:

• :check: Latest toolchain tag: v4.22.0-rc4

• :light_bulb: Detected a workflow build set up by hand.
  A GitHub Action exists to handle this workflow for you.
  See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.

• :check: Detected workflow docs, using the action: leanprover-community/docgen-action

• :check: Detected workflow release-tag, using the action: leanprover-community/lean-release-tag
• :check: Detected workflow update, using the action: leanprover-community/mathlib-update-action
• :check: License: Apache License

• :working_on_it: Consider adding a lint driver.
  You can configure the lake lint command to automatically report code quality suggestions.
  Linters are included with Mathlib or Batteries.
  For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter

• :check: Linting to Mathlib's standards.

• :light_bulb: Consider adding a test driver.
  You can configure the lake test command to build and run test files.
  For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

[Ruben Van de Velde]

Do we need a test driver if we don't have any tests?

[Kim Morrison]

I don't think it's unreasonable that maths projects have tests folders. e.g. if at any point some typeclass search timed out, but you fixed it, the tests folder is a good place to put a regression test (i.e. a #synth statement). But yeah, many won't.

[Ruben Van de Velde]

Yeah, not saying we'd never have any tests, but there doesn't seem to be much need for a driver until then

[Kevin Buzzard]

OK so after a summer of distractions I'm back to working on FLT every day. Right now I am attempting to stop being a complete CI ignoramus; up until now all CI issues have been handled by other people. I would like to try and understand the messages above and furthermore how to fix them, so I've opened the .github directory in FLT for the first time in my life and I'm trying to understand what's in there.

Let's start with the most recent issue in the FLT repo, namely FLT#706 , which was opened by a bot. As far as I can see, it's impossible to tell from the issue itself exactly why this issue was opened, what script was run etc etc. I am pretty confident that ultimately the source of this issue is .github/workflows/update.yml, which seems to be running a script from the totally different repo leanprover-community/mathlib-update-action. Right now (based on experience with the FLT repo) this script seems to be running once a week and creating an issue if a mindless bump of the master branch of Mathlib on FLT fails to build.

I'll get to the issues above a bit later, but I just wanted to check: am I right so far? And why is this script running at all? Is it just the case that every script in .github/workflows is just being run...erm...hmm. Perhaps each file specifies when it is to be run? For example some files in this workflows directory seem to be triggered by e.g. a push, but this file is being triggered by a cron job which (if my understanding of cron is correct) is probably running at 8am (probably a lousy time to run cron jobs because it's on the hour so github is overloaded with cron jobs) on dates for which the day is a multiple of 7 (so it's not even weekly :-) ).

I really like the idea of running this job weekly (and will probably edit the cron job after this discussion so it runs at 2:37am on Sunday nights UK time, which is a far more convenient time for me).

[Ruben Van de Velde]

I don't understand cron syntax either, but yeah, the on fields says when a job is triggered. In this case on schedule, and there's a button somewhere that you can click to make it run at some other time

name: Update Dependencies
on:
  schedule:             # Sets a schedule to trigger the workflow
  - cron: "0 8 */7 * *" # Every 7 days at 08:00 AM UTC (for more info on the cron syntax see https://docs.github.com/en/actions/writing-workflows/choosing-when-your-workflow-runs/events-that-trigger-workflows#schedule)
  workflow_dispatch:    # Allows the workflow to be triggered manually via the GitHub interface

[Ruben Van de Velde]

So if you click the "actions" tab at the top next to "pull requests", you get to https://github.com/ImperialCollegeLondon/FLT/actions and in the left bar all the workflows are listed. Clicking on "Update Dependencies" (this is the name field from the yaml file), you get a link back to the yaml file, and probably a button like this:
Screenshot from 2025-09-01 14-49-13.png

[Yakov Pechersky]

For cron syntax, this is a very useful helper https://crontab.guru/

[Ruben Van de Velde]

So 37 2 * * sun might be good, though it's in UTC, not BST in summer

[Jeremy Tan]

Does UTC/BST really matter here? No

[Ruben Van de Velde]

I was responding to Kevin's comment about UK time, not particularly soliciting opinions on whether the difference would be an issue