Update coq-windows.yml to echo build params better hopefully #4735
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
name: Test Generated C | |
on: | |
push: | |
pull_request: | |
merge_group: | |
schedule: | |
- cron: '0 0 1 * *' | |
jobs: | |
test-c: | |
runs-on: ubuntu-latest | |
concurrency: | |
group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }} | |
cancel-in-progress: true | |
steps: | |
- uses: actions/checkout@v4 | |
with: | |
submodules: recursive | |
- name: install gcc | |
run: | | |
sudo sed -i 's/azure\.//' /etc/apt/sources.list | |
sudo apt-get -o Acquire::Retries=30 update -q | |
sudo apt-get -o Acquire::Retries=30 install -y --allow-unauthenticated \ | |
g++ libssl-dev \ | |
ninja-build libunwind-dev cmake | |
#sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-7 60 --slave /usr/bin/g++ g++ /usr/bin/g++-7 | |
- name: GCC Problem Matcher | |
uses: ammaraskar/[email protected] | |
- name: Set up Go | |
uses: actions/setup-go@v4 | |
id: go | |
- name: make only-test-c-files CC=gcc | |
run: make only-test-c-files CC=gcc EXTERNAL_DEPENDENCIES=1 | |
- name: make only-test-bedrock2-files CC=gcc | |
run: make only-test-bedrock2-files CC=gcc EXTERNAL_DEPENDENCIES=1 | |
- name: BoringSSL C test | |
run: EXTRA_CFLAGS="" etc/ci/test-fiat-c-boringssl.sh fiat-c/src | |
- name: BoringSSL bedrock2 test | |
run: EXTRA_CFLAGS="$(make bedrock2-extra-cflags SKIP_INCLUDE=1 2>/dev/null)" etc/ci/test-fiat-c-boringssl.sh fiat-bedrock2/src |