Skip to content

Commit

Permalink
Another fix to the profiling workflow (#1039)
Browse files Browse the repository at this point in the history
  • Loading branch information
fredrik-bakke authored Feb 22, 2024
1 parent 45c7fd8 commit f7b5f91
Showing 1 changed file with 14 additions and 13 deletions.
27 changes: 14 additions & 13 deletions .github/workflows/profiling.yaml
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
name: Profile library typechecking
name: Profile Library Typechecking

on:
push:
branches:
- master

# Don't cancel previous runs of the same branch
concurrency:
group: '${{ github.workflow }}'
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: false

jobs:
Expand All @@ -16,11 +16,12 @@ jobs:
matrix:
os: [ubuntu-latest]
agda: ['2.6.4']

steps:
- name: Checkout our repository
uses: actions/checkout@v3
with:
path: master
path: repo

- name: Setup Agda
uses: wenkokke/[email protected]
Expand All @@ -29,21 +30,21 @@ jobs:

- name: Typecheck library with profiling
run: |
cd master
mkdir temp
cd repo
mkdir -p temp
make check-profile 2> temp/memory-results.txt | tee temp/benchmark-results.txt
- name: Download previous typechecking profile
run: |
mkdir benchmark-cache
mkdir -p benchmark-cache
curl 'https://agda-unimath-benchmarks.netlify.app/data.json' -o benchmark-cache/data.json
# Stop if there is no initial data (the server gave us an HTML instead of a JSON)
(head -1 benchmark-cache/data.json | grep -v DOCTYPE) || {rm benchmark-cache/data.json; exit 0}
(head -1 benchmark-cache/data.json | grep -v DOCTYPE) || { rm benchmark-cache/data.json; exit 0; }
curl 'https://agda-unimath-benchmarks.netlify.app/data.csv' -o benchmark-cache/data.csv
- name: Process new profiling data
run: |
cd master
cd repo
python3 scripts/typechecking_profile_parser.py \
temp/benchmark-results.txt temp/memory-results.txt \
temp/benchmark-results.json ../benchmark-cache/data.csv \
Expand All @@ -54,7 +55,7 @@ jobs:
with:
tool: 'customSmallerIsBetter'
# Location of the new data
output-file-path: './master/temp/benchmark-results.json'
output-file-path: './repo/temp/benchmark-results.json'
# Location of the aggregate data
external-data-json-path: './benchmark-cache/data.json'

Expand All @@ -66,11 +67,11 @@ jobs:

- name: Prepare new revision of the profiling website
run: |
cd master
mkdir benchmark-website
cd repo
mkdir -p benchmark-website
cp website/benchmarks/index.html benchmark-website/
cp ../benchmark-cache/data.* benchmark-website/
echo 'window.BENCHMARK_DATA =' | cat - ../benchmark-cache/data.json >benchmark-website/data.js
echo 'window.BENCHMARK_DATA =' | cat - ../benchmark-cache/data.json > benchmark-website/data.js
- name: Deploy the new profiling website
run: |
Expand Down

0 comments on commit f7b5f91

Please sign in to comment.