Merge fix/psh-rank-bounded into main — Descent System + Cycle F₂ Closure #30
Workflow file for this run
This file contains hidden or 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: No Duplicate Namespace Check | |
| on: [push, pull_request] | |
| jobs: | |
| check: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean toolchain (elan + lake) | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| source $HOME/.elan/env | |
| lean --version | |
| lake --version | |
| - name: Detect duplicate namespaces (same file only) | |
| run: | | |
| dup=$(grep -R '^[[:space:]]*namespace[[:space:]]\+' -n lean 2>/dev/null \ | |
| | awk -F: '{print $1 ":" $3}' \ | |
| | sort | uniq -c | awk '$1>1 {print $2}') | |
| if [ -n "$dup" ]; then | |
| echo "Duplicate namespaces found within same file:" | |
| echo "$dup" | |
| exit 1 | |
| fi | |
| - name: Lake update | |
| run: | | |
| source $HOME/.elan/env | |
| lake update | |
| - name: Build | |
| run: | | |
| source $HOME/.elan/env | |
| lake build |