Skip to content

feat: handwritten-proof AndOrXor #1502

feat: handwritten-proof AndOrXor

feat: handwritten-proof AndOrXor #1502

Workflow file for this run

name: build & test
on:
push:
branches:
- "main"
pull_request:
merge_group:
permissions:
contents: write
jobs:
build:
name: build and test code
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 Alive Examples
run: |
lake -R exe cache get # download cache of mathlib docs.
lake -R build AliveExamples
- name: Compile Alive Scaling
run: |
lake -R exe cache get # download cache of mathlib docs.
lake -R build AliveScaling
- name: Compile Executable 🧐
run: |
lake -R exe cache get # download cache of mathlib docs.
lake -R build mlirnatural
- name: LLVM Exhaustive Enumeration
run: |
sudo apt install llvm-15 # for opt-15, used to simplify LLVM for reference semantics.
cd test/bruteforce-correctness && ./run.sh
# - name: Run executable ⚙️
# run: |
# ./build/bin/mlirnatural instcombine-test1 "32,2,3" | grep "^some -2$"