Began implementing intrinsically typed regions #2703

	name: core library
	on:
	push:
	branches:
	- "main"
	pull_request:
	merge_group:

	permissions:
	contents: write

	jobs:
	build:
	name: core library
	permissions:
	pull-requests: write
	runs-on: ubuntu-latest
	steps:
	- name: Checkout 🛎️
	uses: actions/checkout@v3

	- name: Install elan 🕑
	run: \|
	set -o pipefail
	curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \| sh -s -- --default-toolchain none -y
	~/.elan/bin/lean --version
	echo "$HOME/.elan/bin" >> $GITHUB_PATH

	- name: Compile Library 🧐
	run: \|
	lake -R exe cache get # download cache of mathlib docs.
	lake -R build SSA

	- name: Compile Decide Experiment 🧐
	run: \|
	lake -R exe cache get # download cache of mathlib docs.
	lake -R build SSA.Experimental.Bits.Decide SSA.Experimental.Bits.Fast.Decide

	- name: Compile Alive Examples
	run: \|
	lake -R exe cache get # download cache of mathlib docs.
	lake -R build AliveExamples 2>&1 \| tee out
	echo `grep theorem SSA/Projects/InstCombine/AliveStatements.lean \| wc -l` > all
	grep 'Alive.*sorry' out \| wc -l > failed
	x=$((`cat all` - `cat failed`)); echo $x > diff
	echo "ALIVE_SUCCESS=$(cat diff)" >> $GITHUB_ENV
	echo "ALIVE_ALL=$(cat all)" >> $GITHUB_ENV
	echo "ALIVE_FAILED=$(cat failed)" >> $GITHUB_ENV

	- uses: actions/github-script@v6
	if: github.event_name == 'pull_request'
	with:
	script: \|
	github.rest.issues.createComment({
	issue_number: context.issue.number,
	owner: context.repo.owner,
	repo: context.repo.repo,
	body: `Alive Statistics: ${{env.ALIVE_SUCCESS}} / ${{env.ALIVE_ALL}} (${{env.ALIVE_FAILED}} failed)`
	})

Provide feedback