Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Bench garagedoor april2 #1855

Closed
wants to merge 3 commits into from
Closed

Bench garagedoor april2 #1855

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9035901
move only_mmio_satisfying to bedrock2
andres-erbsen Apr 6, 2024
09290e8
more paperification of top-level spec details
andres-erbsen Apr 6, 2024
4100d67
[DO NOT MERGE] bench garagedoor
andres-erbsen Apr 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
164 changes: 2 additions & 162 deletions .github/workflows/coq-alpine.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,166 +42,6 @@ jobs:
- name: chroot build params
shell: alpine.sh {0}
run: etc/ci/describe-system-config.sh
- name: etc/ci/github-actions-make.sh deps
- name: bench garagedoor
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@v3
with:
name: standalone-${{ matrix.alpine }}
path: dist/fiat_crypto
# - name: upload standalone js files
# uses: actions/upload-artifact@v3
# with:
# name: standalone-html-${{ matrix.alpine }}
# path: fiat-html
- name: upload OCaml files
uses: actions/upload-artifact@v3
with:
name: ExtractionOCaml-${{ matrix.alpine }}
path: src/ExtractionOCaml
if: always ()
# - name: upload js_of_ocaml files
# uses: actions/upload-artifact@v3
# 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@v3
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@v3
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@v3
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@v3
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' }}
run: /usr/bin/time -v make -j src/Bedrock/End2End/X25519/GarageDoorTop.vo
146 changes: 2 additions & 144 deletions .github/workflows/coq-archlinux.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,147 +38,5 @@ jobs:
run: git config --global --add safe.directory "*"
- name: chroot build params
run: etc/ci/describe-system-config.sh
- name: make deps
run: etc/ci/github-actions-make.sh -j2 deps
- name: all-except-generated-and-js-of-ocaml
run: etc/ci/github-actions-make.sh -j2 all-except-generated-and-js-of-ocaml
- name: generated-files
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@v3
with:
name: generated-files-archlinux
path: generated-files.tgz
if: ${{ failure() }}
- name: install-standalone-unified-ocaml
run: etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist
#- name: standalone-js-of-ocaml
# run: etc/ci/github-actions-make.sh -j2 standalone-js-of-ocaml
#- name: install-standalone-js-of-ocaml
# run: etc/ci/github-actions-make.sh install-standalone-js-of-ocaml
- name: upload standalone files
uses: actions/upload-artifact@v3
with:
name: standalone-archlinux
path: dist/fiat_crypto
#- name: upload standalone js files
# uses: actions/upload-artifact@v3
# with:
# name: standalone-html-archlinux
# path: fiat-html
- name: upload OCaml files
uses: actions/upload-artifact@v3
with:
name: ExtractionOCaml-archlinux
path: src/ExtractionOCaml
if: always ()
#- name: upload js_of_ocaml files
# uses: actions/upload-artifact@v3
# with:
# name: ExtractionJsOfOCaml-archlinux
# path: src/ExtractionJsOfOCaml
# if: always ()
- name: standalone-haskell
run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS'
- name: upload Haskell files
uses: actions/upload-artifact@v3
with:
name: ExtractionHaskell-archlinux
path: src/ExtractionHaskell
if: always ()
- name: only-test-amd64-files-lite
run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1
- name: install
run: etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml
- name: install-without-bedrock2
run: etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml
- name: install-dev
run: etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml
- name: display timing info
run: cat time-of-build-pretty.log
- name: display per-line timing info
run: etc/ci/github-actions-display-per-line-timing.sh

test-standalone:
runs-on: ubuntu-latest
container: archlinux
needs: build
steps:
- name: Install system dependencies
run: |
pacman --noconfirm -Syu git --needed
- uses: actions/checkout@v4
- name: Download standalone archlinux
uses: actions/download-artifact@v3
with:
name: standalone-archlinux
path: dist/
- name: List files
run: find dist
- run: chmod +x dist/fiat_crypto
- name: Test files (container)
run: |
echo "::group::file fiat_crypto"
file dist/fiat_crypto
echo "::endgroup::"
echo "::group::ldd fiat_crypto"
ldd dist/fiat_crypto
echo "::endgroup::"
etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto

publish-standalone-dry-run:
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 archlinux
uses: actions/download-artifact@v3
with:
name: standalone-archlinux
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_archlinux_${arch}"
echo "$fname"
mv dist/fiat_crypto "dist/$fname"
find dist
# - 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' }}

archlinux-check-all:
runs-on: ubuntu-latest
needs: [build, test-standalone, publish-standalone-dry-run]
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-dry-run passed'
if: ${{ needs.publish-standalone-dry-run.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-dry-run failed' && false
if: ${{ needs.publish-standalone-dry-run.result != 'success' }}
- name: bench garagedoor
run: /usr/bin/time -v make -j src/Bedrock/End2End/X25519/GarageDoorTop.vo
Loading
Loading