search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
198 stars 35 forks source link

global `set_option`. #58

Closed joneugster closed 1 year ago

joneugster commented 1 year ago

I would like a global way to set for example set_option tactic.hygienic false for the entire game as I'm now adding that to each level individually.

joneugster commented 1 year ago

Fixed, adding the options to the lakefile.lean

package Adam where
  moreLeanArgs := #["-DautoImplicit=false", "-Dtactic.hygienic=false"]
  moreServerArgs := #["-DautoImplicit=false", "-Dtactic.hygienic=false"]