Skip to content

.github/workflows/main.yml #1214

.github/workflows/main.yml

.github/workflows/main.yml #1214

Workflow file for this run

on:
schedule:
- cron: '0 2 * * *'
push:
jobs:
mathlib_stats:
if: github.event.pusher.name != 'leanprover-community-bot'
runs-on: ubuntu-latest
name: Generate statistics about the mathlib repo
steps:
- name: Checkout scripts
uses: actions/checkout@v2
- name: Checkout mathlib
run: git clone https://github.com/leanprover-community/mathlib
- name: Checkout mathlib-mailmap
uses: actions/checkout@v2
with:
# this repo is private to prevent spambots from scraping email addresses
repository: leanprover-community/mathlib-mailmap
token: ${{ secrets.MAILMAP_GITHUB_TOKEN }}
path: mailmap
- name: install Python
uses: actions/setup-python@v1
with:
python-version: 3.8
- name: Run gitstats
run: |
cp mailmap/mailmap mathlib/.mailmap
./gitstats.py mathlib docs
- name: Install gnuplot
run: |
sudo apt-get update --fix-missing
sudo apt-get install gnuplot
- name: Make nolints graph
run: |
bash nolint_graph.sh > nolint_graph_out.txt
cut -f2 -d: nolint_graph_out.txt > rev_stats.txt
gnuplot plot.gnu
- name: push results
# push results when we push to master
if: github.repository == 'leanprover-community/mathlib_stats' && github.ref == 'refs/heads/master'
uses: EndBug/add-and-commit@v4
with:
add: 'docs'
author_name: 'leanprover-community-bot'
author_email: '[email protected]'
message: 'Update gitstats'
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}