Build

Bump actions/upload-artifact from 3 to 4 #624

Workflow file for this run

	name: Build
	on:
	push:
	branches:
	- 'master'
	paths-ignore:
	- '**.md'
	- '**.gitignore'
	- '**.opam'
	- '**.editorconfig'
	- 'LICENSE'
	- 'papers/**'
	- 'extra/docker/**'
	pull_request:
	paths-ignore:
	- '**.md'
	- '**.gitignore'
	- '**.opam'
	- '**.editorconfig'
	- 'LICENSE'
	- 'papers/**'
	- 'extra/docker/**'
	permissions:
	contents: read
	env:
	OCAML_COMILER_VERSION: "4.13.1"
	JOBS: 2
	jobs:
	build:
	runs-on: ubuntu-latest
	permissions:
	contents: write
	steps:
	- name: Checkout branch ${{ github.ref_name }}
	uses: actions/checkout@v4

	- run: sudo apt-get update
	- name: Restore opam cache
	id: opam-cache
	uses: actions/cache@v3
	with:
	path: "~/.opam"
	key: opam-${{env.OCAML_COMILER_VERSION}}-${{hashFiles('.github/coq-concert.opam.locked')}}
	restore-keys: \|
	opam-${{env.OCAML_COMILER_VERSION}}-

	- name: Set up OCaml
	uses: avsm/setup-ocaml@v1
	with:
	ocaml-version: ${{env.OCAML_COMILER_VERSION}}

	- name: Build dependencies
	#if: ${{ !steps.opam-cache.outputs.cache-hit }}
	run: \|
	opam repo add coq-released https://coq.inria.fr/opam/released
	opam install --deps-only -j${{ env.JOBS }} .github/coq-concert.opam.locked
	opam install -y -j${{ env.JOBS }} coq-dpdgraph
	opam clean -a -c -s --logs

	- name: Set up environment
	run: \|
	echo "::group::Setting up problem matcher"
	echo "::add-matcher::./.github/coq-errors.json"
	echo "::endgroup::"

	- name: Build core
	run: \|
	echo "::group::Build utilities"
	opam exec -- make -j${{ env.JOBS }} utils
	echo "::endgroup::"

	echo "::group::Build execution layer"
	opam exec -- make -j${{ env.JOBS }} execution
	echo "::endgroup::"

	echo "::group::Build embedding layer"
	opam exec -- make -j${{ env.JOBS }} embedding
	echo "::endgroup::"

	echo "::group::Build extraction layer"
	opam exec -- make -j${{ env.JOBS }} extraction
	echo "::endgroup::"

	- name: Build examples
	run: \|
	echo "::group::Build examples"
	opam exec -- make -j${{ env.JOBS }} examples
	echo "::endgroup::"

	- name: Set up Rust
	uses: actions-rs/toolchain@v1
	with:
	toolchain: 1.69.0
	target: wasm32-unknown-unknown
	- name: Set up Concordium tools
	run: \|
	curl -L -O https://distribution.concordium.software/tools/linux/cargo-concordium_1.0.0
	sudo chmod +x cargo-concordium_1.0.0
	sudo mv cargo-concordium_1.0.0 /usr/local/bin/cargo-concordium

	- name: Set up LIGO v0.59.0
	run: \|
	curl -L -O https://gitlab.com/ligolang/ligo/-/jobs/3553205311/artifacts/raw/ligo
	sudo chmod +x ./ligo
	sudo mv ligo /usr/local/bin/

	- name: Set up Liquidity
	run: \|
	sudo chmod +x ./extra/docker/liquidity
	sudo mv extra/docker/liquidity /usr/local/bin/

	- name: Test extraction
	run: \|
	echo "::group::Running tests"
	make -j${{ env.JOBS }} test-extraction
	echo "::endgroup::"

	- name: Upload Liquidity extraction logs
	if: false # Do we still want these logs?
	uses: actions/upload-artifact@v4
	with:
	name: Liquidity logs
	path: extraction/tests/extracted-code/liquidity-extract/liquidity.log
	retention-days: 14

	- name: Prepare extraction results
	if: github.event_name == 'push' && github.repository == 'AU-COBRA/ConCert' && github.ref == 'refs/heads/master'
	run: \|
	echo "::group::Cleaning up extracted code"
	make -j${{ env.JOBS }} clean-extraction-out-files
	make -j${{ env.JOBS }} clean-compiled-extraction
	find extraction/tests/extracted-code -name 'placeholder' -delete
	echo "::endgroup::"

	cp LICENSE extraction/tests/extracted-code/LICENSE
	cp extra/extraction-results.md extraction/tests/extracted-code/README.md
	cp .gitattributes extraction/tests/extracted-code/.gitattributes

	- name: Push to the extraction results repository
	# don't push the extraction results on pull requests and push only from the master branch of the AU-COBRA/ConCert repo.
	if: github.event_name == 'push' && github.repository == 'AU-COBRA/ConCert' && github.ref == 'refs/heads/master'
	uses: cpina/github-action-push-to-another-repository@main
	env:
	SSH_DEPLOY_KEY: ${{ secrets.EXTRACTION_RESULTS_DEPLOY_KEY }}
	with:
	source-directory: 'extraction/tests/extracted-code'
	destination-github-username: 'AU-COBRA'
	destination-repository-name: 'extraction-results'
	user-email: [email protected]
	commit-message: See ORIGIN_COMMIT from $GITHUB_REF
	target-branch: master

	- name: Build documentation
	if: github.event_name == 'push' && github.ref == 'refs/heads/master'
	run: \|
	echo "::group::Running coqdoc"
	opam exec -- make -j${{ env.JOBS }} html
	echo "::endgroup::"

	echo "::group::Install dependencies"
	sudo apt install -y graphviz
	echo "::endgroup::"

	echo "::group::Generate dependency graphs"
	rm -rf docs/graphs
	mkdir -p docs
	mkdir -p docs/graphs

	opam exec -- make dependency-graphs
	mv utils/svg/* docs/graphs/
	mv execution/svg/* docs/graphs/
	mv embedding/svg/* docs/graphs/
	mv extraction/svg/* docs/graphs/
	mv examples/svg/* docs/graphs/
	echo "::endgroup::"

	- name: Prepare documentation for deployment
	if: github.event_name == 'push' && github.ref == 'refs/heads/master'
	uses: actions/upload-pages-artifact@v2
	with:
	path: docs

	deploy-docs:
	if: github.event_name == 'push' && github.ref == 'refs/heads/master'
	needs: build
	runs-on: ubuntu-latest
	permissions:
	pages: write
	id-token: write
	environment:
	name: github-pages
	url: ${{ steps.deployment.outputs.page_url }}
	steps:
	- name: Deploy to GitHub Pages
	id: deployment
	uses: actions/deploy-pages@v3

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Bump actions/upload-artifact from 3 to 4 #624

Workflow file

Bump actions/upload-artifact from 3 to 4 #624

Jobs

Run details

Workflow file for this run