From 4be202af23d9712b5991f68a4aea094be73e0d2d Mon Sep 17 00:00:00 2001 From: joneugster Date: Tue, 17 Oct 2023 16:05:46 +0200 Subject: [PATCH] modify lakefile to hide info messages when building --- lakefile.lean | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 5f82a60..242ffb5 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -8,7 +8,7 @@ def LocalGameServer : Dependency := { def RemoteGameServer : Dependency := { name := `GameServer - src := Source.git "https://github.com/leanprover-community/lean4game.git" "6970f10e30f70ecede1042201e9bd1d838ad1934" "server" + src := Source.git "https://github.com/leanprover-community/lean4game.git" "main" "server" } /- Choose dependency depending on the environment variable NODE_ENV -/ @@ -26,12 +26,13 @@ open Lean in require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "7d308680dc444730e84a86c72357ad9a7aea9c4b" - - +-- NOTE: We abuse the `trace.debug` option to toggle messages in VSCode on and +-- off when calling `lake build`. Ideally there would be a better way using `logInfo` and +-- an option like `lean4game.verbose`. package Game where - moreLeanArgs := #["-Dtactic.hygienic=false", "--quiet"] - moreServerArgs := #["-Dtactic.hygienic=false", "--quiet"] - weakLeanArgs := #["--quiet"] + moreLeanArgs := #["-Dtactic.hygienic=false", "-Dlinter.unusedVariables.funArgs=false", "-Dtrace.debug=false"] + moreServerArgs := #["-Dtactic.hygienic=false", "-Dlinter.unusedVariables.funArgs=true", "-Dtrace.debug=true"] + weakLeanArgs := #[] @[default_target] lean_lib Game