doc: grove: update and add `String` data #18266

	name: Check awaiting-mathlib label

	on:
	merge_group:
	pull_request:
	types: [opened, synchronize, reopened, labeled, unlabeled]

	jobs:
	check-awaiting-mathlib:
	runs-on: ubuntu-latest
	steps:
	- name: Check awaiting-mathlib label
	id: check-awaiting-mathlib-label
	if: github.event_name == 'pull_request'
	uses: actions/github-script@v8
	with:
	script: \|
	const { labels, number: prNumber } = context.payload.pull_request;
	const hasAwaiting = labels.some(label => label.name == "awaiting-mathlib");
	const hasBreaks = labels.some(label => label.name == "breaks-mathlib");
	const hasBuilds = labels.some(label => label.name == "builds-mathlib");

	if (hasAwaiting && hasBreaks) {
	core.setFailed('PR has both "awaiting-mathlib" and "breaks-mathlib" labels.');
	} else if (hasAwaiting && !hasBreaks && !hasBuilds) {
	core.info('PR is marked "awaiting-mathlib" but neither "breaks-mathlib" nor "builds-mathlib" labels are present.');
	core.setOutput('awaiting', 'true');
	}

	- name: Wait for mathlib compatibility
	if: github.event_name == 'pull_request' && steps.check-awaiting-mathlib-label.outputs.awaiting == 'true'
	run: \|
	echo "::notice title=Awaiting mathlib::PR is marked 'awaiting-mathlib' but neither 'breaks-mathlib' nor 'builds-mathlib' labels are present."
	echo "This check will remain in progress until the PR is updated with appropriate mathlib compatibility labels."
	# Keep the job running indefinitely to show "in progress" status
	while true; do
	sleep 3600 # Sleep for 1 hour at a time
	done

Provide feedback