feat: Add `String.length_join` and `List.length_join` #6086

	on:
	push:
	branches-ignore:
	# ignore tmp branches used by bors
	- 'staging.tmp*'
	- 'trying.tmp*'
	- 'staging*.tmp'
	pull_request:

	name: ci

	jobs:
	build:
	name: Build
	runs-on: ubuntu-latest
	steps:
	- name: install elan
	run: \|
	set -o pipefail
	curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz \| tar xz
	./elan-init -y --default-toolchain none
	echo "$HOME/.elan/bin" >> $GITHUB_PATH

	- uses: actions/checkout@v4

	- name: build std
	id: build
	run: lake build -Kwerror

	- name: test std
	if: steps.build.outcome == 'success'
	run: make test

	- name: lint std
	if: steps.build.outcome == 'success'
	run: make lint

	- name: Check that all files are imported
	run: lake env lean scripts/check_imports.lean

	- name: Check for forbidden character ↦
	if: always()
	run: \|
	if grep -r -n --include=\*.lean -e '↦' . ; then
	echo "Error: Found forbidden character ↦"
	exit 1
	fi

	- name: Check for 'namespace Mathlib'
	if: always()
	run: \|
	if grep -r -n --include=\*.lean -e 'namespace Mathlib' . ; then
	echo "Error: Found 'namespace Mathlib'"
	exit 1
	fi

	- name: Check for long lines
	if: always()
	run: \|
	! (find Std -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; \| grep -v -E 'https?://')

	- name: Check for trailing whitespace
	if: always()
	run: \|
	scripts/lintWhitespace.sh

	- name: Don't 'import Lean', use precise imports
	if: always()
	run: \|
	! (find . -name "*.lean" ! -path "./test/import_lean.lean" -type f -print0 \| xargs -0 grep -E -n '^import Lean$')

Provide feedback