disable annoying deprecation warnings & fix strange build error

GroundZero/Exercises/Chap4.lean

@@ -434,7 +434,8 @@ namespace «4.8»
   open GroundZero.Structures
   open GroundZero.Theorems
 
-  hott theorem injOutOfBoolChar {B : Type u} : (Σ (f : 𝟐 → B), injective f) ≃ (Σ (w : B × B), w.1 ≠ w.2) :=
+  -- TODO: what’s wrong with the code generation here?
+  noncomputable hott theorem injOutOfBoolChar {B : Type u} : (Σ (f : 𝟐 → B), injective f) ≃ (Σ (w : B × B), w.1 ≠ w.2) :=
   begin
     fapply Sigma.mk;
     { intro w; existsi (w.1 false, w.1 true);
@@ -453,7 +454,7 @@ namespace «4.8»
       { apply Theorems.funext; intro b; induction b using Bool.casesOn <;> reflexivity } }
   end
 
-  hott theorem embdOutOfBoolChar {B : Type u} :
+  noncomputable hott theorem embdOutOfBoolChar {B : Type u} :
     (𝟐 ↪ B) ≃ (Σ (w : B × B), w.1 ≠ w.2 × contr (w.1 = w.1) × contr (w.2 = w.2)) :=
   begin
     fapply Sigma.mk;

lakefile.lean

@@ -1,7 +1,14 @@
 import Lake
 open Lake DSL
 
-package GroundZero { leanOptions := #[⟨`linter.unusedVariables, false⟩, ⟨`autoImplicit, false⟩] }
+package GroundZero {
+  leanOptions := #[
+    ⟨`linter.deprecated, false⟩,
+    ⟨`linter.unusedVariables, false⟩,
+    ⟨`relaxedAutoImplicit, false⟩,
+    ⟨`autoImplicit, false⟩
+  ]
+}
 
 @[default_target]
 lean_lib GroundZero