-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
3 changed files
with
120 additions
and
56 deletions.
There are no files selected for viewing
This file was deleted.
Oops, something went wrong.
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,63 @@ | ||
name: High-Level (Coordinating) Workflow Continuous Integration EasyCrypt Projects | ||
run-name: ${{ format('Branch "{0}" | Execute test "{1}" (in file "{2}") | See details for EasyCrypt version/branch.', github.ref_name, github.event.inputs.test-name || vars.DEFAULT_TEST_NAME, github.event.inputs.test-file || vars.DEFAULT_TEST_FILE) }} | ||
|
||
on: | ||
# Always trigger on push and pull request to any branch. | ||
# Checks related to executing branch/triggering event are delegated to jobs themselves. | ||
# (Reason for this is that we cannot access contexts in on.push and on.pull_request.) | ||
push: | ||
pull_request: | ||
# Enable manual execution of jobs (possibly with non-default configuration). | ||
workflow_dispatch: | ||
inputs: | ||
ec-branch: | ||
description: Branch (in EasyCrypt repository) | ||
type: string | ||
test-file: | ||
description: Test configuration file location | ||
type: string | ||
test-name: | ||
description: Test name | ||
type: string | ||
|
||
jobs: | ||
# Manually executed jobs (possibly with non-default configuration) | ||
check-custom: | ||
if: ${{ github.event_name == 'workflow_dispatch' }} | ||
uses: ./.github/workflows/ec-ci-ll.yml | ||
with: # If custom configuration manually specified, use that; else, use default configuration (defined in repository variables). | ||
ec-branch: ${{ github.event.inputs.ec-branch || vars.DEFAULT_EC_BRANCH }} | ||
test-file: ${{ github.event.inputs.test-file || vars.DEFAULT_TEST_FILE }} | ||
test-name: ${{ github.event.inputs.test-name || vars.DEFAULT_TEST_NAME }} | ||
# Automatically executed job (on any push or pull request) for the default branch. | ||
check-default: | ||
if: ${{ github.event_name != 'workflow_dispatch' && github.ref_name == github.event.repository.default_branch }} | ||
uses: ./.github/workflows/ec-ci-ll.yml | ||
with: # Use default configuration (defined in repository variables). | ||
ec-branch: ${{ vars.DEFAULT_EC_BRANCH }} | ||
test-file: ${{ vars.DEFAULT_TEST_FILE }} | ||
test-name: ${{ vars.DEFAULT_TEST_NAME }} | ||
# Preprocessing step for check-merge-x job: Extracts 'x' from 'merge-x'. | ||
preprocess-merge-x: | ||
if: ${{ github.event_name != 'workflow_dispatch' && startsWith(github.ref_name, 'merge-') }} | ||
runs-on: ubuntu-latest | ||
outputs: | ||
extracted-branch: ${{ steps.extract-branch.outputs.extracted-branch }} | ||
steps: | ||
- id: extract-branch | ||
run: | | ||
BRANCH=${{ github.ref_name }} | ||
echo "extracted-branch=${BRANCH#merge-}" >> "$GITHUB_OUTPUT" | ||
# Automatically executed job (on any push or pull request) for any merge-x branch. | ||
check-merge-x: | ||
if: ${{ github.event_name != 'workflow_dispatch' && startsWith(github.ref_name, 'merge-') }} | ||
needs: preprocess-merge-x | ||
uses: ./.github/workflows/ec-ci-ll.yml | ||
with: | ||
# Use 'x' (extracted from 'merge-x' by preprocess-merge-x) for the EasyCrypt branch. | ||
# Use default configuration (defined in repository variables) for the remainder. | ||
ec-branch: ${{ needs.preprocess-merge-x.outputs.extracted-branch }} | ||
test-file: ${{ vars.DEFAULT_TEST_FILE }} | ||
test-name: ${{ vars.DEFAULT_TEST_NAME }} | ||
|
||
|
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,57 @@ | ||
name: Low-Level Reusable Workflow Continuous Integration EasyCrypt Projects | ||
|
||
on: | ||
workflow_call: | ||
inputs: | ||
ec-branch: | ||
description: Branch (in EasyCrypt repository) | ||
required: true | ||
type: string | ||
test-file: | ||
description: Test configuration file location | ||
required: true | ||
type: string | ||
test-name: | ||
description: Test name | ||
required: true | ||
type: string | ||
|
||
env: | ||
OPAMROOT: /home/charlie/.opam | ||
OPAMYES: true | ||
OPAMJOBS: 2 | ||
ECRJOBS: 1 | ||
|
||
jobs: | ||
default: | ||
runs-on: ubuntu-20.04 | ||
container: | ||
image: ghcr.io/easycrypt/ec-build-box | ||
steps: | ||
- uses: actions/checkout@v4 | ||
name: Initialize submodules (if any) | ||
with: | ||
submodules: recursive | ||
- uses: actions/checkout@v4 | ||
name: Checkout EasyCrypt | ||
with: | ||
repository: EasyCrypt/easycrypt | ||
ref: ${{ format('refs/heads/{0}', inputs.ec-branch) }} | ||
path: easycrypt | ||
- name: Update OPAM and EasyCrypt dependencies | ||
run: | | ||
opam update | ||
opam pin add -n easycrypt easycrypt | ||
opam install --deps-only easycrypt | ||
- name: Install EasyCrypt | ||
run: opam install easycrypt | ||
- name: Configure SMT provers | ||
run: opam config exec -- easycrypt why3config -why3 ~/.why3.conf | ||
- name: Check project | ||
run: ${{ format('opam config exec -- easycrypt runtest -report report.log -raw-args -gcstats {0} {1}', inputs.test-file, inputs.test-name) }} | ||
- uses: actions/upload-artifact@v4 | ||
name: Upload report | ||
with: | ||
name: report.log | ||
path: report.log | ||
if-no-files-found: ignore |