Defining properties of maxima and minima, lemmas for the take operation in lists, lists from sequences. #3252

Workflow file for this run

	name: CI

	on: [ push , pull_request , merge_group ]

	concurrency:
	group: "${{ github.workflow }} @ ${{ github.event.pull_request.head.label \|\| github.head_ref \|\| github.ref }}"
	cancel-in-progress: true

	# We set the supported coq-version from here. In order to use this environment variable correctly, look at how they are used in the following jobs.
	env:
	coq-version-supported: '8.19'
	ocaml-version: '4.14-flambda'
	deployment-branch: 'gh-pages'

	# Our jobs come in 3 stages, the latter stages depending on the former:
	# - Stage 1: Build jobs
	# - Stage 2: Documentation and validation jobs
	# - Stage 3: Deployment job
	# - Stage 4: Clean-up job

	jobs:

	#
	# Stage 1:
	#

	# Here we define the build jobs:
	# - opam-build: Building the library using opam
	# - quick-build: Building the library quickly using make
	# - build: Building with timeing information for use in doc jobs

	# Building the library using opam
	opam-build:
	strategy:
	fail-fast: false
	matrix:
	coq-version-dummy:
	- 'supported'
	- 'latest'
	- 'dev'
	os:
	- ubuntu-latest
	env:
	coq-version: ${{ matrix.coq-version-dummy }}
	runs-on: ${{ matrix.os }}
	steps:
	# Github actions doesn't let us set workflow level enviornment variables inside the stategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment varible env.coq-version, which uses the globablly set coq-version-supported when running the 'supported' case.
	- name: Set supported coq-version
	if: matrix.coq-version-dummy == 'supported'
	run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV

	- name: Checkout repo
	uses: actions/checkout@v4
	- name: Build HoTT
	uses: coq-community/docker-coq-action@v1
	with:
	opam_file: 'coq-hott.opam'
	coq_version: ${{ env.coq-version }}
	ocaml_version: ${{ env.ocaml-version }}
	export: 'OPAMWITHTEST'
	env:
	OPAMWITHTEST: 'true'

	# Quick build
	quick-build:
	strategy:
	fail-fast: false
	matrix:
	coq-version-dummy:
	- 'supported'
	- 'latest'
	- 'dev'
	os:
	- ubuntu-latest
	env:
	coq-version: ${{ matrix.coq-version-dummy }}
	runs-on: ${{ matrix.os }}
	steps:
	# Github actions doesn't let us set workflow level enviornment variables inside the stategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment varible env.coq-version, which uses the globablly set coq-version-supported when running the 'supported' case.
	- name: Set supported coq-version
	if: matrix.coq-version-dummy == 'supported'
	run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
	- name: Checkout repo
	uses: actions/checkout@v4
	- name: Build HoTT
	uses: coq-community/docker-coq-action@v1
	with:
	coq_version: ${{ env.coq-version }}
	ocaml_version: ${{ env.ocaml-version }}
	custom_script: \|
	startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
	sudo chown -R coq:coq .
	endGroup
	echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
	make -j2
	- name: Revert permissions
	# to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
	if: ${{ always() }}
	run: sudo chown -R 1001:116 .

	# Main build which docs will run off
	build:
	strategy:
	fail-fast: false
	matrix:
	# We build on our supported version of coq and the master version
	coq-version-dummy:
	- 'supported'
	- 'latest'
	include:
	- coq-version-dummy: 'dev'
	extra-gh-reportify: '--warnings'
	env:
	coq-version: ${{ matrix.coq-version-dummy }}
	runs-on: ubuntu-latest
	steps:
	# Github actions doesn't let us set workflow level enviornment variables inside the stategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment varible env.coq-version, which uses the globablly set coq-version-supported when running the 'supported' case.
	- name: Set supported coq-version
	if: matrix.coq-version-dummy == 'supported'
	run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
	# Checkout branch
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	# We use the coq docker so we don't have to build coq
	- uses: coq-community/docker-coq-action@v1
	with:
	coq_version: ${{ env.coq-version }}
	ocaml_version: ${{ env.ocaml-version }}
	custom_script: \|
	startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
	sudo chown -R coq:coq .
	endGroup
	echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
	sudo apt-get -o Acquire::Retries=30 update -q
	sudo apt-get -o Acquire::Retries=30 install python3 python-is-python3 -y --allow-unauthenticated
	etc/coq-scripts/github/reportify-coq.sh --errors ${{ matrix.extra-gh-reportify }} make TIMED=1 -j2 --output-sync

	- name: Revert permissions
	# to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
	if: ${{ always() }}
	run: sudo chown -R 1001:116 .
	# Tar workspace files
	- name: 'Tar .vo files'
	run: tar -cf workspace.tar .
	# We upload build artifacts for use by documentation
	- name: 'Upload Artifact'
	uses: actions/upload-artifact@v4
	with:
	name: workspace-${{ env.coq-version }}
	path: workspace.tar

	# Nix build
	nix:
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	- uses: cachix/install-nix-action@v20
	with:
	name: coq-hott
	authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
	extraPullNames: coq-hott
	- run: nix build


	#
	# Stage 2:
	#

	# Here we define the documentation and validation jobs:
	# - doc-alectryon: Builds the alectryon documentation
	# - doc-dep-graph: Builds dependency graphs
	# - doc-coqdoc: Builds the coqdoc documentation
	# - doc-timing: Builds the timing documentation
	# - coqchk: Runs coqchk
	# - install: Tests install target

	# alectryon job
	doc-alectryon:
	needs: build
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	# Download artifact
	- uses: actions/download-artifact@v4
	with:
	name: workspace-${{ env.coq-version-supported }}
	# Unpack Tar
	- run: tar -xf workspace.tar
	- name: add problem matchers
	run: \|
	#echo "::add-matcher::etc/coq-scripts/github/coq-oneline-error.json" # now via a script
	#echo "::add-matcher::etc/coq-scripts/github/coqdoc.json" # disabled for now, since they don't have file names
	echo "::add-matcher::etc/coq-scripts/github/alectryon-error.json"
	#echo "::add-matcher::etc/coq-scripts/github/alectryon-warning.json" # too noisy right now, cf https://github.com/cpitclaudel/alectryon/issues/34 and https://github.com/cpitclaudel/alectryon/issues/33
	- uses: coq-community/docker-coq-action@v1
	with:
	coq_version: ${{ env.coq-version-supported }}
	ocaml_version: ${{ env.ocaml-version }}
	custom_script: \|
	opam install -y coq-serapi
	sudo apt-get -o Acquire::Retries=30 update -q
	sudo apt-get -o Acquire::Retries=30 install python3-pip python3-venv autoconf -y --allow-unauthenticated
	startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
	sudo chown -R coq:coq .
	endGroup
	# Create and activate a virtual environment
	python3 -m venv myenv
	source myenv/bin/activate
	# Install the required Python packages in the virtual environment
	python -m pip install --upgrade pip
	python -m pip install pygments dominate beautifulsoup4 docutils==0.17.1
	echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
	make alectryon ALECTRYON_EXTRAFLAGS=--traceback
	- name: Revert permissions
	# to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
	if: ${{ always() }}
	run: sudo chown -R 1001:116 .
	- name: tar alectryon artifact
	run: tar -cf alectryon-html.tar alectryon-html
	- name: upload alectryon artifact
	uses: actions/upload-artifact@v4
	with:
	name: alectryon-html
	path: alectryon-html.tar


	# dependency graph doc job
	doc-dep-graphs:
	needs: build
	runs-on: ubuntu-latest
	steps:
	# Checkout branch
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	# Download artifact
	- uses: actions/download-artifact@v4
	with:
	name: workspace-${{ env.coq-version-supported }}
	# Unpack Tar
	- run: tar -xf workspace.tar
	# We use the coq docker so we don't have to build coq
	- uses: coq-community/docker-coq-action@v1
	with:
	coq_version: ${{ env.coq-version-supported }}
	ocaml_version: ${{ env.ocaml-version }}
	custom_script: \|
	sudo apt-get update
	sudo apt-get install -y ghc cabal-install
	sudo apt-get install -y --allow-unauthenticated \
	libssl-dev aspcud \
	graphviz xsltproc python3-lxml python-pexpect-doc \
	libxml2-dev libxslt1-dev time lua5.1 unzip npm
	# libnode-dev node-gyp

	cabal update
	cabal install --lib graphviz text fgl
	sudo -E npm config set strict-ssl false
	#sudo -E npm i -g npm
	sudo -E npm install -g doctoc

	startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
	sudo chown -R coq:coq .
	endGroup
	echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
	## Make dependency graph
	make HoTT.deps HoTTCore.deps
	runhaskell etc/DepsToDot.hs --coqdocbase="http://hott.github.io/Coq-HoTT/alectryon-html/" --title="HoTT Library Dependency Graph" < HoTT.deps > HoTT.dot
	runhaskell etc/DepsToDot.hs --coqdocbase="http://hott.github.io/Coq-HoTT/alectryon-html/" --title="HoTT Core Library Dependency Graph" < HoTTCore.deps > HoTTCore.dot
	dot -Tsvg HoTT.dot -o HoTT.svg
	dot -Tsvg HoTTCore.dot -o HoTTCore.svg
	rm -rf dep-graphs
	mkdir -p dep-graphs
	mv HoTT.svg HoTTCore.svg dep-graphs/

	## Install coq-dpdgraph
	opam install coq-dpdgraph.1.0+8.19 -y

	# For some reason, we get a stackoverflow. So we are lax
	# with making these.
	ulimit -s unlimited
	make svg-file-dep-graphs -k \|\| true
	## Try to make again to see errors
	make svg-file-dep-graphs -k \|\| true
	# `dot` hates file-dep-graphs/hott-all.dot, because it's too big, and
	# makes `dot` spin for over a dozen minutes. So disable it for now.
	#make svg-aggregate-dep-graphs -k \|\| exit $?

	# We try to make the index.html but there might be some dead
	# links if the previous didn't succeed.
	make file-dep-graphs/index.html -k \|\| true

	- name: Revert permissions
	# to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
	if: ${{ always() }}
	run: sudo chown -R 1001:116 .
	# Tar dependency graph files
	- name: 'Tar .svg files'
	run: \|
	tar -cf dep-graphs.tar dep-graphs
	tar -cf file-dep-graphs.tar file-dep-graphs
	# We upload the artifacts
	- name: 'Upload Artifact dep-graphs.tar'
	uses: actions/upload-artifact@v4
	with:
	name: dep-graphs
	path: dep-graphs.tar
	- name: 'Upload Artifact file-dep-graphs.tar'
	uses: actions/upload-artifact@v4
	with:
	name: file-dep-graphs
	path: file-dep-graphs.tar

	# doc-coqdoc job
	# This builds coqdoc and timing docs and uploads their artifacts
	doc-coqdoc:
	needs: build
	runs-on: ubuntu-latest
	steps:
	# Checkout branch
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	# Download artifact
	- uses: actions/download-artifact@v4
	with:
	name: workspace-${{ env.coq-version-supported }}
	# Unpack Tar
	- run: tar -xf workspace.tar
	# We use the coq docker so we don't have to build coq
	- uses: coq-community/docker-coq-action@v1
	with:
	coq_version: ${{ env.coq-version-supported }}
	ocaml_version: ${{ env.ocaml-version }}
	custom_script: \|
	startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
	sudo chown -R coq:coq .
	endGroup
	echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
	## Make HTML doc
	make -j2 html
	mv html coqdoc-html
	- name: Revert permissions
	# to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
	if: ${{ always() }}
	run: sudo chown -R 1001:116 .
	# Tar html files
	- name: 'Tar doc files'
	run: tar -cf coqdoc-html.tar coqdoc-html
	# Upload coqdoc-html artifact
	- name: 'Upload coqdoc-html Artifact'
	uses: actions/upload-artifact@v4
	with:
	name: coqdoc-html
	path: coqdoc-html.tar

	# doc-timing job
	# This builds coqdoc and timing docs and uploads their artifacts
	doc-timing:
	needs: build
	runs-on: ubuntu-latest
	steps:
	# Checkout branch
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	# Download artifact
	- uses: actions/download-artifact@v4
	with:
	name: workspace-${{ env.coq-version-supported }}
	# Unpack Tar
	- run: tar -xf workspace.tar
	# We use the coq docker so we don't have to build coq
	- uses: coq-community/docker-coq-action@v1
	with:
	coq_version: ${{ env.coq-version-supported }}
	ocaml_version: ${{ env.ocaml-version }}
	custom_script: \|
	sudo apt-get update
	sudo apt-get install -y time python3 python-is-python3 lua5.1
	startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
	sudo chown -R coq:coq .
	endGroup
	echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
	## Make timing doc
	make -j2 timing-html
	- name: Revert permissions
	# to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
	if: ${{ always() }}
	run: sudo chown -R 1001:116 .
	# Tar html files
	- name: 'Tar doc files'
	run: tar -cf timing-html.tar timing-html
	# Upload timing-html artifact
	- name: 'Upload timing-html Artifact'
	uses: actions/upload-artifact@v4
	with:
	name: timing-html
	path: timing-html.tar

	# The coqchk job
	coqchk:
	needs: build
	strategy:
	fail-fast: false
	matrix:
	# We build on our supported version of coq and the master version
	coq-version-dummy:
	- 'supported'
	- 'latest'
	- 'dev'
	env:
	coq-version: ${{ matrix.coq-version-dummy }}
	runs-on: ubuntu-latest
	steps:
	# Github actions doesn't let us set workflow level enviornment variables inside the stategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment varible env.coq-version, which uses the globablly set coq-version-supported when running the 'supported' case.
	- name: Set supported coq-version
	if: matrix.coq-version-dummy == 'supported'
	run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
	# Checkout branch
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	# Download artifact
	- uses: actions/download-artifact@v4
	with:
	name: workspace-${{ env.coq-version }}
	# Unpack Tar
	- run: tar -xf workspace.tar
	# We use the coq docker so we don't have to build coq
	- uses: coq-community/docker-coq-action@v1
	with:
	coq_version: ${{ env.coq-version }}
	ocaml_version: ${{ env.ocaml-version }}
	custom_script: \|
	startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
	sudo chown -R coq:coq .
	endGroup
	echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
	make validate
	- name: Revert permissions
	# to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
	if: ${{ always() }}
	run: sudo chown -R 1001:116 .

	# Test install target
	install:
	needs: build
	strategy:
	fail-fast: false
	matrix:
	# We build on our supported version of coq and the master version
	coq-version-dummy:
	- 'supported'
	- 'latest'
	- 'dev'
	env:
	coq-version: ${{ matrix.coq-version-dummy }}
	runs-on: ubuntu-latest
	steps:
	# Github actions doesn't let us set workflow level enviornment variables inside the stategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment varible env.coq-version, which uses the globablly set coq-version-supported when running the 'supported' case.
	- name: Set supported coq-version
	if: matrix.coq-version-dummy == 'supported'
	run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
	# Checkout branch
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	# Download artifact
	- uses: actions/download-artifact@v4
	with:
	name: workspace-${{ env.coq-version }}
	# Unpack Tar
	- run: tar -xf workspace.tar
	# We use the coq docker so we don't have to build coq
	- uses: coq-community/docker-coq-action@v1
	with:
	coq_version: ${{ env.coq-version }}
	ocaml_version: ${{ env.ocaml-version }}
	custom_script: \|
	startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
	sudo chown -R coq:coq .
	endGroup
	echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
	## Test install target
	make install
	echo 'Require Import HoTT.HoTT.' \| coqtop -q

	- name: Revert permissions
	# to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
	if: ${{ always() }}
	run: sudo chown -R 1001:116 .

	#
	# Stage 3
	#

	deploy-doc:
	# We only deploy when the reference is the master branch
	if: ${{ github.ref == 'refs/heads/master' }}
	# This job relies on the documentation jobs having finished. Technically we don't need to rely on coqchk and install, but it is simpler this way.
	needs:
	- coqchk
	- install
	- doc-alectryon
	- doc-dep-graphs
	- doc-coqdoc
	- doc-timing
	runs-on: ubuntu-latest
	steps:
	# Checkout branch
	- uses: actions/checkout@v4
	# Download alectryon artifact
	- uses: actions/download-artifact@v4
	with:
	name: alectryon-html
	# Download dependency graph artifacts
	- uses: actions/download-artifact@v4
	with:
	name: dep-graphs
	# Download file dependency graph artifacts
	- uses: actions/download-artifact@v4
	with:
	name: file-dep-graphs
	# Download coqdoc artifact
	- uses: actions/download-artifact@v4
	with:
	name: coqdoc-html
	# Download timing artifact
	- uses: actions/download-artifact@v4
	with:
	name: timing-html
	# Unpack Tar files
	- run: \|
	mkdir doc
	tar -xf alectryon-html.tar -C doc
	tar -xf dep-graphs.tar -C doc
	tar -xf file-dep-graphs.tar -C doc
	tar -xf coqdoc-html.tar -C doc
	tar -xf timing-html.tar -C doc

	- name: Deploy 🚀
	uses: JamesIves/[email protected]
	with:
	branch: ${{ env.deployment-branch }}
	folder: doc
	single-commit: true


	#
	# Stage 4
	#

	# Here we define the cleanup job:
	# - delete-artifacts: We delete the artifacts from the previous jobs

	delete-artifacts:
	# We always want to run this job even if we cancel
	if: ${{ always() }}
	# We depend on the stage 3 jobs
	needs:
	- deploy-doc
	runs-on: ubuntu-latest
	steps:
	# Delete workspace artifacts
	- uses: geekyeggo/delete-artifact@v5
	with:
	name: workspace-${{ env.coq-version-supported }}
	- uses: geekyeggo/delete-artifact@v5
	with:
	name: workspace-latest
	- uses: geekyeggo/delete-artifact@v5
	with:
	name: workspace-dev
	# Delete documentation artifacts
	- uses: geekyeggo/delete-artifact@v5
	with:
	name: dep-graphs
	- uses: geekyeggo/delete-artifact@v5
	with:
	name: file-dep-graphs
	- uses: geekyeggo/delete-artifact@v5
	with:
	name: alectryon-html
	- uses: geekyeggo/delete-artifact@v5
	with:
	name: coqdoc-html
	- uses: geekyeggo/delete-artifact@v5
	with:
	name: timing-html

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Defining properties of maxima and minima, lemmas for the take operation in lists, lists from sequences. #3252

Workflow file

Defining properties of maxima and minima, lemmas for the take operation in lists, lists from sequences. #3252

Jobs

Run details

Workflow file for this run