diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml index 09cb7857..f5aa4932 100644 --- a/.github/workflows/compile.yml +++ b/.github/workflows/compile.yml @@ -7,10 +7,7 @@ on: permissions: contents: read - -concurrency: - group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true + checks: write env: COMPILE_DIR: Benchmarks/Compile @@ -61,7 +58,7 @@ jobs: with: lake-package-directory: ${{ env.COMPILE_DIR }} build: false - use-github-cache: false + use-github-cache: false # FLT and FC take a few minutes to rebuild, so we cache the build artifacts - if: matrix.cache_pkg uses: actions/cache@v4 @@ -73,5 +70,58 @@ jobs: - run: lake build Compile${{ matrix.bench }} working-directory: ${{ env.COMPILE_DIR }} # Run the `ix` compiler over the input library env - - run: ix compile --path ${{ env.COMPILE_DIR }}/Compile${{ matrix.bench }}.lean - + - name: Run ix compile + run: ix compile --path ${{ env.COMPILE_DIR }}/Compile${{ matrix.bench }}.lean 2>&1 | tee output.txt + # Parse the ##benchmark## line into Bencher Metric Format JSON + - name: Generate benchmark JSON + run: | + line=$(grep '^##benchmark##' output.txt) + elapsed_s=$(echo "$line" | awk '{printf "%.3f", $2 / 1000}') + bytes=$(echo "$line" | awk '{print $3}') + constants=$(echo "$line" | awk '{print $4}') + throughput=$(echo "$line" | awk '{if ($2 > 0) printf "%.2f", $4 * 1000 / $2; else print 0}') + cat > benchmark.json <