Skip to content

.github/workflows/main.yml #1572

.github/workflows/main.yml

.github/workflows/main.yml #1572

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 mathlib4
run: git clone https://github.com/leanprover-community/mathlib4
- 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
cp mailmap/mailmap mathlib4/.mailmap
./gitstats.py mathlib docs
./gitstats.py mathlib4 docs4
cp docs4/gitstats.js docs/gitstats4.js
# - 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: 'leanprover.community@gmail.com'
message: 'Update gitstats'
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}