diff --git a/src/lake/Lake/Config/Meta.lean b/src/lake/Lake/Config/Meta.lean
index f457662593..524d60e515 100644
--- a/src/lake/Lake/Config/Meta.lean
+++ b/src/lake/Lake/Config/Meta.lean
@@ -16,10 +16,8 @@ open Lean Syntax Parser Command
 
 namespace Lake
 
-public section -- for `syntax .. := ...`
-syntax configField :=
+public syntax configField :=
   atomic(nestedDeclModifiers ident,+) declSig (" := " term)?
-end
 
 /--
 An tailored `structure` command for producing Lake configuration data types.
diff --git a/src/lake/Lake/DSL/DeclUtil.lean b/src/lake/Lake/DSL/DeclUtil.lean
index 6c47ef0c5c..b0d15211c4 100644
--- a/src/lake/Lake/DSL/DeclUtil.lean
+++ b/src/lake/Lake/DSL/DeclUtil.lean
@@ -34,9 +34,7 @@ public def expandAttrs (attrs? : Option Attributes) : Array AttrInstance :=
   else
     #[]
 
-public section -- for `syntax ... := ...`
-
-syntax identOrStr :=
+public syntax identOrStr :=
   ident <|> str
 
 public abbrev IdentOrStr := TSyntax ``identOrStr
@@ -48,42 +46,40 @@ public def expandIdentOrStrAsIdent (stx : IdentOrStr) : Ident :=
   | _ => ⟨.missing⟩
 
 /-- A field assignment in a declarative configuration. -/
-syntax declField :=
+public syntax declField :=
   ident " := " term
 
 @[inherit_doc declField]
 public abbrev DeclField := TSyntax ``declField
 
-syntax structVal :=
+public syntax structVal :=
   "{" structInstFields(sepByIndentSemicolon(declField)) "}"
 
-syntax declValDo :=
+public syntax declValDo :=
   ppSpace Term.do (Term.whereDecls)?
 
-syntax declValStruct :=
+public syntax declValStruct :=
   ppSpace structVal (Term.whereDecls)?
 
-syntax declValWhere :=
+public syntax declValWhere :=
   " where " structInstFields(sepByIndentSemicolon(declField)) (Term.whereDecls)?
 
-syntax simpleDeclSig :=
+public syntax simpleDeclSig :=
   ident Term.typeSpec declValSimple
 
-syntax optConfig :=
+public syntax optConfig :=
   (declValWhere <|> declValStruct)?
 
 public abbrev OptConfig := TSyntax ``optConfig
 
-syntax bracketedSimpleBinder :=
+public syntax bracketedSimpleBinder :=
   "(" ident (" : " term)? ")"
 
-syntax simpleBinder :=
+public syntax simpleBinder :=
   ident <|> bracketedSimpleBinder
 
 public abbrev SimpleBinder := TSyntax ``simpleBinder
 
-end
-
 open Lean.Parser.Term in
 public def expandOptSimpleBinder (stx? : Option SimpleBinder) : MacroM FunBinder := do
   match stx? with
diff --git a/src/lake/Lake/DSL/Syntax.lean b/src/lake/Lake/DSL/Syntax.lean
index e10558c172..e3b83fb6f1 100644
--- a/src/lake/Lake/DSL/Syntax.lean
+++ b/src/lake/Lake/DSL/Syntax.lean
@@ -10,8 +10,6 @@ public import Lake.DSL.DeclUtil
 
 open Lean Parser Elab Command
 
-public section -- for `syntax ... := ...`
-
 /-!
 This module defines the syntax of the Lake DSL. The syntax is defined separately from the elaborator
 and/or macro definitions to allow clients to import it without crashing Lean. In particular, this
@@ -95,13 +93,13 @@ scoped syntax (name := postUpdateDecl)
 This is the `require` DSL syntax used to specify package dependencies.
 -/
 
-syntax fromPath :=
+public syntax fromPath :=
   term
 
-syntax fromGit :=
+public syntax fromGit :=
   &"git " term:max ("@" term:max)? ("/" term)?
 
-syntax fromSource :=
+public syntax fromSource :=
   fromGit <|> fromPath
 
 /--
@@ -130,30 +128,30 @@ branch, or tag. If none is provided, Lake defaults to `master`. After checkout,
 Lake loads the package located in `subDir` (or the repository root if no
 subdirectory is specified).
 -/
-syntax fromClause :=
+public syntax fromClause :=
   " from " fromSource
 
 /-
 A `NameMap String` of Lake options used to configure the dependency.
 This is equivalent to passing `-K` options to the dependency on the command line.
 -/
-syntax withClause :=
+public syntax withClause :=
   " with " term
 
-syntax verSpec :=
+public syntax verSpec :=
   &"git "? term:max
 
 /--
 The version of the package to require.
 To specify a Git revision, use the syntax `@ git <rev>`.
 -/
-syntax verClause :=
+public syntax verClause :=
   " @ " verSpec
 
-syntax depName :=
+public syntax depName :=
   atomic(str " / ")? identOrStr
 
-syntax depSpec :=
+public syntax depSpec :=
   depName (verClause)? (fromClause)? (withClause)?
 
 /--
@@ -193,7 +191,7 @@ public instance : Coe RequireDecl Command where
 Syntax for declaring Lake targets and facets.
 -/
 
-syntax buildDeclSig :=
+public syntax buildDeclSig :=
   identOrStr (ppSpace simpleBinder)? Term.typeSpec declValSimple
 
 /-!
@@ -343,7 +341,7 @@ public instance : Coe InputDirCommand Command where
 ## External Library Target Declaration
 -/
 
-syntax externLibDeclSpec :=
+public syntax externLibDeclSpec :=
   identOrStr (ppSpace simpleBinder)? declValSimple
 
 /--
@@ -370,7 +368,7 @@ scoped syntax (name := externLibCommand)
 DSL definitions to define a Lake script for a package.
 -/
 
-syntax scriptDeclSpec :=
+public syntax scriptDeclSpec :=
   identOrStr (ppSpace simpleBinder)? (declValSimple <|> declValDo)
 
 /--
@@ -413,8 +411,8 @@ namespace DSL
 Notation for specifying build keys in a package.
 -/
 
-syntax facetSuffix := atomic(":" noWs) ident
-syntax packageTargetLit := atomic("+" noWs)? ident
+public syntax facetSuffix := atomic(":" noWs) ident
+public syntax packageTargetLit := atomic("+" noWs)? ident
 
 /-- A module target key literal (with optional facet). -/
 scoped syntax:max (name := moduleTargetKeyLit)
@@ -437,7 +435,7 @@ The `do` command syntax groups multiple similarly indented commands together.
 The group can then be passed to another command that usually only accepts a
 single command (e.g., `meta if`).
 -/
-syntax cmdDo := ("do" many1Indent(command)) <|> command
+public syntax cmdDo := ("do" many1Indent(command)) <|> command
 
 /--
 The `meta if` command has two forms: