Trigger CI for leanprover/lean4#2766

.github/workflows/bors.yml

@@ -179,7 +179,7 @@ jobs:
 
       - name: check for noisy stdout lines
         run: |
-          ! grep "stdout:" stdout.log
+          ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras
@@ -256,10 +256,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-          # we just keep rebuilding until it works!
-          # I'll try to come up with something better.
-          until lake build > /dev/null 2>&1; do :; done
+          lake build
           ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker

.github/workflows/build.yml

@@ -16,6 +16,7 @@ on:
       - 'nolints'
       # ignore staging branch used by bors, this is handled by bors.yml
       - 'staging'
+  merge_group:
 
 name: continuous integration
 
@@ -185,7 +186,7 @@ jobs:
 
       - name: check for noisy stdout lines
         run: |
-          ! grep "stdout:" stdout.log
+          ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras
@@ -262,10 +263,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-          # we just keep rebuilding until it works!
-          # I'll try to come up with something better.
-          until lake build > /dev/null 2>&1; do :; done
+          lake build
           ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker

.github/workflows/build.yml.in

@@ -165,7 +165,7 @@ jobs:
 
       - name: check for noisy stdout lines
         run: |
-          ! grep "stdout:" stdout.log
+          ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras
@@ -242,10 +242,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-          # we just keep rebuilding until it works!
-          # I'll try to come up with something better.
-          until lake build > /dev/null 2>&1; do :; done
+          lake build
           ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker

.github/workflows/build_fork.yml

@@ -183,7 +183,7 @@ jobs:
 
       - name: check for noisy stdout lines
         run: |
-          ! grep "stdout:" stdout.log
+          ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras
@@ -260,10 +260,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-          # we just keep rebuilding until it works!
-          # I'll try to come up with something better.
-          until lake build > /dev/null 2>&1; do :; done
+          lake build
           ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker

.github/workflows/label_new_contributor.yml

@@ -0,0 +1,45 @@
+name: Label New Contributors
+
+on:
+  pull_request:
+    types: [opened]
+
+jobs:
+  label-new-contributor:
+    runs-on: ubuntu-latest
+    permissions:
+      pull-requests: write
+
+    steps:
+    - name: Get PR author
+      id: pr-author
+      run: echo "::set-output name=author::$(jq -r .pull_request.user.login "$GITHUB_EVENT_PATH")"
+      shell: bash
+
+    - name: Check if user is new contributor
+      id: check-contributor
+      uses: actions/github-script@v5
+      with:
+        script: |
+          const { owner, repo } = context.repo
+          const author = "${{ steps.pr-author.outputs.author }}"
+          const prs = await github.rest.pulls.list({
+            owner,
+            repo,
+            state: "closed",
+            author
+          })
+          return (prs.data.length < 5)
+
+    - name: Add label if new contributor
+      if: steps.check-contributor.outputs.result == 'true'
+      uses: actions/github-script@v5
+      with:
+        script: |
+          const { owner, repo, number } = context.issue
+          await github.rest.issues.addLabels({
+            owner,
+            repo,
+            issue_number: number,
+            labels: ['new-contributor']
+          })

.github/workflows/mk_build_yml.sh

@@ -28,6 +28,7 @@ on:
       - 'nolints'
       # ignore staging branch used by bors, this is handled by bors.yml
       - 'staging'
+  merge_group:
 
 name: continuous integration
 EOF

.github/workflows/nightly_bump_toolchain.yml

@@ -10,7 +10,7 @@ jobs:
 
     steps:
     - name: Checkout code
-      uses: actions/checkout@v2
+      uses: actions/checkout@v3
       with:
         ref: nightly-testing # checkout nightly-testing branch
         token: ${{ secrets.NIGHTLY_TESTING }}

.github/workflows/nightly_detect_failure.yml

@@ -23,3 +23,25 @@ jobs:
         topic: 'CI failure on the nightly-testing branch'
         content: |
           The latest CI for branch#nightly-testing has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}).
+
+  handle_success:
+    if: ${{ github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.head_branch == 'nightly-testing' }}
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout code
+      uses: actions/checkout@v3
+      with:
+        ref: nightly-testing # checkout nightly-testing branch
+        fetch-depth: 0 # checkout all branches so that we can push from `nightly-testing` to `nightly-testing-YYYY-MM-DD`
+        token: ${{ secrets.NIGHTLY_TESTING }}
+    - name: Update the nightly-testing-YYYY-MM-DD branch
+      run: |
+        toolchain=$(<lean-toolchain)
+        if [[ $toolchain =~ leanprover/lean4:nightly-([a-zA-Z0-9_-]+) ]]; then
+          version=${BASH_REMATCH[1]}
+          git push origin refs/heads/nightly-testing:refs/heads/nightly-testing-$version
+        else
+          echo "Error: The file lean-toolchain does not contain the expected pattern."
+          exit 1
+        fi

.github/workflows/nightly_merge_master.yml

@@ -12,7 +12,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repository
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
         with:
           fetch-depth: 0
           token: ${{ secrets.NIGHTLY_TESTING }}

Archive.lean

@@ -1,4 +1,7 @@
 import Archive.Arithcc
+import Archive.Examples.IfNormalization.Result
+import Archive.Examples.IfNormalization.Statement
+import Archive.Examples.IfNormalization.WithoutAesop
 import Archive.Examples.MersennePrimes
 import Archive.Examples.PropEncodable
 import Archive.Imo.Imo1959Q1

Archive/Examples/IfNormalization/Result.lean

@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2023 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+-/
+import Archive.Examples.IfNormalization.Statement
+import Mathlib.Data.List.AList
+import Mathlib.Tactic.Recall
+
+/-!
+# A solution to the if normalization challenge in Lean.
+
+See `Statement.lean` for background.
+-/
+
+set_option autoImplicit true
+
+macro "◾" : tactic => `(tactic| aesop)
+macro "◾" : term => `(term| by aesop)
+
+namespace IfExpr
+
+/-!
+We add some local simp lemmas so we can unfold the definitions of the normalization condition.
+-/
+attribute [local simp] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
+  List.disjoint
+
+/-!
+Adding these lemmas to the simp set allows Lean to handle the termination proof automatically.
+-/
+attribute [local simp] Nat.lt_add_one_iff le_add_of_le_right
+
+/-!
+Some further simp lemmas for handling if-then-else statements.
+-/
+attribute [local simp] apply_ite ite_eq_iff'
+
+-- A copy of Lean's `decide_eq_true_eq` which unifies the `Decidable` instance
+-- rather than finding it by typeclass search.
+-- See https://github.com/leanprover/lean4/pull/2816
+@[simp] theorem decide_eq_true_eq {i : Decidable p} : (@decide p i = true) = p :=
+  _root_.decide_eq_true_eq
+
+
+/-!
+Simp lemmas for `eval`.
+We don't want a `simp` lemma for `(ite i t e).eval` in general, only once we know the shape of `i`.
+-/
+@[simp] theorem eval_lit : (lit b).eval f  = b := rfl
+@[simp] theorem eval_var : (var i).eval f  = f i := rfl
+@[simp] theorem eval_ite_lit :
+    (ite (.lit b) t e).eval f = bif b then t.eval f else e.eval f := rfl
+@[simp] theorem eval_ite_var :
+    (ite (.var i) t e).eval f = bif f i then t.eval f else e.eval f := rfl
+@[simp] theorem eval_ite_ite :
+    (ite (ite a b c) d e).eval f = (ite a (ite b d e) (ite c d e)).eval f := by
+  cases h : eval f a <;> simp_all [eval]
+
+/-- Custom size function for if-expressions, used for proving termination. -/
+@[simp] def normSize : IfExpr → Nat
+  | lit _ => 0
+  | var _ => 1
+  | .ite i t e => 2 * normSize i + max (normSize t) (normSize e) + 1
+
+/-- Normalizes the expression at the same time as assigning all variables in
+`e` to the literal booleans given by `l` -/
+def normalize (l : AList (fun _ : ℕ => Bool)) :
+    (e : IfExpr) → { e' : IfExpr //
+        (∀ f, e'.eval f = e.eval (fun w => (l.lookup w).elim (f w) (fun b => b)))
+        ∧ e'.normalized
+        ∧ ∀ (v : ℕ), v ∈ vars e' → l.lookup v = none }
+  | lit b => ⟨lit b, ◾⟩
+  | var v =>
+    match h : l.lookup v with
+    | none => ⟨var v, ◾⟩
+    | some b => ⟨lit b, ◾⟩
+  | .ite (lit true)   t e => have t' := normalize l t; ⟨t'.1, ◾⟩
+  | .ite (lit false)  t e => have e' := normalize l e; ⟨e'.1, ◾⟩
+  | .ite (.ite a b c) t e => have i' := normalize l (.ite a (.ite b t e) (.ite c t e)); ⟨i'.1, ◾⟩
+  | .ite (var v)      t e =>
+    match h : l.lookup v with
+    | none =>
+      have ⟨t', ht₁, ht₂, ht₃⟩ := normalize (l.insert v true) t
+      have ⟨e', he₁, he₂, he₃⟩ := normalize (l.insert v false) e
+      ⟨if t' = e' then t' else .ite (var v) t' e', by
+        refine ⟨fun f => ?_, ?_, fun w b => ?_⟩
+        · -- eval = eval
+          simp
+          cases hfv : f v
+          · simp_all
+            congr
+            ext w
+            by_cases w = v <;> ◾
+          · simp [h, ht₁]
+            congr
+            ext w
+            by_cases w = v <;> ◾
+        · -- normalized
+          have := ht₃ v
+          have := he₃ v
+          ◾
+        · -- lookup = none
+          have := ht₃ w
+          have := he₃ w
+          by_cases w = v <;> ◾⟩
+    | some b =>
+      have i' := normalize l (.ite (lit b) t e); ⟨i'.1, ◾⟩
+  termination_by normalize e => e.normSize
+  decreasing_by { decreasing_with simp (config := { arith := true }) [Zero.zero]; done }
+
+/-
+We recall the statement of the if-normalization problem.
+
+We want a function from if-expressions to if-expressions,
+that outputs normalized if-expressions and preserves meaning.
+-/
+recall IfNormalization :=
+  { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized ∧ (Z e).eval = e.eval }
+
+example : IfNormalization :=
+  ⟨_, fun e => ⟨(IfExpr.normalize ∅ e).2.2.1, by simp [(IfExpr.normalize ∅ e).2.1]⟩⟩