[Develop] CI refactoring, test coverage data gathering (disabled for CI) and reports generation.

.config/nextest.toml

@@ -0,0 +1,139 @@
+# Copied from https://nexte.st/docs/configuration/
+
+# This is the default config used by nextest. It is embedded in the binary at
+# build time. It may be used as a template for .config/nextest.toml.
+
+[store]
+# The directory under the workspace root at which nextest-related files are
+# written. Profile-specific storage is currently written to dir/<profile-name>.
+dir = "target/nextest"
+
+# This section defines the default nextest profile. Custom profiles are layered
+# on top of the default profile.
+[profile.default]
+# "retries" defines the number of times a test should be retried. If set to a
+# non-zero value, tests that succeed on a subsequent attempt will be marked as
+# flaky. Can be overridden through the `--retries` option.
+# Examples
+# * retries = 3
+# * retries = { backoff = "fixed", count = 2, delay = "1s" }
+# * retries = { backoff = "exponential", count = 10, delay = "1s", jitter = true, max-delay = "10s" }
+retries = 0
+
+# The number of threads to run tests with. Supported values are either an
+# integer or the string "num-cpus". Can be overridden through the
+# `--test-threads` option.
+test-threads = "num-cpus"
+
+# The number of threads required for each test. This is generally used in
+# overrides to mark certain tests as heavier than others. However, it can also
+# be set as a global parameter.
+threads-required = 1
+
+# Show these test statuses in the output.
+#
+# The possible values this can take are:
+# * none: no output
+# * fail: show failed (including exec-failed) tests
+# * retry: show flaky and retried tests
+# * slow: show slow tests
+# * pass: show passed tests
+# * skip: show skipped tests (most useful for CI)
+# * all: all of the above
+#
+# Each value includes all the values above it; for example, "slow" includes
+# failed and retried tests.
+#
+# Can be overridden through the `--status-level` flag.
+status-level = "pass"
+
+# Similar to status-level, show these test statuses at the end of the run.
+final-status-level = "flaky"
+
+# "failure-output" defines when standard output and standard error for failing
+# tests are produced.
+# Accepted values are
+# * "immediate": output failures as soon as they happen
+# * "final": output failures at the end of the test run
+# * "immediate-final": output failures as soon as they happen and at the end of
+#   the test run; combination of "immediate" and "final"
+# * "never": don't output failures at all
+#
+# For large test suites and CI it is generally useful to use "immediate-final".
+#
+# Can be overridden through the `--failure-output` option.
+failure-output = "immediate"
+
+# "success-output" controls production of standard output and standard error on
+# success. This should generally be set to "never".
+success-output = "never"
+
+# Cancel the test run on the first failure. For CI runs, consider setting this
+# to false.
+fail-fast = true
+
+# Treat a test that takes longer than the configured 'period' as slow, and print
+# a message. See <https://nexte.st/book/slow-tests> for more information.
+#
+# Optional: specify the parameter 'terminate-after' with a non-zero integer,
+# which will cause slow tests to be terminated after the specified number of
+# periods have passed.
+# Example: slow-timeout = { period = "60s", terminate-after = 2 }
+slow-timeout = { period = "60s" }
+
+# Treat a test as leaky if after the process is shut down, standard output and
+# standard error aren't closed within this duration.
+#
+# This usually happens in case of a test that creates a child process and lets
+# it inherit those handles, but doesn't clean the child process up (especially
+# when it fails).
+#
+# See <https://nexte.st/book/leaky-tests> for more information.
+leak-timeout = "100ms"
+
+[profile.default.junit]
+# Output a JUnit report into the given file inside 'store.dir/<profile-name>'.
+# If unspecified, JUnit is not written out.
+
+# path = "junit.xml"
+
+# The name of the top-level "report" element in JUnit report. If aggregating
+# reports across different test runs, it may be useful to provide separate names
+# for each report.
+report-name = "nextest-run"
+
+# Whether standard output and standard error for passing tests should be stored
+# in the JUnit report.
+# Output is stored in the <system-out> and <system-err> elements of the
+# <testcase> element.
+store-success-output = false
+
+# Whether standard output and standard error for failing tests should be stored
+# in the JUnit report.
+# Output is stored in the <system-out> and <system-err> elements of the
+# <testcase> element.
+#
+# Note that if a description can be extracted from the output, it is always
+# stored in the <description> element.
+store-failure-output = true
+
+# This profile is activated if MIRI_SYSROOT is set.
+[profile.default-miri]
+
+[profile.ci]
+# Retrying at least twice in case it is a memory issue.
+retries = 2
+
+# Print out output for failing tests as soon as they fail, and also at the end
+# of the run (for easy scrollability).
+failure-output = "immediate-final"
+
+# The number of threads to run tests with. Supported values are either an integer or
+# the string "num-cpus". Can be overridden through the `--test-threads` option.
+test-threads = "num-cpus"
+
+[[profile.ci.overrides]]
+filter = "test(completeness)"
+threads-required = 2
+# The CI is slower. On a consumer laptop, completeness tests take up to 3m.
+slow-timeout = "5m"

.github/actions/codecov-shared/action.yml

@@ -0,0 +1,31 @@
+name: "Shared Codecov reporting steps"
+description: "Shared Codecov reporting steps"
+inputs:
+  token:
+    description: "Codecov token"
+    required: true
+  files:
+    description: "Files to upload to Codecov"
+    required: false
+    default: "./target/coverage/lcov.info"
+  flags:
+    description: "Flags to pass to Codecov"
+    required: false
+    default: ""
+  name:
+    description: "The report name"
+    required: false
+    default: "proof-systems"
+runs:
+  using: "composite"
+  steps:
+    - name: Upload coverage reports to Codecov
+      uses: codecov/codecov-action@v4
+      with:
+        token: ${{ inputs.token }}
+        files: ${{ inputs.files }}
+        flags: ${{ inputs.flags }}
+        name: ${{ inputs.name }}
+        verbose: true
+        handle_no_reports_found: true
+        fail_ci_if_error: false

.github/actions/coverage-summary-shared/action.yml

@@ -0,0 +1,32 @@
+name: "Shared code coverage summary"
+description: "Shared code coverage summary"
+inputs:
+  html_file:
+    description: "HTML file with the coverage report"
+    required: false
+    default: "target/coverage/index.html"
+  shell:
+    description: "Shell to use"
+    required: false
+    default: "bash"
+runs:
+  using: "composite"
+  steps:
+    - name: Add test coverage summary
+      run: |
+        echo "### Test coverage summary" >> $GITHUB_STEP_SUMMARY
+        # Define the HTML file
+        html_file="${{ inputs.html_file }}"
+        # Extract data for Lines, Functions, and Branches using `sed`
+        lines=$(sed -n '/heading">Lines/{n;n;s/.*<abbr [^>]*>\(.*%\)<\/abbr>.*/\1/p;}' "$html_file")
+        functions=$(sed -n '/heading">Functions/{n;n;s/.*<abbr [^>]*>\(.*%\)<\/abbr>.*/\1/p;}' "$html_file")
+        branches=$(sed -n '/heading">Branches/{n;n;s/.*<abbr [^>]*>\(.*%\)<\/abbr>.*/\1/p;}' "$html_file")
+        # Compose Markdown summary table
+        echo "" >> $GITHUB_STEP_SUMMARY
+        echo "| Metric    | Coverage |" >> $GITHUB_STEP_SUMMARY
+        echo "|-----------|----------|" >> $GITHUB_STEP_SUMMARY
+        echo "| Lines     | $lines |" >> $GITHUB_STEP_SUMMARY
+        echo "| Functions | $functions |" >> $GITHUB_STEP_SUMMARY
+        echo "| Branches  | $branches |" >> $GITHUB_STEP_SUMMARY
+        echo "" >> $GITHUB_STEP_SUMMARY
+      shell: ${{ inputs.shell }}

.github/actions/ocaml-shared/action.yml

@@ -0,0 +1,15 @@
+name: "Shared OCaml setting up steps"
+description: "Shared OCaml setting up steps"
+inputs:
+  ocaml_version:
+    description: "OCaml version"
+    required: true
+runs:
+  using: "composite"
+  steps:
+    - name: Setup OCaml ${{ inputs.ocaml_version }}
+      uses: ocaml/setup-ocaml@v3
+      with:
+        ocaml-compiler: ${{ inputs.ocaml_version }}
+        # https://github.com/ocaml/setup-ocaml/issues/211#issuecomment-1058882386
+        # disable-cache: true

.github/actions/toolchain-shared/action.yml

@@ -0,0 +1,26 @@
+name: "Shared Rust toolchain setting up steps"
+description: "Shared Rust toolchain setting up steps"
+inputs:
+  rust_toolchain_version:
+    description: "Rust toolchain version"
+    required: true
+  shell:
+    description: "Shell to use"
+    required: false
+    default: "bash"
+runs:
+  using: "composite"
+  steps:
+    # As action-rs does not seem to be maintained anymore, building from
+    # scratch the environment using rustup
+    - name: Setup Rust toolchain ${{ inputs.rust_toolchain_version }}
+      run: |
+        curl --proto '=https' --tlsv1.2 -sSf -o rustup-init \
+        https://static.rust-lang.org/rustup/dist/x86_64-unknown-linux-gnu/rustup-init
+        chmod +x ./rustup-init
+        ./rustup-init -y --default-toolchain "${{ inputs.rust_toolchain_version }}" --profile default
+        rm ./rustup-init
+        echo "$HOME/.cargo/bin" >> $GITHUB_PATH
+        # overwriting default rust-toolchain
+        echo ${{ inputs.rust_toolchain_version }} > rust-toolchain
+      shell: ${{ inputs.shell }}

.github/workflows/benches.yml

@@ -9,47 +9,37 @@ env:
   OCAML_VERSION: "4.14.0"
   RUST_TOOLCHAIN_VERSION: "1.71"
 
-
 jobs:
   bench:
     runs-on: ubuntu-latest
     name: Run benchmarks
     if: github.event.label.name == 'benchmark'
     steps:
-      - name: Checkout PR
-        uses: actions/checkout@v4.1.1
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
 
-      # as action-rs does not seem to be maintained anymore, building from
-      # scratch the environment using rustup
-      - name: Setup Rust toolchain $RUST_TOOLCHAIN_VERSION
-        run:
-          |
-            curl --proto '=https' --tlsv1.2 -sSf -o rustup-init \
-            https://static.rust-lang.org/rustup/dist/x86_64-unknown-linux-gnu/rustup-init
-            chmod +x ./rustup-init
-            ./rustup-init -y --default-toolchain "$RUST_TOOLCHAIN_VERSION" --profile default
-            rm ./rustup-init
-            echo "$HOME/.cargo/bin" >> $GITHUB_PATH
-            # overwriting default rust-toolchain
-            echo $RUST_TOOLCHAIN_VERSION > rust-toolchain
+      - name: Use shared Rust toolchain setting up steps
+        uses: ./.github/actions/toolchain-shared
+        with:
+          rust_toolchain_version: ${{ env.RUST_TOOLCHAIN_VERSION }}
 
       - name: Install dependencies
         run: |
           set -x
-          cargo install cargo-criterion   # criterion
+          cargo install cargo-criterion
 
-      - name: Setup OCaml ${{ env.OCAML_VERSION }}
-        uses: ocaml/setup-ocaml@v2
+      - name: Use shared OCaml setting up steps
+        uses: ./.github/actions/ocaml-shared
         with:
-          ocaml-compiler: ${{ env.OCAML_VERSION }}
-          # https://github.com/ocaml/setup-ocaml/issues/211#issuecomment-1058882386
-          # disable-cache: true
+          ocaml_version: ${{ env.OCAML_VERSION }}
 
-#      - name: Run iai bench
-#        run: |
-#          set -x
-#          cargo bench -p kimchi --bench proof_iai > iai_bench
-#          cat iai_bench
+      #      - name: Run iai bench
+      #        run: |
+      #          set -x
+      #          cargo bench -p kimchi --bench proof_iai > iai_bench
+      #          cat iai_bench
 
       - name: Run criterion bench
         run: |
@@ -59,7 +49,7 @@ jobs:
           cat criterion_bench
 
       - name: Write result in PR
-        uses: actions/github-script@v5
+        uses: actions/github-script@v7
         with:
           script: |
             const fs = require('fs');

.github/workflows/ci-nightly.yml

@@ -0,0 +1,74 @@
+#
+# This workflow is triggered by scheduler or on-demand to run all the tests with the code coverage enabled and using the self-hosted GitHub runner.
+# Test coverage report is attached to the current job execution results in a form of Zip archive.
+#
+
+name: Nightly tests with the code coverage
+
+on:
+  schedule:
+    - cron: "0 0 * * *" # every day at midnight
+  workflow_dispatch: {}
+
+env:
+  # https://doc.rust-lang.org/cargo/reference/profiles.html#release
+  RUSTFLAGS: -Coverflow-checks=y -Cdebug-assertions=y
+  # https://doc.rust-lang.org/cargo/reference/profiles.html#incremental
+  CARGO_INCREMENTAL: 1
+  # https://nexte.st/book/pre-built-binaries.html#using-nextest-in-github-actions
+  CARGO_TERM_COLOR: always
+  # 30 MB of stack for Keccak tests
+  RUST_MIN_STACK: 31457280
+
+jobs:
+  run_tests:
+    name: Run all tests with the code coverage
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        rust_toolchain_version: ["1.74"]
+        # FIXME: currently not available for 5.0.0.
+        # It might be related to boxroot dependency, and we would need to bump
+        # up the ocaml-rs dependency
+        ocaml_version: ["4.14"]
+        os: ["hetzner-1"]
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Use shared Rust toolchain setting up steps
+        uses: ./.github/actions/toolchain-shared
+        with:
+          rust_toolchain_version: ${{ matrix.rust_toolchain_version }}
+
+      - name: Use shared OCaml setting up steps
+        uses: ./.github/actions/ocaml-shared
+        with:
+          ocaml_version: ${{ matrix.ocaml_version }}
+
+      - name: Install test dependencies
+        run: |
+          make install-test-deps
+
+      - name: Run all tests with the code coverage
+        run: |
+          eval $(opam env)
+          make clean
+          make nextest-all-with-coverage
+          make test-doc-with-coverage
+          make generate-test-coverage-report
+
+      - name: Use shared code coverage summary
+        uses: ./.github/actions/coverage-summary-shared
+
+      - name: Upload the HTML test coverage report
+        uses: actions/upload-artifact@v4
+        continue-on-error: true
+        if: always()
+        with:
+          if-no-files-found: ignore
+          name: test-coverage-html-report-${{ matrix.rust_toolchain_version }}-${{ matrix.os }}
+          path: target/coverage/
+          retention-days: 30