diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 9950b7dd51..b892e0f09c 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -16,17 +16,13 @@ import Lean.ResolveName
 namespace Lean
 namespace Core
 
-def maxHeartbeatsDefault := 50000
-
-builtin_initialize
-  registerOption `maxHeartbeats {
-    defValue := DataValue.ofNat maxHeartbeatsDefault,
-    group := "",
-    descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
-  }
+register_builtin_option maxHeartbeats : Nat := {
+  defValue := 50000
+  descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
+}
 
 def getMaxHeartbeats (opts : Options) : Nat :=
-  opts.get `maxHeartbeats maxHeartbeatsDefault * 1000
+  maxHeartbeats.get opts * 1000
 
 structure State where
   env             : Environment
@@ -111,7 +107,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 instance [MetaEval α] : MetaEval (CoreM α) where
   eval env opts x _ := do
     let x : CoreM α := do try x finally printTraces
-    let (a, s) ← x.toIO { maxRecDepth := getMaxRecDepth opts, options := opts } { env := env }
+    let (a, s) ← x.toIO { maxRecDepth := maxRecDepth.get opts, options := opts } { env := env }
     MetaEval.eval s.env opts a (hideUnit := true)
 
 -- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
diff --git a/src/Lean/Data/Format.lean b/src/Lean/Data/Format.lean
index 7476c600e0..ebec3626d7 100644
--- a/src/Lean/Data/Format.lean
+++ b/src/Lean/Data/Format.lean
@@ -14,13 +14,23 @@ def getWidth (o : Options) : Nat    := o.get `format.width  defWidth
 def getIndent (o : Options) : Nat   := o.get `format.indent defIndent
 def getUnicode (o : Options) : Bool := o.get `format.unicode defUnicode
 
-builtin_initialize
-  registerOption `format.indent { defValue := defIndent, group := "format", descr := "indentation" }
-  registerOption `format.unicode { defValue := defUnicode, group := "format", descr := "unicode characters" }
-  registerOption `format.width { defValue := defWidth, group := "format", descr := "line width" }
+register_builtin_option format.width : Nat := {
+  defValue := defWidth
+  descr := "indentation"
+}
+
+register_builtin_option format.unicode : Bool := {
+  defValue := defUnicode
+  descr    := "unicode characters"
+}
+
+register_builtin_option format.indent : Nat := {
+  defValue := defIndent
+  descr    := "indentation"
+}
 
 def pretty' (f : Format) (o : Options := {}) : String :=
-  pretty f (getWidth o)
+  pretty f (format.width.get o)
 
 end Format
 end Std
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 9af90f2431..731361435b 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -53,10 +53,10 @@ abbrev CommandElab  := Syntax → CommandElabM Unit
 abbrev Linter := Syntax → CommandElabM Unit
 
 def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State := {
-  env := env
-  messages := messages
-  scopes := [{ header := "", opts := opts }]
-  maxRecDepth := getMaxRecDepth opts
+  env         := env
+  messages    := messages
+  scopes      := [{ header := "", opts := opts }]
+  maxRecDepth := maxRecDepth.get opts
 }
 
 /- Linters should be loadable as plugins, so store in a global IO ref instead of an attribute managed by the
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 24e6fba2db..5e5ba3f82e 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -331,18 +331,14 @@ private def updateResultingUniverse (numParams : Nat) (indTypes : List Inductive
     let ctors := indType.ctors.map fun ctor => { ctor with type := updateLevel ctor.type };
     { indType with type := type, ctors := ctors }
 
-builtin_initialize
-  registerOption `bootstrap.inductiveCheckResultingUniverse {
+register_builtin_option bootstrap.inductiveCheckResultingUniverse : Bool := {
     defValue := true,
     group    := "bootstrap",
     descr    := "by default the `inductive/structure commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into `Prop`. In the `Init` package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator"
-  }
-
-def getCheckResultingUniverseOption (opts : Options) : Bool :=
-  opts.get `bootstrap.inductiveCheckResultingUniverse true
+}
 
 def checkResultingUniverse (u : Level) : TermElabM Unit := do
-  if getCheckResultingUniverseOption (← getOptions) then
+  if bootstrap.inductiveCheckResultingUniverse.get (← getOptions) then
     let u ← instantiateLevelMVars u
     if !u.isZero && !u.isNeverZero then
       throwError! "invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'{indentD u}"
@@ -497,7 +493,7 @@ def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
   let ref := view0.ref
   runTermElabM view0.declName fun vars => withRef ref do
     mkInductiveDecl vars views
-    mkSizeOfInstances view0.declName  
+    mkSizeOfInstances view0.declName
   applyDerivingHandlers views
 
 end Lean.Elab.Command
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 78050e0bed..e20fe28289 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -689,16 +689,15 @@ def elabMatchAltView (alt : MatchAltView) (matchType : Expr) : TermElabM (AltLHS
 def mkMatcher (elimName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss : List AltLHS) : TermElabM MatcherResult :=
   liftMetaM $ Meta.Match.mkMatcher elimName matchType numDiscrs lhss
 
-builtin_initialize
-  registerOption `match.ignoreUnusedAlts { defValue := false, group := "", descr := "if true, do not generate error if an alternative is not used" }
-
-def ignoreUnusedAlts (opts : Options) : Bool :=
-  opts.get `match.ignoreUnusedAlts false
+register_builtin_option match.ignoreUnusedAlts : Bool := {
+  defValue := false
+  descr := "if true, do not generate error if an alternative is not used"
+}
 
 def reportMatcherResultErrors (altLHSS : List AltLHS) (result : MatcherResult) : TermElabM Unit := do
   unless result.counterExamples.isEmpty do
     withHeadRefOnly <| throwError! "missing cases:\n{Meta.Match.counterExamplesToMessageData result.counterExamples}"
-  unless ignoreUnusedAlts (← getOptions) || result.unusedAltIdxs.isEmpty do
+  unless match.ignoreUnusedAlts.get (← getOptions) || result.unusedAltIdxs.isEmpty do
     let mut i := 0
     for alt in altLHSS do
       if result.unusedAltIdxs.contains i then
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index c5b38cf3ef..e6855118b7 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -543,7 +543,7 @@ def throwTypeMismatchError {α} (header? : Option String) (expectedType : Expr)
   | some f => Meta.throwAppTypeMismatch f e extraMsg
 
 @[inline] def withoutMacroStackAtErr {α} (x : TermElabM α) : TermElabM α :=
-  withTheReader Core.Context (fun (ctx : Core.Context) => { ctx with options := setMacroStackOption ctx.options false }) x
+  withTheReader Core.Context (fun (ctx : Core.Context) => { ctx with options := pp.macroStack.set ctx.options false }) x
 
 /- Try to synthesize metavariable using type class resolution.
    This method assumes the local context and local instances of `instMVar` coincide
@@ -569,14 +569,13 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
   | LOption.undef    => pure false -- we will try later
   | LOption.none     => throwError! "failed to synthesize instance{indentExpr type}"
 
-def maxCoeSizeDefault := 16
-builtin_initialize
-  registerOption `maxCoeSize { defValue := maxCoeSizeDefault, group := "", descr := "maximum number of instances used to construct an automatic coercion" }
-private def getCoeMaxSize (opts : Options) : Nat :=
-  opts.getNat `maxCoeSize maxCoeSizeDefault
+register_builtin_option maxCoeSize : Nat := {
+  defValue := 16
+  descr    := "maximum number of instances used to construct an automatic coercion"
+}
 
 def synthesizeCoeInstMVarCore (instMVar : MVarId) : TermElabM Bool := do
-  synthesizeInstMVarCore instMVar (getCoeMaxSize (← getOptions))
+  synthesizeInstMVarCore instMVar (some (maxCoeSize.get (← getOptions)))
 
 /-
 The coercion from `α` to `Thunk α` cannot be implemented using an instance because it would
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 0ab1b36443..525e4ca717 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -56,15 +56,14 @@ def getBetterRef (ref : Syntax) (macroStack : MacroStack) : Syntax :=
     | some elem => elem.before
     | none      => ref
 
-def ppMacroStackDefault := false
-def getMacroStackOption (o : Options) : Bool:= o.get `pp.macroStack ppMacroStackDefault
-def setMacroStackOption (o : Options) (flag : Bool) : Options := o.setBool `pp.macroStack flag
-
-builtin_initialize
-  registerOption `pp.macroStack { defValue := ppMacroStackDefault, group := "pp", descr := "dispaly macro expansion stack" }
+register_builtin_option pp.macroStack : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "dispaly macro expansion stack"
+}
 
 def addMacroStack {m} [Monad m] [MonadOptions m] (msgData : MessageData) (macroStack : MacroStack) : m MessageData := do
-  if !getMacroStackOption (← getOptions) then pure msgData else
+  if !pp.macroStack.get (← getOptions) then pure msgData else
   match macroStack with
   | []             => pure msgData
   | stack@(top::_) =>
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index fb5dc48a4e..f188f92f35 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -568,11 +568,11 @@ private def getUElimPos? (matcherLevels : List Level) (uElim : Level) : MetaM (O
     | some pos => pure $ some pos.val
 
 /- See comment at `mkMatcher` before `mkAuxDefinition` -/
-builtin_initialize
-  registerOption `bootstrap.gen_matcher_code { defValue := true, group := "bootstrap", descr := "disable code generation for auxiliary matcher function" }
-
-def generateMatcherCode (opts : Options) : Bool :=
-  opts.get `bootstrap.gen_matcher_code true
+register_builtin_option bootstrap.genMatcherCode : Bool := {
+  defValue := true
+  group := "bootstrap"
+  descr := "disable code generation for auxiliary matcher function"
+}
 
 /-
 Create a dependent matcher for `matchType` where `matchType` is of the form
@@ -616,7 +616,7 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss :
        | negSucc n => succ n
        ```
        which is defined **before** `Int.decLt` -/
-    let matcher ← mkAuxDefinition matcherName type val (compile := generateMatcherCode (← getOptions))
+    let matcher ← mkAuxDefinition matcherName type val (compile := bootstrap.genMatcherCode.get (← getOptions))
     trace[Meta.Match.debug]! "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
     let uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen
     discard <| isLevelDefEq uElimGen uElim
diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean
index 8009f3427c..4b551d0df7 100644
--- a/src/Lean/Meta/SizeOf.lean
+++ b/src/Lean/Meta/SizeOf.lean
@@ -280,18 +280,18 @@ private def mkSizeOfSpecTheorems (indTypeNames : Array Name) (sizeOfFns : Array
       mkSizeOfSpecTheorem indInfo sizeOfFns recMap ctorName
   return ()
 
-builtin_initialize
-  registerOption `genSizeOf { defValue := true, group := "", descr := "generate `SizeOf` instance for inductive types and structures" }
-  registerOption `genSizeOfSpec { defValue := true, group := "", descr := "generate `SizeOf` specificiation theorems for automatically generated instances" }
+register_builtin_option genSizeOf : Bool := {
+  defValue := true
+  descr    := "generate `SizeOf` instance for inductive types and structures"
+}
 
-def generateSizeOfInstance (opts : Options) : Bool :=
-  opts.get `genSizeOf true
-
-def generateSizeOfSpec (opts : Options) : Bool :=
-  opts.get `genSizeOfSpec true
+register_builtin_option genSizeOfSpec : Bool := {
+  defValue := true
+  descr    := "generate `SizeOf` specificiation theorems for automatically generated instances"
+}
 
 def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
-  if (← getEnv).contains ``SizeOf && generateSizeOfInstance (← getOptions) && !(← isInductivePredicate typeName) then
+  if (← getEnv).contains ``SizeOf && genSizeOf.get (← getOptions) && !(← isInductivePredicate typeName) then
     let indInfo ← getConstInfoInduct typeName
     unless indInfo.isUnsafe do
       let (fns, recMap) ← mkSizeOfFns typeName
@@ -319,7 +319,7 @@ def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
                 hints       := ReducibilityHints.abbrev
               }
               addInstance instDeclName AttributeKind.global (evalPrio! default)
-      if generateSizeOfSpec (← getOptions) then
+      if genSizeOfSpec.get (← getOptions) then
         mkSizeOfSpecTheorems indInfo.all.toArray fns recMap
 
 builtin_initialize
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index b6d406a96b..5aeb58f020 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -13,27 +13,23 @@ import Lean.Meta.WHNF
 import Lean.Util.Profile
 
 namespace Lean.Meta
+
+register_builtin_option synthInstance.maxHeartbeats : Nat := {
+  defValue := 300
+  descr := "maximum amount of heartbeats per typeclass resolution problem. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
+}
+
+register_builtin_option synthInstance.maxSize : Nat := {
+  defValue := 128
+  descr := "maximum number of instances used to construct a solution in the type class instance synthesis procedure"
+}
+
 namespace SynthInstance
 
-open Std (HashMap)
-
-def maxHeartbeatsDefault := 300
-
-builtin_initialize
-  registerOption `synthInstance.maxHeartbeats {
-    defValue := DataValue.ofNat maxHeartbeatsDefault,
-    group := "",
-    descr := "maximum amount of heartbeats per typeclass resolution problem. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
-  }
-
 def getMaxHeartbeats (opts : Options) : Nat :=
-  opts.get `synthInstance.maxHeartbeats maxHeartbeatsDefault * 1000
+  synthInstance.maxHeartbeats.get opts * 1000
 
-def maxResultSizeDefault := 128
-builtin_initialize
-  registerOption `synthInstance.maxSize { defValue := maxResultSizeDefault, group := "", descr := "maximum number of instances used to construct a solution in the type class instance synthesis procedure" }
-private def getMaxSize (opts : Options) : Nat :=
-  opts.getNat `synthInstance.maxSize maxResultSizeDefault
+open Std (HashMap)
 
 builtin_initialize inferTCGoalsRLAttr : TagAttribute ←
   registerTagAttribute `inferTCGoalsRL "instruct type class resolution procedure to solve goals from right to left for this instance"
@@ -561,7 +557,7 @@ private def preprocessOutParam (type : Expr) : MetaM Expr :=
 
 def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) ⟨0, 0⟩ do
   let opts ← getOptions
-  let maxResultSize := maxResultSize?.getD (SynthInstance.getMaxSize opts)
+  let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
   let inputConfig ← getConfig
   withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.reducible,
                                           foApprox := true, ctxApprox := true, constApprox := false }) do
diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean
index da6d3e5518..36930ce308 100644
--- a/src/Lean/Meta/Tactic/Intro.lean
+++ b/src/Lean/Meta/Tactic/Intro.lean
@@ -55,12 +55,14 @@ namespace Lean.Meta
   let (fvars, mvarId) ← loop n lctx #[] 0 s mvarType
   pure (fvars.map Expr.fvarId!, mvarId)
 
-def hygienicIntroDefault := true
-def getHygienicIntro : MetaM Bool := do
-  return (← getOptions).get `hygienicIntro hygienicIntroDefault
+register_builtin_option hygienicIntro : Bool := {
+  defValue := true
+  group    := "tactic"
+  descr    := "make sure 'intro'-like tactics are hygienic"
+}
 
-builtin_initialize
-  registerOption `hygienicIntro { defValue := hygienicIntroDefault, group := "tactic", descr := "make sure 'intro'-like tactics are hygienic" }
+def getHygienicIntro : MetaM Bool := do
+  return hygienicIntro.get (← getOptions)
 
 private def mkAuxNameImp (preserveBinderNames : Bool) (hygienic : Bool) (lctx : LocalContext) (binderName : Name) : List Name → MetaM (Name × List Name)
   | []         => do
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index c7ec5d2bbc..157b054448 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -22,11 +22,10 @@ def smartUnfoldingSuffix := "_sunfold"
 @[inline] def mkSmartUnfoldingNameFor (n : Name) : Name :=
   Name.mkStr n smartUnfoldingSuffix
 
-def smartUnfoldingDefault := true
-builtin_initialize
-  registerOption `smartUnfolding { defValue := smartUnfoldingDefault, group := "", descr := "when computing weak head normal form, use auxiliary definition created for functions defined by structural recursion" }
-private def useSmartUnfolding (opts : Options) : Bool :=
-  opts.getBool `smartUnfolding smartUnfoldingDefault
+register_builtin_option smartUnfolding : Bool := {
+  defValue := true
+  descr := "when computing weak head normal form, use auxiliary definition created for functions defined by structural recursion"
+}
 
 /- ===========================
    Helper methods
@@ -400,7 +399,7 @@ mutual
               deltaBetaDefinition fInfo fLvls e.getAppRevArgs (fun _ => pure none) (fun e => pure (some e))
             else
               return none
-          if useSmartUnfolding (← getOptions) then
+          if smartUnfolding.get (← getOptions) then
             let fAuxInfo? ← getConstNoEx? (mkSmartUnfoldingNameFor fInfo.name)
             match fAuxInfo? with
             | some fAuxInfo@(ConstantInfo.defnInfo _) =>
diff --git a/src/Lean/Util/RecDepth.lean b/src/Lean/Util/RecDepth.lean
index 3fc5319c47..c74972e99b 100644
--- a/src/Lean/Util/RecDepth.lean
+++ b/src/Lean/Util/RecDepth.lean
@@ -7,10 +7,9 @@ import Lean.Data.Options
 
 namespace Lean
 
-def getMaxRecDepth (opts : Options) : Nat :=
-  opts.getNat `maxRecDepth defaultMaxRecDepth
-
-builtin_initialize
-  registerOption `maxRecDepth { defValue := defaultMaxRecDepth, group := "", descr := "maximum recursion depth for many Lean procedures" }
+register_builtin_option maxRecDepth : Nat := {
+  defValue := defaultMaxRecDepth
+  descr    := "maximum recursion depth for many Lean procedures"
+}
 
 end Lean