diff --git a/lakefile.lean b/lakefile.lean index 88bfec83..34d4bf2c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -10,12 +10,27 @@ def moreServerArgs := #[ -- These settings only apply during `lake build`, but not in VSCode editor. def moreLeanArgs := moreServerArgs +-- These are additional settings which do not affect the lake hash, +-- so they can be enabled in CI and disabled locally or vice versa. +-- Warning: Do not put any options here that actually change the olean files, +-- or inconsistent behavior may result +def weakLeanArgs : Array String := + if get_config? CI |>.isSome then + #["-DwarningAsError=true"] + else + #[] + package «carleson» where moreServerArgs := moreServerArgs require mathlib from git "https://github.com/leanprover-community/mathlib4.git" +-- This is run only if we're in `dev` mode. This is so not everyone has to build doc-gen +meta if get_config? env = some "dev" then +require «doc-gen4» from git + "https://github.com/leanprover/doc-gen4" @ "main" + @[default_target] lean_lib «Carleson» where moreLeanArgs := moreLeanArgs