Skip to content

add winning_of_going_to_some_winning #728

add winning_of_going_to_some_winning

add winning_of_going_to_some_winning #728

Workflow file for this run

# based on https://github.com/leanprover-community/lean-liquid/blob/master/.github/workflow/build.yml
on:
push:
name: CI
jobs:
build:
name: Build PDL
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
- name: install elan
run: |
set -o pipefail
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
~/.elan/bin/lean --version
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: make pdl
run: make pdl
bml:
name: Build BML
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
- name: install elan
run: |
set -o pipefail
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
~/.elan/bin/lean --version
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: make bml
run: make bml
stats:
name: Stats
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: install ripgrep
run: sudo apt install -y ripgrep
- name: PDL count lines in src
run: |
shopt -s globstar
wc -l Pdl/**/*.lean
- name: PDL count sorries
run: |
rg --count-matches sorry Pdl | awk -F ':' 'BEGIN {sum = 0} {sum += $2} {print $2 " " $1} END {print sum " sorries in total"}'
- name: BML count lines in src
run: |
shopt -s globstar
wc -l Bml/**/*.lean
- name: BML count sorries
run: |
rg --count-matches sorry Bml | awk -F ':' 'BEGIN {sum = 0} {sum += $2} {print $2 " " $1} END {print sum " sorries in total"}'