Skip to content
CI

Bml: compile it all (but still with sorries - is that a word?) #53

Sign in to view logs

Bml: compile it all (but still with sorries - is that a word?)

Bml: compile it all (but still with sorries - is that a word?) #53

Workflow file for this run

.github/workflows/build.yml at a67849b
# based on https://github.com/leanprover-community/lean-liquid/blob/master/.github/workflow/build.yml
on:
push:
name: CI
jobs:
build:
name: Build
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
run: make
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: count lines in src
run: |
shopt -s globstar
wc -l Pdl/**/*.lean
- name: 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"}'