2023-04-25 18:37:27 +02:00
|
|
|
import Lake
|
|
|
|
|
open Lake DSL
|
|
|
|
|
|
2023-05-04 11:48:58 +02:00
|
|
|
def LocalGameServer : Dependency := {
|
|
|
|
|
name := `GameServer
|
|
|
|
|
src := Source.path "../lean4game/server"
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
def RemoteGameServer : Dependency := {
|
|
|
|
|
name := `GameServer
|
|
|
|
|
src := Source.git "https://github.com/leanprover-community/lean4game.git" "main" "server"
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/- Choose dependency depending on the environment variable NODE_ENV -/
|
|
|
|
|
open Lean in
|
|
|
|
|
#eval (do
|
|
|
|
|
let gameServerName :=
|
|
|
|
|
if (← IO.getEnv "NODE_ENV") == some "development" then ``LocalGameServer else ``RemoteGameServer
|
|
|
|
|
modifyEnv (fun env => Lake.packageDepAttr.ext.addEntry env gameServerName)
|
|
|
|
|
: Elab.Command.CommandElabM Unit)
|
|
|
|
|
|
2023-05-08 18:23:18 +02:00
|
|
|
require std from git
|
|
|
|
|
"https://github.com/leanprover/std4" @ "44a92d84c31a88b9af9329a441890ad449d8cd5f"
|
2023-04-25 18:37:27 +02:00
|
|
|
|
|
|
|
|
package NNG where
|
|
|
|
|
moreLeanArgs := #["-DautoImplicit=false", "-Dtactic.hygienic=false"]
|
|
|
|
|
moreServerArgs := #["-DautoImplicit=false", "-Dtactic.hygienic=false"]
|
|
|
|
|
|
|
|
|
|
@[default_target]
|
|
|
|
|
lean_lib NNG
|
