chore: enable fail on warning

.github/workflows/ci-tools.yml

@@ -27,7 +27,7 @@ jobs:
       - name: Compile `mlirnatural` Executable 🧐
         run: |
           lake -R exe cache get # download cache of mathlib docs.
-          lake -R build mlirnatural
+          lake -R build mlirnatural --wfail
 
       - name: LLVM Exhaustive Enumeration
         run: |
@@ -37,7 +37,7 @@ jobs:
       - name: Compile `opt` Executable 🧐
         run: |
           lake -R exe cache get # download cache of mathlib docs.
-          lake -R build opt
+          lake -R build opt --wfail
 
       - name: LLVM opt round trip test
         run: |
@@ -46,11 +46,11 @@ jobs:
       - name: Compile Alive Scaling
         run: |
           lake -R exe cache get # download cache of mathlib docs.
-          lake -R build AliveScaling
+          lake -R build AliveScaling --wfail
 
       - name: Check for changes in AliveStatements
         run: |
           lake -R exe cache get
-          lake build
+          lake build --wfail
           (cd SSA/Projects/InstCombine/; ./update_alive_statements.py)
           bash -c '! git diff | grep .'  # iff git diff is empty, 'grep .' fails, '!' inverts the failure, and in the forced bash

.github/workflows/ci.yml

@@ -29,12 +29,12 @@ jobs:
       - name: Compile Library 🧐
         run: |
           lake -R exe cache get # download cache of mathlib docs.
-          lake -R build SSA
+          lake -R build SSA --wfail
 
       - name: Compile Alive Examples
         run: |
           lake -R exe cache get # download cache of mathlib docs.
-          lake -R build AliveExamples 2>&1 | tee out
+          lake -R build AliveExamples --wfail 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

SSA/Projects/InstCombine/Alive.lean

@@ -2,10 +2,6 @@
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
--- Pure math statements needed to prove alive statements.
--- Include these, as they are reasonably fast to typecheck.
-import SSA.Projects.InstCombine.AliveStatements
-
 -- Handwritten Alive examples.
 -- This has those examples from alive that failed to be
 -- translated correctly due to bugs in the translator.

SSA/Projects/Tensor1D/Tensor1D.lean

@@ -38,25 +38,26 @@ def Tensor1d.empty [Inhabited α] : Tensor1d α where
 -- [0..[left..left+len)..size)
 -- if the (left + len) is larger than size, then we don't have a valid extract,
 -- so we return a size zero tensor.
-def Tensor1d.extract [Inhabited α] (t: Tensor1d α)
-  (left: Index) (len: Index) : Tensor1d α :=
-  let right := if (left + len) < t.size then left + len else 0
-  let size := right - left
-  { size := size,
-    val := fun ix =>
-    if left + len < t.size
-    then if (ix < len) then t.val (ix + left) else default
-    else default,
-    spec := by {
-      intros ix IX;
-      by_cases A:(left + len < t.size) <;> simp[A] at right ⊢;
-      try simp[A] at right
-      -- TODO: how to substitute?
-      have LEN : len < t.size := by simp[Index] at *; linarith
-      intros H
-      sorry
-    }
-  }
+-- def Tensor1d.extract [Inhabited α] (t: Tensor1d α)
+--   (left: Index) (len: Index) : Tensor1d α :=
+--   let right := if (left + len) < t.size then left + len else 0
+--   let size := right - left
+--   { size := size,
+--     val := fun ix =>
+--     if left + len < t.size
+--     then if (ix < len) then t.val (ix + left) else default
+--     else default,
+--     spec := by {
+--       intros ix IX;
+--       by_cases A:(left + len < t.size) <;> simp[A] at right ⊢;
+--       try simp[A] at right
+--       -- TODO: how to substitute?
+--       have LEN : len < t.size := by simp[Index] at *; linarith
+--       intros H
+--       sorry
+--     }
+--   }
+
 def Tensor1d.map [Inhabited α] (f : α → α) (t : Tensor1d α) : Tensor1d α where
   size := t.size
   val := fun ix => if ix < t.size then f (t.val ix) else default
@@ -72,15 +73,15 @@ def Tensor1d.map [Inhabited α] (f : α → α) (t : Tensor1d α) : Tensor1d α
 -- when we are out of bounds, because the side that is (map extract) will have
 -- (f default), while (extract map) will be (default)
 -- theorem 1: extract (map) = map extract
-theorem Tensor1d.extract_map [Inhabited α] (t: Tensor1d α) (left len: Index) :
-  (t.extract left len).map f = (t.map f).extract left len := by {
-    simp[Tensor1d.extract, Tensor1d.map]
-    funext ix;
-    by_cases VALID_EXTRACT : left + len < t.size <;> simp[VALID_EXTRACT]
-    by_cases VALID_INDEX : ix < len <;> simp[VALID_INDEX]
-    have IX_INBOUNDS : ix + left < t.size := by simp[Index] at *; linarith
-    simp[IX_INBOUNDS]
-}
+-- theorem Tensor1d.extract_map [Inhabited α] (t: Tensor1d α) (left len: Index) :
+--   (t.extract left len).map f = (t.map f).extract left len := by {
+--     simp[Tensor1d.extract, Tensor1d.map]
+--     funext ix;
+--     by_cases VALID_EXTRACT : left + len < t.size <;> simp[VALID_EXTRACT]
+--     by_cases VALID_INDEX : ix < len <;> simp[VALID_INDEX]
+--     have IX_INBOUNDS : ix + left < t.size := by simp[Index] at *; linarith
+--     simp[IX_INBOUNDS]
+-- }
 
 def Tensor1d.fill [Inhabited α] (t: Tensor1d α) (v: α) : Tensor1d α where
   size := t.size