From b6715bcbffba02376cc3db2a47e6f631f81a7090 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 20 Apr 2023 15:45:06 +0200 Subject: [PATCH] add global options to the games (disbable tactic.hygienic) --- server/adam/lakefile.lean | 8 ++++---- server/nng/lakefile.lean | 10 +++++----- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/server/adam/lakefile.lean b/server/adam/lakefile.lean index d33792a..a075148 100644 --- a/server/adam/lakefile.lean +++ b/server/adam/lakefile.lean @@ -6,9 +6,9 @@ require GameServer from ".."/"leanserver" require mathlib from git "https://github.com/leanprover-community/mathlib4.git"@"master" -package Adam +package Adam where + moreLeanArgs := #["-DautoImplicit=false", "-Dtactic.hygienic=false"] + moreServerArgs := #["-DautoImplicit=false", "-Dtactic.hygienic=false"] @[default_target] -lean_lib Adam { - moreLeanArgs := #["-DautoImplicit=false"] -} +lean_lib Adam diff --git a/server/nng/lakefile.lean b/server/nng/lakefile.lean index 942473c..82868bf 100644 --- a/server/nng/lakefile.lean +++ b/server/nng/lakefile.lean @@ -3,12 +3,12 @@ open Lake DSL require GameServer from ".."/"leanserver" - require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "fc4a489c2af75f687338fe85c8901335360f8541" -package NNG + +package NNG where + moreLeanArgs := #["-DautoImplicit=false", "-Dtactic.hygienic=false"] + moreServerArgs := #["-DautoImplicit=false", "-Dtactic.hygienic=false"] @[default_target] -lean_lib NNG { - moreLeanArgs := #["-DautoImplicit=false"] -} +lean_lib NNG