[Merged by Bors] - fix: allow build steps to access timezone by kim-em · Pull Request #28510 · leanprover-community/mathlib4

kim-em · 2025-08-16T08:59:58Z

Problem

The deprecated attribute linter was failing with timezone database errors:

unable to locate share/zoneinfo in the local timezone database at /etc/localtime

This was happening because the linter uses Std.Time.PlainDate.now to compare dates, which requires timezone information.

Solution

Add -ro /etc/timezone to landrun shell options.

Changes

Add timezone permissions to shell in .github/build.in.yml
Regenerated all build workflow files (build.yml, bors.yml, build_fork.yml)

This should fix the deprecated attribute linter failures in CI.

…te linter The deprecated attribute linter was failing with timezone database errors: 'unable to locate share/zoneinfo in the local timezone database at /etc/localtime' This adds the szenius/set-timezone@v2.0 action to all build workflows to ensure proper timezone configuration in CI environments.

github-actions · 2025-08-16T09:01:15Z

PR summary 90c0e186fd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

kim-em · 2025-08-16T09:01:32Z

I'll add a test in a follow-up PR, but because this is a CI change it needs to go in first.

bryangingechen

Thanks!
bors d+

mathlib-bors · 2025-08-16T10:25:09Z

✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

kim-em · 2025-08-16T11:13:27Z

bors merge

…e linter (#28510) ## Problem The deprecated attribute linter was failing with timezone database errors: ``` unable to locate share/zoneinfo in the local timezone database at /etc/localtime ``` This was happening because the linter uses `Std.Time.PlainDate.now` to compare dates, which requires timezone information. ## Solution Add the `szenius/set-timezone@v2.0` action to all build workflows to ensure proper timezone configuration in CI environments. ## Changes - Added timezone setup step to `.github/build.in.yml` - Regenerated all build workflow files (`build.yml`, `bors.yml`, `build_fork.yml`) - The timezone setup runs after cleanup and before jq setup This should fix the deprecated attribute linter failures in CI. Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

mathlib-bors · 2025-08-16T11:15:34Z

Build failed:

CI Success

bryangingechen · 2025-08-16T11:29:29Z

It seems we are setting etc/timezone on our runners (see the Dockerfile in the private repo for such things), so I wonder if there's some landrun setting tweak we should be making instead?

edit: I went ahead and changed this PR to that approach instead.

kim-em · 2025-08-16T23:04:02Z

Thank you! I had missed that this was a landrun issue.

kim-em · 2025-08-16T23:04:11Z

bors merge

## Problem The deprecated attribute linter was failing with timezone database errors: ``` unable to locate share/zoneinfo in the local timezone database at /etc/localtime ``` This was happening because the linter uses `Std.Time.PlainDate.now` to compare dates, which requires timezone information. ## Solution Add `-ro /etc/timezone` to `landrun` shell options. ## Changes - Add timezone permissions to `shell` in `.github/build.in.yml` - Regenerated all build workflow files (`build.yml`, `bors.yml`, `build_fork.yml`) This should fix the deprecated attribute linter failures in CI. Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

mathlib-bors · 2025-08-16T23:15:46Z

Pull request successfully merged into master.

Build succeeded:

CI Success

## Problem The deprecated attribute linter was failing with timezone database errors: ``` unable to locate share/zoneinfo in the local timezone database at /etc/localtime ``` This was happening because the linter uses `Std.Time.PlainDate.now` to compare dates, which requires timezone information. ## Solution Add `-ro /etc/timezone` to `landrun` shell options. ## Changes - Add timezone permissions to `shell` in `.github/build.in.yml` - Regenerated all build workflow files (`build.yml`, `bors.yml`, `build_fork.yml`) This should fix the deprecated attribute linter failures in CI. Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

kim-em force-pushed the fix/timezone-setup-for-deprecated-linter branch from 8fc33bb to edfb409 Compare August 16, 2025 09:00

github-actions Bot added the CI Modifies the continuous integration setup or other automation label Aug 16, 2025

kim-em mentioned this pull request Aug 16, 2025

feat: linter for stale deprecated attrs #28505

Closed

1 task

bryangingechen approved these changes Aug 16, 2025

View reviewed changes

Comment thread .github/build.in.yml Outdated

Comment thread .github/workflows/bors.yml Outdated

Comment thread .github/workflows/build.yml Outdated

Comment thread .github/workflows/build_fork.yml Outdated

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Aug 16, 2025

kim-em and others added 2 commits August 16, 2025 21:12

Update .github/build.in.yml

ebef072

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Apply suggestions from code review

81973ca

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

ghost added the ready-to-merge This PR has been sent to bors. label Aug 16, 2025

try allowing access to /etc/timezone in landrun

e07f74d

bryangingechen changed the title ~~fix: add timezone setup to build workflows to fix deprecated attribute linter~~ fix: allow build steps to access timezone Aug 16, 2025

bryangingechen removed the ready-to-merge This PR has been sent to bors. label Aug 16, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Aug 16, 2025

mathlib-bors Bot changed the title ~~fix: allow build steps to access timezone~~ [Merged by Bors] - fix: allow build steps to access timezone Aug 16, 2025

mathlib-bors Bot closed this Aug 16, 2025

mo271 mentioned this pull request Mar 10, 2026

Lean server crashing without /etc/localtime? google-deepmind/formal-conjectures#3503

Closed

Navigation Menu

Uh oh!

[Merged by Bors] - fix: allow build steps to access timezone - #28510

[Merged by Bors] - fix: allow build steps to access timezone#28510
kim-em wants to merge 4 commits into
leanprover-community:masterfrom
kim-em:fix/timezone-setup-for-deprecated-linter

kim-em commented Aug 16, 2025 •

edited by bryangingechen

Loading

Uh oh!

github-actions Bot commented Aug 16, 2025 •

edited

Loading

Uh oh!

kim-em commented Aug 16, 2025

Uh oh!

bryangingechen left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-bors Bot commented Aug 16, 2025

Uh oh!

kim-em commented Aug 16, 2025

Uh oh!

mathlib-bors Bot commented Aug 16, 2025

Uh oh!

bryangingechen commented Aug 16, 2025 •

edited

Loading

Uh oh!

kim-em commented Aug 16, 2025

Uh oh!

kim-em commented Aug 16, 2025

Uh oh!

mathlib-bors Bot commented Aug 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

kim-em commented Aug 16, 2025 • edited by bryangingechen Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Problem

Solution

Changes

Uh oh!

github-actions Bot commented Aug 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 90c0e186fd

Import changes for modified files

Declarations diff

Uh oh!

kim-em commented Aug 16, 2025

Uh oh!

bryangingechen left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-bors Bot commented Aug 16, 2025

Uh oh!

kim-em commented Aug 16, 2025

Uh oh!

mathlib-bors Bot commented Aug 16, 2025

Uh oh!

bryangingechen commented Aug 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kim-em commented Aug 16, 2025

Uh oh!

kim-em commented Aug 16, 2025

Uh oh!

mathlib-bors Bot commented Aug 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

kim-em commented Aug 16, 2025 •

edited by bryangingechen

Loading

github-actions Bot commented Aug 16, 2025 •

edited

Loading

bryangingechen commented Aug 16, 2025 •

edited

Loading