update front materials #4
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: Clean build and profiling of library | |
| on: | |
| push: | |
| branches: | |
| - master | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: false | |
| jobs: | |
| typecheck-clean: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| agda: ['2.8.0'] | |
| permissions: | |
| contents: write | |
| steps: | |
| - name: Checkout our repository | |
| uses: actions/checkout@v4 | |
| with: | |
| path: repo | |
| - name: Setup Agda ${{ matrix.agda }} (prebuilt) | |
| uses: ./repo/.github/actions/setup-agda | |
| with: | |
| agda-version: ${{ matrix.agda }} | |
| - name: Typecheck library with profiling | |
| run: | | |
| cd repo | |
| agda --version | |
| mkdir -p temp | |
| make check-profile 2> temp/memory-results.txt | tee temp/benchmark-results.txt | |
| - name: Save Agda build cache | |
| uses: actions/cache/save@v4 | |
| with: | |
| path: repo/_build | |
| key: | |
| ${{ runner.os }}-check-${{ github.ref }}-${{ matrix.agda }}-${{ | |
| hashFiles('repo/src/**') }} | |
| - name: Download previous typechecking profile | |
| run: | | |
| mkdir -p benchmark-cache | |
| cd repo | |
| git fetch origin benchmark-data || true | |
| if git show-ref --verify --quiet refs/remotes/origin/benchmark-data; then | |
| git show origin/benchmark-data:data.json > ../benchmark-cache/data.json | |
| else | |
| cp website/benchmarks/data.json ../benchmark-cache/data.json | |
| fi | |
| - name: Process new profiling data | |
| run: | | |
| cd repo | |
| python3 scripts/typechecking_profile_parser.py \ | |
| temp/benchmark-results.txt temp/memory-results.txt \ | |
| temp/benchmark-results.json ../benchmark-cache/data.csv \ | |
| ${{ github.sha }} | |
| - name: Merge JSON profiling data | |
| uses: rhysd/github-action-benchmark@v1 | |
| with: | |
| tool: 'customSmallerIsBetter' | |
| # Location of the new data | |
| output-file-path: './repo/temp/benchmark-results.json' | |
| # Location of the aggregate data | |
| external-data-json-path: './benchmark-cache/data.json' | |
| - name: Publish the profiling CSV as an artifact | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: 'Library profiling history' | |
| path: './benchmark-cache/data.csv' | |
| - name: Update benchmark-data branch | |
| env: | |
| GITHUB_TOKEN: ${{ github.token }} | |
| run: | | |
| repo_url="https://x-access-token:${GITHUB_TOKEN}@github.com/${GITHUB_REPOSITORY}.git" | |
| git clone --depth 1 --branch benchmark-data "${repo_url}" benchmark-data-branch || true | |
| if [ ! -d benchmark-data-branch/.git ]; then | |
| git init benchmark-data-branch | |
| cd benchmark-data-branch | |
| git checkout --orphan benchmark-data | |
| git remote add origin "${repo_url}" | |
| else | |
| cd benchmark-data-branch | |
| fi | |
| cp ../benchmark-cache/data.json ./data.json | |
| cp ../benchmark-cache/data.csv ./data.csv | |
| git config user.name "github-actions[bot]" | |
| git config user.email "41898282+github-actions[bot]@users.noreply.github.com" | |
| git add data.json data.csv | |
| git commit -m "Update benchmark history for ${GITHUB_SHA}" || exit 0 | |
| git push origin benchmark-data |