Skip to content

convert lowercase repository name when composing BUILD_IMAGE tags#41628

Merged
vbraun merged 3 commits into
sagemath:developfrom
MingLLuo:develop
May 9, 2026
Merged

convert lowercase repository name when composing BUILD_IMAGE tags#41628
vbraun merged 3 commits into
sagemath:developfrom
MingLLuo:develop

Conversation

@MingLLuo

@MingLLuo MingLLuo commented Feb 12, 2026

Copy link
Copy Markdown
Contributor

In .github/workflows/build.yml, I added a Normalize Docker image name step (in both affected jobs) that:

  • converts GITHUB_REPOSITORY to lowercase
  • writes a normalized BUILD_IMAGE value to $GITHUB_ENV

Docker image repository names must be lowercase. With usernames/orgs containing uppercase characters (for example MingLLuo/sage), buildx fails with:
invalid tag "...": repository name must be lowercase

The similiar Issue also mentioned in #40581

📝 Checklist

  • The title is concise and informative.
  • The description explains in detail what this PR is about.
  • I have linked a relevant issue or discussion.
  • I have created tests covering the changes.
  • I have updated the documentation and checked the documentation preview.

⌛ Dependencies

X

@cxzhong cxzhong requested a review from kwankyu April 27, 2026 15:24
@cxzhong

cxzhong commented Apr 27, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Please run the workflows @vbraun @tscrim

@kwankyu

kwankyu commented Apr 27, 2026

Copy link
Copy Markdown
Collaborator

Why not modify Line 72?

@github-actions

github-actions Bot commented Apr 28, 2026 •
edited
Loading

Copy link
Copy Markdown

Documentation preview for this PR (built with commit ad70590; changes) is ready! 🎉
This preview will update shortly after each push to this PR.

@MingLLuo

MingLLuo commented Apr 28, 2026

Copy link
Copy Markdown
Contributor Author

Would it be acceptable to change line 72 to use ${{ github.repository_id }} instead of ${{ github.repository }}?

github.repository_id will avoid the issue and keep BUILD_IMAGE defined without adding more steps

@kwankyu

kwankyu commented Apr 29, 2026

Copy link
Copy Markdown
Collaborator

Would it be acceptable to change line 72 to use ${{ github.repository_id }} instead of ${{ github.repository }}?

I guess so. The path is not used outside of the action. Right?

Or if we prefer github.repository for any aesthetic reason, then I hope that at least the default ubuntu-noble-standard is factored out to the env.

@MingLLuo

MingLLuo commented Apr 29, 2026

Copy link
Copy Markdown
Contributor Author

It won't affect other parts. And I think it's a better way to solve them, without converting repo name to lowercase.

@cxzhong

cxzhong commented Apr 29, 2026

Copy link
Copy Markdown
Contributor

we should rerun the workflow to see

@kwankyu kwankyu added s: positive review github actions Pull requests that update GitHub Actions code and removed s: needs review labels Apr 29, 2026
@vbraun vbraun merged commit be847b5 into sagemath:develop May 9, 2026
27 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kwankyu kwankyu kwankyu approved these changes

+1 more reviewer

@cxzhong cxzhong cxzhong approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

github actions Pull requests that update GitHub Actions code

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@MingLLuo @cxzhong @kwankyu @vbraun