Merge branch 'main' into dev #1193

	name: Ubuntu CI
	permissions: {}

	on:
	workflow_dispatch:
	push:
	branches: [main, dev]
	pull_request:
	types: [opened, reopened, synchronize]

	concurrency:
	group: ${{ github.workflow }}-${{ github.event.pull_request.number \|\| github.ref }}
	cancel-in-progress: true

	env:
	NPROC: 3

	jobs:
	ubuntu:
	permissions:
	contents: read
	runs-on: ubuntu-latest
	strategy:
	fail-fast: false
	steps:
	- name: Checkout source code
	uses: actions/checkout@v4
	- name: Setup cache
	uses: actions/cache@v3
	with:
	# Ref: https://github.com/apache/incubator-mxnet/pull/18459/files
	path: ~/.ccache
	# We include the commit sha in the cache key, as new cache entries are
	# only created if there is no existing entry for the key yet.
	key: ${{ runner.os }}-ccache-${{ github.sha }}
	# Restore any ccache cache entry, if none for
	# ${{ runner.os }}-ccache-${{ github.sha }} exists.
	# Common prefix will be used so that ccache can be used across commits.
	restore-keys: \|
	${{ runner.os }}-ccache
	- name: Set up Python version
	uses: actions/setup-python@v5
	with:
	python-version: "3.11"
	# Pre-installed packages: https://github.com/actions/runner-images/tree/main/images
	- name: Install ccache
	run: \|
	sudo apt-get --yes install ccache
	ccache -M 2G # GitHub's total cache limit is 5GB for all OSes.
	- name: Config and build
	run: \|
	PATH=/usr/lib/ccache:$PATH
	ccache -s
	./ci/run_ci.sh
	ccache -s

Provide feedback