Profile typechecking performance (#1031)

- [X] Set up `make`-hook for profiling - [X] Set up GitHub workflow for profiling - [x] Generate pretty graphs based on profiling data - [x] Host graphs on a webpage ~I'm not yet completely sure I set up the workflow correctly.~ Also note that 4GB memory is not enough for this profiler to work (#985). Resolves #1030. <details><summary>Example output</summary> ```text Total 90,422ms Miscellaneous 26,895ms category-theory.category-of-maps-from-small-to-large-categories 7,846ms everything 3,827ms synthetic-homotopy-theory.functoriality-sequential-colimits 2,399ms trees.underlying-trees-elements-coalgebras-polynomial-endofunctors 2,299ms finite-group-theory.simpson-delooping-sign-homomorphism 1,900ms category-theory.slice-precategories 1,878ms synthetic-homotopy-theory.26-id-pushout 1,728ms synthetic-homotopy-theory.universal-cover-circle 1,570ms set-theory.cumulative-hierarchy 1,560ms polytopes.abstract-polytopes 1,459ms synthetic-homotopy-theory.hatchers-acyclic-type 1,446ms trees.equivalences-enriched-directed-trees 1,164ms trees.combinator-enriched-directed-trees 1,161ms trees.underlying-trees-of-elements-of-w-types 1,143ms synthetic-homotopy-theory.acyclic-maps 1,034ms finite-group-theory.abstract-quaternion-group 1,012ms commutative-algebra.joins-radical-ideals-commutative-rings 1,006ms order-theory.galois-connections 928ms category-theory.adjunctions-large-precategories 881ms group-theory.torsors 814ms group-theory.normal-submonoids 794ms ring-theory.left-ideals-generated-by-subsets-rings 665ms commutative-algebra.euclidean-domains 586ms synthetic-homotopy-theory.sections-descent-circle 540ms trees.functoriality-combinator-directed-trees 535ms synthetic-homotopy-theory.sequential-colimits 522ms finite-group-theory.subgroups-finite-groups 509ms reflection.group-solver 506ms order-theory.nuclei-large-locales 493ms category-theory.natural-transformations-functors-from-small-to-large-categories 472ms commutative-algebra.integral-domains 465ms category-theory.adjunctions-large-categories 460ms ring-theory.localizations-rings 408ms group-theory.abelianization-groups 399ms synthetic-homotopy-theory.descent-circle-equivalence-types 380ms synthetic-homotopy-theory.dependent-pushout-products 380ms graph-theory.equivalences-enriched-undirected-graphs 369ms lists.universal-property-lists-wild-monoids 359ms category-theory.full-subcategories 355ms synthetic-homotopy-theory.descent-circle-function-types 350ms commutative-algebra.joins-ideals-commutative-rings 349ms category-theory.groupoids 343ms category-theory.function-precategories 330ms commutative-algebra.zariski-locale 307ms synthetic-homotopy-theory.interval-type 291ms trees.undirected-trees 285ms orthogonal-factorization-systems.functoriality-higher-modalities 280ms linear-algebra.vectors-on-euclidean-domains 280ms group-theory.normal-cores-subgroups 280ms synthetic-homotopy-theory.descent-circle-subtypes 278ms category-theory.opposite-preunivalent-categories 274ms group-theory.substitution-functor-group-actions 269ms finite-group-theory.cartier-delooping-sign-homomorphism 260ms structured-types.dependent-products-wild-monoids 254ms ring-theory.joins-ideals-rings 253ms category-theory.restrictions-functors-cores-precategories 253ms ring-theory.joins-left-ideals-rings 243ms commutative-algebra.function-commutative-rings 240ms set-theory.cardinalities 236ms commutative-algebra.integer-multiples-of-elements-commutative-rings 233ms synthetic-homotopy-theory.descent-circle-dependent-pair-types 232ms group-theory.normalizer-subgroups 223ms category-theory.coproducts-in-precategories 219ms category-theory.opposite-large-precategories 210ms category-theory.opposite-categories 192ms group-theory.saturated-congruence-relations-monoids 189ms group-theory 186ms ring-theory.products-left-ideals-rings 178ms lists.quicksort-lists 178ms ring-theory.products-right-ideals-rings 176ms orthogonal-factorization-systems.extensions-lifts-families-of-elements 172ms category-theory 163ms modal-type-theory.flat-sharp-adjunction 159ms category-theory.yoneda-lemma-categories 154ms category-theory.representing-arrow-category 148ms group-theory.quotient-groups-concrete-groups 146ms synthetic-homotopy-theory.powers-of-loops 140ms linear-algebra.scalar-multiplication-vectors-on-rings 132ms synthetic-homotopy-theory.coequalizers 130ms category-theory.augmented-simplex-category 124ms synthetic-homotopy-theory.1-acyclic-types 124ms ring-theory.algebras-rings 123ms higher-group-theory.iterated-cartesian-products-higher-groups 123ms group-theory.cartesian-products-abelian-groups 121ms category-theory.cores-categories 121ms orthogonal-factorization-systems.local-maps 118ms commutative-algebra.function-commutative-semirings 116ms commutative-algebra.dependent-products-commutative-semirings 114ms category-theory.representable-functors-large-precategories 112ms category-theory.split-essentially-surjective-functors-precategories 112ms ring-theory.function-semirings 111ms graph-theory.trails-undirected-graphs 110ms finite-group-theory.finite-commutative-monoids 109ms commutative-algebra.ideals-commutative-semirings 109ms trees.raising-universe-levels-directed-trees 106ms category-theory.natural-numbers-object-precategories 104ms synthetic-homotopy-theory.cocartesian-morphisms-arrows 104ms order-theory 103ms group-theory.category-of-orbits-groups 101ms category-theory.products-of-precategories 99ms category-theory.exponential-objects-precategories 98ms group-theory.category-of-group-actions 97ms organic-chemistry.alcohols 96ms synthetic-homotopy-theory.spectra 90ms group-theory.representations-monoids-precategories 88ms category-theory.homotopies-natural-transformations-large-precategories 88ms structured-types.function-wild-monoids 87ms real-numbers.dedekind-real-numbers 83ms graph-theory.faithful-morphisms-undirected-graphs 83ms structured-types.pointed-universal-property-contractible-types 81ms synthetic-homotopy-theory 80ms ring-theory 79ms orthogonal-factorization-systems.factorization-operations-global-function-classes 79ms group-theory.function-abelian-groups 77ms graph-theory.raising-universe-levels-directed-graphs 77ms order-theory.accessible-elements-relations 77ms order-theory.chains-preorders 76ms category-theory.essentially-surjective-functors-precategories 74ms commutative-algebra.radical-ideals-generated-by-subsets-commutative-rings 74ms orthogonal-factorization-systems.functoriality-pullback-hom 72ms modal-type-theory.flat-dependent-pair-types 72ms synthetic-homotopy-theory.tangent-spheres 72ms group-theory.kernels-homomorphisms-concrete-groups 71ms order-theory.chains-posets 68ms ring-theory.precategory-of-semirings 65ms graph-theory.complete-bipartite-graphs 64ms ring-theory.quotient-rings 64ms commutative-algebra 63ms group-theory.cayleys-theorem 63ms synthetic-homotopy-theory.premanifolds 61ms category-theory.monomorphisms-in-large-precategories 61ms category-theory.initial-objects-precategories 60ms group-theory.intersections-subgroups-abelian-groups 58ms group-theory.inverse-semigroups 57ms commutative-algebra.multiples-of-elements-commutative-rings 53ms modal-type-theory.flat-discrete-types 53ms order-theory.well-founded-relations 52ms trees 52ms group-theory.centers-monoids 51ms category-theory.sieves-in-categories 50ms trees.rooted-undirected-trees 50ms organic-chemistry.methane 50ms order-theory.maximal-chains-posets 50ms order-theory.maximal-chains-preorders 50ms synthetic-homotopy-theory.acyclic-types 50ms category-theory.endomorphisms-in-categories 49ms group-theory.centers-semigroups 48ms group-theory.precategory-of-concrete-groups 47ms group-theory.monomorphisms-groups 46ms orthogonal-factorization-systems 45ms structured-types.finite-multiplication-magmas 43ms group-theory.function-monoids 43ms higher-group-theory.subgroups-higher-groups 41ms orthogonal-factorization-systems.local-families-of-types 40ms commutative-algebra.local-commutative-rings 39ms category-theory.representable-functors-categories 39ms synthetic-homotopy-theory.descent-circle-constant-families 39ms structured-types.cyclic-types 37ms trees.bounded-multisets 36ms orthogonal-factorization-systems.lifting-operations 36ms group-theory.precategory-of-commutative-monoids 36ms commutative-algebra.trivial-commutative-rings 35ms order-theory.lower-types-preorders 35ms group-theory.conjugation-concrete-groups 34ms graph-theory.paths-undirected-graphs 34ms ring-theory.invariant-basis-property-rings 32ms order-theory.well-founded-orders 31ms group-theory.monomorphisms-concrete-groups 31ms structured-types 31ms linear-algebra.diagonal-matrices-on-rings 30ms category-theory.essential-fibers-of-functors-precategories 30ms graph-theory 30ms group-theory.function-semigroups 30ms group-theory.transitive-group-actions 29ms group-theory.orbit-stabilizer-theorem-concrete-groups 29ms trees.empty-multisets 28ms group-theory.concrete-monoids 28ms ring-theory.radical-ideals-rings 27ms group-theory.products-of-tuples-of-elements-commutative-monoids 27ms group-theory.perfect-subgroups 26ms graph-theory.trails-directed-graphs 26ms finite-group-theory 25ms category-theory.equivalences-of-large-precategories 25ms graph-theory.vertex-covers 25ms group-theory.elements-of-finite-order-groups 25ms order-theory.directed-complete-posets 25ms graph-theory.eulerian-circuits-undirected-graphs 25ms group-theory.exponents-groups 24ms graph-theory.regular-undirected-graphs 24ms order-theory.locally-finite-posets 24ms order-theory.precategory-of-decidable-total-orders 24ms orthogonal-factorization-systems.identity-modality 24ms graph-theory.voltage-graphs 23ms finite-group-theory.alternating-groups 23ms finite-group-theory.alternating-concrete-groups 23ms order-theory.precategory-of-finite-posets 23ms modal-type-theory.sharp-codiscrete-maps 23ms orthogonal-factorization-systems.raise-modalities 22ms group-theory.mere-equivalences-group-actions 22ms reflection.boolean-reflection 21ms synthetic-homotopy-theory.mere-spheres 21ms ring-theory.characteristics-rings 21ms synthetic-homotopy-theory.morphisms-descent-data-circle 21ms group-theory.furstenberg-groups 20ms structured-types.morphisms-magmas 20ms order-theory.ideals-preorders 20ms group-theory.principal-group-actions 20ms trees.coalgebra-of-enriched-directed-trees 19ms order-theory.interval-subposets 19ms group-theory.sheargroups 19ms ring-theory.free-rings-with-one-generator 19ms trees.planar-binary-trees 18ms group-theory.normal-subgroups-concrete-groups 18ms structured-types.fibers-of-pointed-maps 18ms modal-type-theory.crisp-identity-types 18ms group-theory.dihedral-groups 17ms organic-chemistry.alkynes 17ms group-theory.exponents-abelian-groups 17ms group-theory.perfect-cores 17ms set-theory.infinite-sets 17ms group-theory.perfect-groups 17ms group-theory.orbits-group-actions 17ms orthogonal-factorization-systems.zero-modality 16ms synthetic-homotopy-theory.sequentially-compact-types 16ms group-theory.stabilizer-groups 16ms trees.coalgebra-of-directed-trees 15ms structured-types.contractible-pointed-types 15ms orthogonal-factorization-systems.separated-types 15ms trees.rooted-quasitrees 15ms ring-theory.generating-elements-rings 14ms graph-theory.hypergraphs 14ms set-theory.cantor-space 14ms orthogonal-factorization-systems.sigma-closed-modalities 14ms commutative-algebra.boolean-rings 13ms linear-algebra 13ms synthetic-homotopy-theory.join-powers-of-types 13ms lists 13ms graph-theory.directed-graph-structures-on-standard-finite-sets 12ms orthogonal-factorization-systems.sigma-closed-reflective-modalities 12ms reflection 11ms trees.multiset-indexed-dependent-products-of-types 11ms graph-theory.closed-walks-undirected-graphs 11ms higher-group-theory 10ms synthetic-homotopy-theory.category-of-connected-set-bundles-circle 10ms group-theory.isomorphisms-concrete-groups 10ms linear-algebra.scalar-multiplication-matrices 10ms graph-theory.acyclic-undirected-graphs 10ms 209,027,633,416 bytes allocated in the heap 20,208,785,744 bytes copied during GC 1,709,639,904 bytes maximum residency (28 sample(s)) 2,508,576 bytes maximum slop 3121 MiB total memory in use (0 MiB lost due to fragmentation) Tot time (elapsed) Avg pause Max pause Gen 0 48930 colls, 0 par 18.386s 19.088s 0.0004s 0.0485s Gen 1 28 colls, 0 par 0.691s 1.009s 0.0360s 0.2568s TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1) SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled) INIT time 0.001s ( 0.001s elapsed) MUT time 71.440s ( 71.424s elapsed) GC time 19.077s ( 20.097s elapsed) EXIT time 0.210s ( 0.002s elapsed) Total time 90.727s ( 91.525s elapsed) Alloc rate 2,925,929,451 bytes per MUT second Productivity 78.7% of total user, 78.0% of total elapsed ``` </details> --------- Co-authored-by: VojtechStep <[email protected]>
UniMath · Feb 22, 2024 · 071533a · 071533a
1 parent 208023d
commit 071533a
Show file tree

Hide file tree

Showing 8 changed files with 502 additions and 4 deletions.
diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
@@ -54,7 +54,7 @@ jobs:
             ${{ runner.os }}-check-${{ github.ref }}-${{ matrix.agda }}-
             ${{ runner.os }}-check-refs/heads/master-${{ matrix.agda }}-
 
-      - name: Typecheck the whole formalization
+      - name: Typecheck library
         run: |
           cd master
           make check

diff --git a/.github/workflows/clean-up.yaml b/.github/workflows/clean-up.yaml
@@ -1,4 +1,4 @@
-name: cleanup caches generated by pull requests
+name: Clean up caches generated by pull requests
 on:
   pull_request:
     types:

diff --git a/.github/workflows/pages.yaml b/.github/workflows/pages.yaml
@@ -1,4 +1,4 @@
-name: Formalization website
+name: Build and deploy library website
 on:
   # To run this workflow manually
   workflow_dispatch:

diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml
@@ -0,0 +1,76 @@
+name: Profile library typechecking
+on:
+  push:
+    branches:
+      - master
+
+# Don't cancel previous runs of the same branch
+concurrency:
+  group: '${{ github.workflow }}'
+  cancel-in-progress: false
+
+jobs:
+  typecheck-performance:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest]
+        agda: ['2.6.4']
+    steps:
+      - name: Checkout our repository
+        uses: actions/checkout@v3
+        with:
+          path: master
+
+      - name: Setup Agda
+        uses: wenkokke/[email protected]
+        with:
+          agda-version: ${{ matrix.agda }}
+
+      - name: Typecheck library with profiling
+        run: |
+          cd master
+          make check-profile 2> temp/memory-results.txt | tee temp/benchmark-results.txt
+
+      - name: Download previous typechecking profile
+        run: |
+          mkdir 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)
+          curl 'https://agda-unimath-benchmarks.netlify.app/data.csv' -o benchmark-cache/data.csv
+
+      - name: Process new profiling data
+        run: |
+          cd master
+          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: './master/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: Prepare new revision of the profiling website
+        run: |
+          cd master
+          mkdir 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
+
+      - name: Deploy the new profiling website
+        run: |
+          npx netlify-cli deploy --dir=benchmark-website
diff --git a/.gitignore b/.gitignore
@@ -423,6 +423,7 @@ package-lock.json
 docs/
 html/
 book/
+temp/
 src/temp/
 src/everything.lagda.md
 SUMMARY.md

diff --git a/Makefile b/Makefile
@@ -7,7 +7,7 @@
 everythingOpts := --guardedness --cohesion --flat-split
 # use "$ export AGDAVERBOSE=-v20" if you want to see all
 AGDAVERBOSE ?= -v1
-AGDARTS := +RTS -M4.0G -RTS
+AGDARTS := +RTS -M6.0G -RTS
 AGDAFILES := $(shell find src -name temp -prune -o -type f \( -name "*.lagda.md" -not -name "everything.lagda.md" \) -print)
 CONTRIBUTORS_FILE := CONTRIBUTORS.toml
 
@@ -20,6 +20,7 @@ CONTRIBUTORS_FILE := CONTRIBUTORS.toml
 # at is at least in a proper code block with syntax highlighting, albeit without
 # the agda-unimath chrome.
 AGDAHTMLFLAGS ?= --html --html-highlight=auto --html-dir=docs --css=website/css/Agda.css --only-scope-checking
+AGDAPROFILEFLAGS ?= --profile=modules +RTS -s -RTS
 AGDA ?= agda $(AGDAVERBOSE) $(AGDARTS)
 TIME ?= time
 
@@ -70,6 +71,10 @@ src/everything.lagda.md: agdaFiles
 check: ./src/everything.lagda.md
 	${TIME} ${AGDA} $?
 
+.PHONY: check-profile
+check-profile: ./src/everything.lagda.md
+	${AGDA} ${AGDAPROFILEFLAGS} $?
+
 agda-html: ./src/everything.lagda.md
 	@rm -rf ./docs/
 	@mkdir -p ./docs/

diff --git a/scripts/typechecking_profile_parser.py b/scripts/typechecking_profile_parser.py
@@ -0,0 +1,135 @@
+import json
+import re
+import argparse
+import csv
+
+
+def parse_memory_profiling_data(filepath):
+    results = dict()
+
+    # Define patterns to match each line and their corresponding unit
+    patterns = {
+        "memory_allocated_in_heap": (r"(\d+(?:,\d+)*) bytes allocated in the heap", "B"),
+        "memory_copied_during_GC": (r"(\d+(?:,\d+)*) bytes copied during GC", "B"),
+        "maximum_residency": (r"(\d+(?:,\d+)*) bytes maximum residency", "B"),
+        "memory_maximum_slop": (r"(\d+(?:,\d+)*) bytes maximum slop", "B"),
+        "total_memory_in_use": (r"(\d+) MiB total memory in use", "MiB")
+    }
+
+    with open(filepath, 'r') as file:
+        for line in file:
+            for key, (pattern, unit) in patterns.items():
+                match = re.search(pattern, line)
+                if match:
+                    value = int(match.group(1).replace(",", ""))
+                    if key == "memory_maximum_slop":  # Convert maximum slo to KiB and truncate
+                        value //= 1024
+                        unit = "KiB"
+                    elif unit == "B":  # Convert bytes to MiB and truncate
+                        value //= 1024 * 1024
+                        unit = "MiB"
+                    results[key] = {"value": value, "unit": unit}
+
+    return results
+
+def parse_benchmark_results(input_path):
+    benchmarks = dict()
+    with open(input_path, 'r') as file:
+        for line in file:
+            # Match lines that end with "ms" indicating a timing result
+            match = re.fullmatch(r'^\s*(\S+)\s+(\d+(?:,\d+)*)ms\s*$', line)
+            if match:
+                name = match.group(1).strip()
+                # Correctly parse and combine the number groups to handle commas in numbers
+                milliseconds = int(match.group(2).replace(',',''))
+                benchmarks[name] = {'value': milliseconds, 'unit':'ms'}
+    return benchmarks
+
+
+def subdict(original_dict, keys_to_extract):
+    if keys_to_extract is None:
+        return original_dict
+    else:
+        return {key: original_dict[key] for key in keys_to_extract if key in original_dict}
+
+def convert_dict_to_list(data, keys_to_extract=None):
+    return [{'name': name, **details} for name, details in subdict(data, keys_to_extract).items()]
+
+def save_github_action_benchmark_json(output_path, benchmarks, memory_stats, benchmark_keys, memory_keys):
+    with open(output_path, 'w') as file:
+        json.dump(convert_dict_to_list(benchmarks, benchmark_keys) + convert_dict_to_list(memory_stats, memory_keys) , file, indent=2)
+
+def read_existing_csv_to_dict(csv_path, commit_hash):
+    # Initialize a dictionary to hold the CSV data
+    data_dict = {}
+    fieldnames = ['name', 'unit', commit_hash]
+
+    try:
+        # Attempt to open the file, which will fail if the file doesn't exist
+        with open(csv_path, mode='r', newline='') as csvfile:
+            reader = csv.DictReader(csvfile)
+            # Update fieldnames with those found in the existing CSV, plus the new commit hash if necessary
+            fieldnames = reader.fieldnames + [commit_hash] if commit_hash not in reader.fieldnames else reader.fieldnames
+            for row in reader:
+                data_dict[row['name']] = row
+    except FileNotFoundError:
+        # File doesn't exist, proceed without modifying data_dict or fieldnames
+        pass
+
+    return data_dict, fieldnames
+
+def update_csv_data(data_dict, benchmarks, memory_stats, commit_hash):
+    # Combine benchmarks and memory stats for easier processing
+    combined_data = {**memory_stats, **benchmarks}
+
+    # Update the data_dict with new or updated values
+    for name, details in combined_data.items():
+        if name not in data_dict:
+            data_dict[name] = {'name': name, 'unit': details['unit']}
+        data_dict[name][commit_hash] = int(details['value'])
+
+def write_csv_from_dict(csv_path, data_dict, fieldnames, commit_hash):
+    def custom_sort(item):
+        # Sort all items that do not have unit "ms" first, then sort based on whether the name is capitalized, and then based on worst newest benchmark
+        is_not_ms_unit = item['unit'] != "ms"
+
+        if is_not_ms_unit:
+            # If the unit is not `ms`, preserve order
+            return (False, False, 0)
+        else:
+            # If the unit is `ms`, sort based on capitalization, then on newest benchmark
+            return (True , item['name'][0].islower(), 0 if commit_hash not in item.keys() else -item[commit_hash])
+
+
+
+    with open(csv_path, mode='w', newline='') as csvfile:
+        writer = csv.DictWriter(csvfile, fieldnames=fieldnames)
+        writer.writeheader()
+        # Sort the data based on the custom sort function before writing
+        sorted_data = sorted(data_dict.values(), key=custom_sort)
+        for row in sorted_data:
+            writer.writerow(row)
+
+def save_as_csv(benchmarks, memory_stats, csv_path, commit_hash):
+    data_dict, fieldnames = read_existing_csv_to_dict(csv_path, commit_hash)
+    update_csv_data(data_dict, benchmarks, memory_stats, commit_hash)
+    write_csv_from_dict(csv_path, data_dict, fieldnames, commit_hash)
+
+if __name__ == "__main__":
+    # Set up argument parsing
+    parser = argparse.ArgumentParser(description='Convert benchmark results to JSON format.')
+    parser.add_argument('input_times_path', help='Path to the input file containing typechecking times.')
+    parser.add_argument('input_memory_path', help='Path to the input file containing memory statistics.')
+    parser.add_argument('output_json_path', help='Path to the output JSON file.')
+    parser.add_argument('csv_path', help='Path to the profiling CSV file.')
+    parser.add_argument('commit_hash', help='Commit hash for current commit.')
+
+    # Parse arguments from command line
+    args = parser.parse_args()
+
+    # Use the provided command-line arguments
+    benchmarks = parse_benchmark_results(args.input_times_path)
+    memory_stats = parse_memory_profiling_data(args.input_memory_path)
+
+    save_github_action_benchmark_json(args.output_json_path, benchmarks, memory_stats, ["Total",], ["total_memory_in_use",])
+    save_as_csv(benchmarks, memory_stats, args.csv_path, args.commit_hash)
-Original file line number
+Diff line change
@@ Expand Up / @@ -423,6 +423,7 @@ package-lock.json @@
     docs/
     html/
     book/
+    temp/
     src/temp/
     src/everything.lagda.md
     SUMMARY.md
@@ Expand Down @@