chore: simplify lakefile (#950)

.github/workflows/build.yml

@@ -20,7 +20,7 @@ jobs:
         name: build, test, and lint batteries
         uses: leanprover/lean-action@v1
         with:
-          build-args: '-Kwerror'
+          build-args: '--wfail'
 
       - name: Check that all files are imported
         run: lake env lean scripts/check_imports.lean

lakefile.lean

@@ -2,13 +2,8 @@ import Lake
 
 open Lake DSL
 
-macro "opt_arg?" x:ident v:term : term => `(if get_config? $x |>.isSome then $v else default)
-
 package batteries where
-  moreLeanArgs := opt_arg? werror #["-DwarningAsError=true"]
-  leanOptions :=
-    #[⟨`linter.missingDocs, true⟩] ++
-    opt_arg? disable_new_compiler #[⟨`compiler.enableNew, false⟩]
+  leanOptions := #[⟨`linter.missingDocs, true⟩]
 
 @[default_target]
 lean_lib Batteries