Skip to content

Bump rewriter from edd0611 to 8ab716a #820

Bump rewriter from edd0611 to 8ab716a

Bump rewriter from edd0611 to 8ab716a #820

Workflow file for this run

name: CI (Coq, Alpine)
on:
push:
branches: [ master ]
pull_request:
merge_group:
workflow_dispatch:
release:
types: [published]
schedule:
- cron: '0 0 1 * *'
jobs:
build:
strategy:
fail-fast: false
matrix:
include:
- alpine: 'edge'
# - alpine: 'latest-stable'
runs-on: ubuntu-latest
name: alpine-${{ matrix.alpine }}
concurrency:
group: ${{ github.workflow }}-alpine-${{ matrix.alpine }}-${{ github.head_ref || github.run_id }}
cancel-in-progress: true
steps:
- uses: actions/checkout@v4
with:
submodules: recursive
- uses: jirutka/setup-alpine@v1
with:
branch: ${{ matrix.alpine }}
extra-repositories: https://dl-cdn.alpinelinux.org/alpine/edge/testing
packages: git make jq gcc musl-dev python3 ocaml ocaml-findlib ghc cabal coq ocaml-zarith bash sudo
- name: host build params
run: etc/ci/describe-system-config.sh
- name: chroot build params
shell: alpine.sh {0}
run: etc/ci/describe-system-config.sh
- name: etc/ci/github-actions-make.sh deps
shell: alpine.sh {0}
run: etc/ci/github-actions-make.sh -j2 deps
- name: all-except-generated-and-js-of-ocaml
shell: alpine.sh {0}
run: etc/ci/github-actions-make.sh -j2 CAMLEXTRAFLAGS="-ccopt -static" all-except-generated-and-js-of-ocaml
- name: install-standalone-unified-ocaml
shell: alpine.sh {0}
run: make install-standalone-unified-ocaml BINDIR=dist
# - name: install-standalone-js-of-ocaml
# shell: alpine.sh {0}
# run: make install-standalone-js-of-ocaml
- name: upload standalone files
uses: actions/upload-artifact@v4
with:
name: standalone-${{ matrix.alpine }}
path: dist/fiat_crypto
# - name: upload standalone js files
# uses: actions/upload-artifact@v4
# with:
# name: standalone-html-${{ matrix.alpine }}
# path: fiat-html
- name: upload OCaml files
uses: actions/upload-artifact@v4
with:
name: ExtractionOCaml-${{ matrix.alpine }}
path: src/ExtractionOCaml
if: always ()
# - name: upload js_of_ocaml files
# uses: actions/upload-artifact@v4
# with:
# name: ExtractionJsOfOCaml-${{ matrix.alpine }}
# path: src/ExtractionJsOfOCaml
# if: always ()
- name: generated-files
shell: alpine.sh {0}
run: etc/ci/github-actions-make.sh -j2 generated-files
- run: tar -czvf generated-files.tgz fiat-*/
if: ${{ failure() }}
- name: upload generated files
uses: actions/upload-artifact@v4
with:
name: generated-files-${{ matrix.alpine }}
path: generated-files.tgz
if: ${{ failure() }}
- name: standalone-haskell
shell: alpine.sh {0}
run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS'
- name: upload Haskell files
uses: actions/upload-artifact@v4
with:
name: ExtractionHaskell-${{ matrix.alpine }}
path: src/ExtractionHaskell
if: always ()
- name: only-test-amd64-files-lite
shell: alpine.sh {0}
run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1
- name: install
shell: alpine.sh {0}
run: sudo make EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml
- name: install-without-bedrock2
shell: alpine.sh {0}
run: sudo make EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml
- name: install-dev
shell: alpine.sh {0}
run: sudo make EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml
- name: display timing info
run: cat time-of-build-pretty.log || true
- name: display per-line timing info
run: etc/ci/github-actions-display-per-line-timing.sh
test-standalone:
strategy:
fail-fast: false
matrix:
include:
- alpine: 'edge'
# - alpine: 'latest-stable'
runs-on: ubuntu-latest
name: test-standalone-${{ matrix.alpine }}
needs: build
steps:
- uses: actions/checkout@v4
- name: Download standalone ${{ matrix.alpine }}
uses: actions/download-artifact@v4
with:
name: standalone-${{ matrix.alpine }}
path: dist/
- name: List files
run: find dist
- run: chmod +x dist/fiat_crypto
- name: Test files (host)
run: |
echo "::group::file fiat_crypto"
file dist/fiat_crypto
echo "::endgroup::"
echo "::group::ldd fiat_crypto"
ldd dist/fiat_crypto || true
echo "::endgroup::"
etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto
- uses: jirutka/setup-alpine@v1
with:
branch: ${{ matrix.alpine }}
extra-repositories: https://dl-cdn.alpinelinux.org/alpine/edge/testing
- name: Test files (container)
shell: alpine.sh {0}
run: etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto
publish-standalone:
runs-on: ubuntu-latest
needs: build
permissions:
contents: write # IMPORTANT: mandatory for making GitHub Releases
steps:
- uses: actions/checkout@v4
with:
fetch-depth: 0 # Fetch all history for all tags and branches
tags: true # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version
- name: Download standalone edge
uses: actions/download-artifact@v4
with:
name: standalone-edge
path: dist/
- name: List files
run: find dist
- name: Rename files
run: |
echo "::group::find arch"
arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")"
tag="$(git describe --tags HEAD)"
fname="Fiat-Cryptography_${tag}_Linux_${arch}"
echo "$fname"
mv dist/fiat_crypto "dist/$fname"
find dist
file "dist/$fname"
- name: Upload artifacts to GitHub Release
env:
GITHUB_TOKEN: ${{ github.token }}
# Upload to GitHub Release using the `gh` CLI.
# `dist/` contains the built packages
run: >-
gh release upload
'${{ github.ref_name }}' dist/**
--repo '${{ github.repository }}'
if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }}
alpine-check-all:
runs-on: ubuntu-latest
needs: [build, test-standalone, publish-standalone]
if: always()
steps:
- run: echo 'build passed'
if: ${{ needs.build.result == 'success' }}
- run: echo 'test-standalone passed'
if: ${{ needs.test-standalone.result == 'success' }}
- run: echo 'publish-standalone passed'
if: ${{ needs.publish-standalone.result == 'success' }}
- run: echo 'build failed' && false
if: ${{ needs.build.result != 'success' }}
- run: echo 'test-standalone failed' && false
if: ${{ needs.test-standalone.result != 'success' }}
- run: echo 'publish-standalone failed' && false
if: ${{ needs.publish-standalone.result != 'success' }}