This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Add mathlib4 porting comments #643
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
name: Add mathlib4 porting comments | |
on: | |
schedule: | |
- cron: "0 0 * * *" | |
workflow_dispatch: | |
jobs: | |
build: | |
name: Update comments | |
runs-on: ubuntu-latest | |
steps: | |
- uses: actions/checkout@v3 | |
- name: install Python | |
uses: actions/setup-python@v4 | |
with: | |
python-version: 3.8 | |
- name: install latest mathlibtools | |
run: | | |
pip install git+https://github.com/leanprover-community/mathlib-tools | |
# multiline outputs are only supported in javascript | |
- name: update docstrings and generate message | |
uses: actions/github-script@v5 | |
id: generate-message | |
with: | |
script: | | |
proc = await exec.getExecOutput("python", ["./scripts/add_port_comments.py"]); | |
console.log(proc.stdout); | |
core.setOutput("FILE_LIST", proc.stdout); | |
- name: Create Pull Request | |
uses: peter-evans/create-pull-request@v4 | |
with: | |
base: master | |
commit-message: "chore(*): add mathlib4 synchronization comments" | |
title: "chore(*): add mathlib4 synchronization comments" | |
author: leanprover-community-bot <[email protected]> | |
body: | | |
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). | |
Relates to the following files: | |
${{ steps.generate-message.outputs.FILE_LIST }} | |
--- | |
I am a bot; please check that I have not put a comment in a bad place before running `bors merge`! | |
labels: | | |
easy | |
awaiting-review | |
mathlib4-synchronization |