diff --git a/.github/workflows/build-template.yml b/.github/workflows/build-template.yml
index 4579e6fa07ac..68d4a50f8fef 100644
--- a/.github/workflows/build-template.yml
+++ b/.github/workflows/build-template.yml
@@ -220,7 +220,7 @@ jobs:
           path: pack/*
       - name: Lean stats
         run: |
-          build/$TARGET_STAGE/bin/lean --stats src/Lean.lean -Dexperimental.module=true
+          build/$TARGET_STAGE/bin/lean --stats src/Lean.lean
         if: ${{ !matrix.cross }}
       - name: Test
         id: test
diff --git a/script/lakefile.toml b/script/lakefile.toml
index 5a4049f5b342..71c97b2930e7 100644
--- a/script/lakefile.toml
+++ b/script/lakefile.toml
@@ -1,5 +1,4 @@
 name = "scripts"
-leanOptions = { experimental.module = true }
 
 [[lean_exe]]
 name = "modulize"
diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index b8af3376f0d2..92c1dbfdcb5e 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -355,10 +355,10 @@ private def getNiceCommandStartPos? (stx : Syntax) : Option String.Pos.Raw := do
     stx := stx[1]
   stx.getPos?
 
-/-- Allow use of module system -/
+/-- No-op, deprecated -/
 register_builtin_option experimental.module : Bool := {
   defValue := false
-  descr := "Allow use of module system (experimental)"
+  descr := "no-op, deprecated"
 }
 
 /--
@@ -494,11 +494,6 @@ where
 
       let startTime := (← IO.monoNanosNow).toFloat / 1000000000
       let mut opts := setup.opts
-      -- HACK: no better way to enable in core with `USE_LAKE` off
-      if setup.mainModuleName.getRoot ∈ [`Init, `Std, `Lean, `Lake, `LakeMain] then
-        opts := experimental.module.setIfNotSet opts true
-      if !stx.raw[0].isNone && !experimental.module.get opts then
-        throw <| IO.Error.userError "`module` keyword is experimental and not enabled here"
       -- allows `headerEnv` to be leaked, which would live until the end of the process anyway
       let (headerEnv, msgLog) ← Elab.processHeaderCore (leakEnv := true)
         stx.startPos setup.imports setup.isModule setup.opts .empty ctx.toInputContext
diff --git a/src/lakefile.toml.in b/src/lakefile.toml.in
index 758b397f0317..51f1c94605d6 100644
--- a/src/lakefile.toml.in
+++ b/src/lakefile.toml.in
@@ -40,8 +40,6 @@ leanLibDir = "lib/lean"
 # Destination for static libraries
 nativeLibDir = "lib/lean"
 
-leanOptions = { experimental.module = true }
-
 # Additional options derived from the CMake configuration
 # For example, CI will set `-DwarningAsError=true` through this
 moreLeanArgs = [${LEAN_EXTRA_OPTS_TOML}]
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index 3b38f17a5ca2..e06e242804de 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -18,42 +18,42 @@
   run_config:
     <<: *time
     cwd: ../../src
-    cmd: lean -Dexperimental.module=true Init/Prelude.lean
+    cmd: lean Init/Prelude.lean
 - attributes:
     description: Init.Data.List.Sublist async
     tags: [other]
   run_config:
     <<: *time
     cwd: ../../src
-    cmd: lean -Dexperimental.module=true Init/Data/List/Sublist.lean
+    cmd: lean Init/Data/List/Sublist.lean
 - attributes:
     description: Std.Data.Internal.List.Associative
     tags: [other]
   run_config:
     <<: *time
     cwd: ../../src
-    cmd: lean -Dexperimental.module=true Std/Data/Internal/List/Associative.lean
+    cmd: lean Std/Data/Internal/List/Associative.lean
 - attributes:
     description: Std.Data.DHashMap.Internal.RawLemmas
     tags: [other]
   run_config:
     <<: *time
     cwd: ../../src
-    cmd: lean -Dexperimental.module=true Std/Data/DHashMap/Internal/RawLemmas.lean
+    cmd: lean Std/Data/DHashMap/Internal/RawLemmas.lean
 - attributes:
     description: Init.Data.BitVec.Lemmas
     tags: [other]
   run_config:
     <<: *time
     cwd: ../../src
-    cmd: lean -Dexperimental.module=true Init/Data/BitVec/Lemmas.lean
+    cmd: lean Init/Data/BitVec/Lemmas.lean
 - attributes:
     description: Init.Data.List.Sublist re-elab -j4
     tags: [other]
   run_config:
     <<: *time
     cwd: ../../src
-    cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/List/Sublist.lean 10 -j4 -Dexperimental.module=true
+    cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/List/Sublist.lean 10 -j4
     max_runs: 2
     parse_output: true
 - attributes:
@@ -62,7 +62,7 @@
   run_config:
     <<: *time
     cwd: ../../src
-    cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/BitVec/Lemmas.lean 3 -j4 -Dexperimental.module=true
+    cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/BitVec/Lemmas.lean 3 -j4
     max_runs: 2
     parse_output: true
 - attributes:
@@ -71,7 +71,7 @@
   run_config:
     <<: *time
     cwd: ../../src
-    cmd: lean --run ../script/benchReelabWatchdogRss.lean lean Init/Data/List/Sublist.lean 10 -j4 -Dexperimental.module=true
+    cmd: lean --run ../script/benchReelabWatchdogRss.lean lean Init/Data/List/Sublist.lean 10 -j4
     max_runs: 2
     parse_output: true
 # This benchmark uncovered the promise cycle in `realizeConst` (#11328)
@@ -81,7 +81,7 @@
   run_config:
     <<: *time
     cwd: ../../src
-    cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/List/Basic.lean 10 -j4 -Dexperimental.module=true
+    cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/List/Basic.lean 10 -j4
     max_runs: 2
     parse_output: true
 - attributes:
@@ -471,7 +471,7 @@
     tags: [other]
   run_config:
     <<: *time
-    cmd: lean -Dexperimental.module=true workspaceSymbols.lean
+    cmd: lean workspaceSymbols.lean
     max_runs: 2
 - attributes:
     description: bv_decide_realworld
@@ -620,16 +620,16 @@
     tags: [other]
   run_config:
     <<: *time
-    cmd: lean -Dexperimental.module=true ../lean/run/grind_bitvec2.lean
+    cmd: lean ../lean/run/grind_bitvec2.lean
 - attributes:
     description: grind_list2.lean
     tags: [other]
   run_config:
     <<: *time
-    cmd: lean -Dexperimental.module=true ../lean/run/grind_list2.lean
+    cmd: lean ../lean/run/grind_list2.lean
 - attributes:
     description: grind_ring_5.lean
     tags: [other]
   run_config:
     <<: *time
-    cmd: lean -Dexperimental.module=true ../lean/run/grind_ring_5.lean
+    cmd: lean ../lean/run/grind_ring_5.lean
diff --git a/tests/common.sh b/tests/common.sh
index 52756c06f373..a5759abe1441 100644
--- a/tests/common.sh
+++ b/tests/common.sh
@@ -25,7 +25,7 @@ function lean_has_llvm_support {
 }
 
 function compile_lean_c_backend {
-    lean -Dexperimental.module=true --c="$f.c" "$f" || fail "Failed to compile $f into C file"
+    lean --c="$f.c" "$f" || fail "Failed to compile $f into C file"
     leanc ${LEANC_OPTS-} -O3 -DNDEBUG -o "$f.out" "$@" "$f.c" || fail "Failed to compile C file $f.c"
 }
 
@@ -34,7 +34,7 @@ function compile_lean_llvm_backend {
     rm "*.ll" || true # remove debugging files.
     rm "*.bc" || true # remove bitcode files
     rm "*.o" || true # remove object files
-    lean -Dexperimental.module=true --bc="$f.linked.bc" "$f" || fail "Failed to compile $f into bitcode file"
+    lean --bc="$f.linked.bc" "$f" || fail "Failed to compile $f into bitcode file"
     leanc ${LEANC_OPTS-} -O3 -DNDEBUG -o "$f.out" "$@" "$f.linked.bc" || fail "Failed to link object file '$f.linked.bc'"
     set +o xtrace
 }
diff --git a/tests/lake/lakefile.toml b/tests/lake/lakefile.toml
index f76bf1f8231b..42e7e7bc416d 100644
--- a/tests/lake/lakefile.toml
+++ b/tests/lake/lakefile.toml
@@ -11,4 +11,3 @@ name = "lake"
 root = "LakeMain"
 needs = ["Lake"]
 supportInterpreter = true
-leanOptions.experimental.module = true
diff --git a/tests/lake/tests/cache/lakefile.lean b/tests/lake/tests/cache/lakefile.lean
index 2d49a6424312..cf963d9c46cb 100644
--- a/tests/lake/tests/cache/lakefile.lean
+++ b/tests/lake/tests/cache/lakefile.lean
@@ -7,8 +7,7 @@ package test where
 
 lean_lib Test
 
-lean_lib Module where
-  leanOptions := #[⟨`experimental.module, true⟩]
+lean_lib Module
 
 lean_lib Ignored
 
diff --git a/tests/lake/tests/module/dep/lakefile.toml b/tests/lake/tests/module/dep/lakefile.toml
index 455e6d8076d6..f9b0c3f2513e 100644
--- a/tests/lake/tests/module/dep/lakefile.toml
+++ b/tests/lake/tests/module/dep/lakefile.toml
@@ -1,5 +1,4 @@
 name = "dep"
-leanOptions.experimental.module = true
 
 [[lean_lib]]
 name = "Dep.NoImportAll"
diff --git a/tests/lake/tests/module/lakefile.toml b/tests/lake/tests/module/lakefile.toml
index 285f1b0ccd17..824dcd4b3e7c 100644
--- a/tests/lake/tests/module/lakefile.toml
+++ b/tests/lake/tests/module/lakefile.toml
@@ -1,6 +1,5 @@
 name = "test"
 defaultTargets = ["Test"]
-leanOptions.experimental.module = true
 
 [[lean_lib]]
 name = "Test"
diff --git a/tests/lakefile.toml b/tests/lakefile.toml
index 1623d16a3471..7b462676214d 100644
--- a/tests/lakefile.toml
+++ b/tests/lakefile.toml
@@ -1,9 +1,5 @@
 name = "tests"
 
-# Allow `module` in tests when opened in the language server.
-# Enabled during actual test runs in the respective test_single.sh.
-moreGlobalServerArgs = ["-Dexperimental.module=true"]
-
 [[lean_lib]]
 name = "Tests"
 globs = ["lean.*"]
diff --git a/tests/lean/run/test_single.sh b/tests/lean/run/test_single.sh
index b2cbed7288e4..64705ca4a6d3 100755
--- a/tests/lean/run/test_single.sh
+++ b/tests/lean/run/test_single.sh
@@ -3,4 +3,4 @@ source ../../common.sh
 
 # `--root` to infer same private names as in the server
 # Elab.inServer to allow for arbitrary `#eval`
-exec_check_raw lean --root=../.. -Dlinter.all=false -Dexperimental.module=true -DElab.inServer=true "$f"
+exec_check_raw lean --root=../.. -Dlinter.all=false -DElab.inServer=true "$f"
diff --git a/tests/lean/run/whereCmd.lean b/tests/lean/run/whereCmd.lean
index 9fdb4fe4dd16..778df8b31a59 100644
--- a/tests/lean/run/whereCmd.lean
+++ b/tests/lean/run/whereCmd.lean
@@ -5,7 +5,6 @@ import Lean
 
 -- Restore the options to a pristine state
 set_option internal.cmdlineSnapshots false
-set_option experimental.module false
 set_option Elab.inServer false
 
 /-- info: -- In root namespace with initial scope -/
diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh
index 8ff0c2110be2..12d20dedbb9e 100755
--- a/tests/lean/test_single.sh
+++ b/tests/lean/test_single.sh
@@ -4,5 +4,5 @@ source ../common.sh
 # these tests don't have to succeed
 # `--root` to infer same private names as in the server
 # Elab.inServer to allow for arbitrary `#eval`
-exec_capture lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -Dexperimental.module=true -DElab.inServer=true "$f" || true
+exec_capture lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -DElab.inServer=true "$f" || true
 diff_produced
diff --git a/tests/pkg/def_clash/deps/fooA/lakefile.toml b/tests/pkg/def_clash/deps/fooA/lakefile.toml
index 337fe19f76bb..604c25986b99 100644
--- a/tests/pkg/def_clash/deps/fooA/lakefile.toml
+++ b/tests/pkg/def_clash/deps/fooA/lakefile.toml
@@ -2,4 +2,3 @@ name = "fooA"
 
 [[lean_lib]]
 name = "FooA"
-leanOptions.experimental.module = true
diff --git a/tests/pkg/def_clash/deps/fooB/lakefile.toml b/tests/pkg/def_clash/deps/fooB/lakefile.toml
index 6e6d2d1fe9a9..2818f88678ca 100644
--- a/tests/pkg/def_clash/deps/fooB/lakefile.toml
+++ b/tests/pkg/def_clash/deps/fooB/lakefile.toml
@@ -2,4 +2,3 @@ name = "fooB"
 
 [[lean_lib]]
 name = "FooB"
-leanOptions.experimental.module = true
diff --git a/tests/pkg/def_clash/deps/useA/lakefile.toml b/tests/pkg/def_clash/deps/useA/lakefile.toml
index 95a4a95f2a3e..23b0a8156af1 100644
--- a/tests/pkg/def_clash/deps/useA/lakefile.toml
+++ b/tests/pkg/def_clash/deps/useA/lakefile.toml
@@ -2,7 +2,6 @@ name = "useA"
 
 [[lean_lib]]
 name = "UseA"
-leanOptions.experimental.module = true
 
 [[require]]
 name = "fooA"
diff --git a/tests/pkg/def_clash/deps/useB/lakefile.toml b/tests/pkg/def_clash/deps/useB/lakefile.toml
index 7a978c7ccd73..5bd8d59e493d 100644
--- a/tests/pkg/def_clash/deps/useB/lakefile.toml
+++ b/tests/pkg/def_clash/deps/useB/lakefile.toml
@@ -2,7 +2,6 @@ name = "useB"
 
 [[lean_lib]]
 name = "UseB"
-leanOptions.experimental.module = true
 
 [[require]]
 name = "fooB"
diff --git a/tests/pkg/def_clash/lakefile.toml b/tests/pkg/def_clash/lakefile.toml
index 94a4d5873656..614256996b53 100644
--- a/tests/pkg/def_clash/lakefile.toml
+++ b/tests/pkg/def_clash/lakefile.toml
@@ -2,19 +2,15 @@ name = "test"
 
 [[lean_lib]]
 name = "Test"
-leanOptions.experimental.module = true
 
 [[lean_lib]]
 name = "TestFoo"
-leanOptions.experimental.module = true
 
 [[lean_exe]]
 name = "TestUse"
-leanOptions.experimental.module = true
 
 [[lean_exe]]
 name = "TestLocalUse"
-leanOptions.experimental.module = true
 
 [[require]]
 name = "useA"
diff --git a/tests/pkg/mod_clash/depA/lakefile.toml b/tests/pkg/mod_clash/depA/lakefile.toml
index a987b57abce2..03a45afe0c7e 100644
--- a/tests/pkg/mod_clash/depA/lakefile.toml
+++ b/tests/pkg/mod_clash/depA/lakefile.toml
@@ -5,7 +5,6 @@ name = "Same"
 
 [[lean_lib]]
 name = "Similar"
-leanOptions.experimental.module = true
 
 [[lean_lib]]
 name = "Diff"
diff --git a/tests/pkg/mod_clash/depB/lakefile.toml b/tests/pkg/mod_clash/depB/lakefile.toml
index a987b57abce2..03a45afe0c7e 100644
--- a/tests/pkg/mod_clash/depB/lakefile.toml
+++ b/tests/pkg/mod_clash/depB/lakefile.toml
@@ -5,7 +5,6 @@ name = "Same"
 
 [[lean_lib]]
 name = "Similar"
-leanOptions.experimental.module = true
 
 [[lean_lib]]
 name = "Diff"
diff --git a/tests/pkg/mod_clash/lakefile.toml b/tests/pkg/mod_clash/lakefile.toml
index 3851e411e53e..ba506393d178 100644
--- a/tests/pkg/mod_clash/lakefile.toml
+++ b/tests/pkg/mod_clash/lakefile.toml
@@ -2,7 +2,6 @@ name = "test"
 
 [[lean_lib]]
 name = "Test"
-leanOptions.experimental.module = true
 
 [[require]]
 name = "depA"
diff --git a/tests/pkg/module/lakefile.toml b/tests/pkg/module/lakefile.toml
index 20fbd974757f..ce8144ecaf5e 100644
--- a/tests/pkg/module/lakefile.toml
+++ b/tests/pkg/module/lakefile.toml
@@ -4,4 +4,4 @@ defaultTargets = ["Module"]
 [[lean_lib]]
 name = "Module"
 # Elab.inServer to allow for arbitrary `#eval`
-leanOptions = { experimental.module = true, Elab.inServer = true }
+leanOptions = { Elab.inServer = true }
diff --git a/tests/pkg/rebuild/lakefile.toml b/tests/pkg/rebuild/lakefile.toml
index b5d7c7b45a68..cf42a8dd53b8 100644
--- a/tests/pkg/rebuild/lakefile.toml
+++ b/tests/pkg/rebuild/lakefile.toml
@@ -3,4 +3,3 @@ defaultTargets = ["Rebuild"]
 
 [[lean_lib]]
 name = "Rebuild"
-leanOptions = { experimental.module = true }
diff --git a/tests/pkg/structure_docstrings/lakefile.toml b/tests/pkg/structure_docstrings/lakefile.toml
index 4c0b776af5ce..7f151db26dcf 100644
--- a/tests/pkg/structure_docstrings/lakefile.toml
+++ b/tests/pkg/structure_docstrings/lakefile.toml
@@ -3,11 +3,10 @@ defaultTargets = ["StructureDocstrings", "StructureDocstringsTest"]
 
 [[lean_lib]]
 name = "StructureDocstrings"
-leanOptions = { experimental.module = true }
 roots = ["StructureDocstrings.A", "StructureDocstrings.B"]
 
 [[lean_lib]]
 name = "StructureDocstringsTest"
 # Elab.inServer to allow docstring tests to access .server level data
-leanOptions = { experimental.module = true, Elab.inServer = true }
+leanOptions = { Elab.inServer = true }
 roots = ["StructureDocstrings.C"]
diff --git a/tests/pkg/ver_clash/DiamondExample-A/lakefile.toml b/tests/pkg/ver_clash/DiamondExample-A/lakefile.toml
index 8a243dbdb783..050130fc9dd0 100644
--- a/tests/pkg/ver_clash/DiamondExample-A/lakefile.toml
+++ b/tests/pkg/ver_clash/DiamondExample-A/lakefile.toml
@@ -3,4 +3,3 @@ defaultTargets = ["DiamondExampleA"]
 
 [[lean_lib]]
 name = "DiamondExampleA"
-leanOptions.experimental.module = true
diff --git a/tests/pkg/ver_clash/DiamondExample-B/lakefile.toml b/tests/pkg/ver_clash/DiamondExample-B/lakefile.toml
index 4f634b3f6c25..5fbdc7651a9c 100644
--- a/tests/pkg/ver_clash/DiamondExample-B/lakefile.toml
+++ b/tests/pkg/ver_clash/DiamondExample-B/lakefile.toml
@@ -8,4 +8,3 @@ rev = "v1"
 
 [[lean_lib]]
 name = "DiamondExampleB"
-leanOptions.experimental.module = true
diff --git a/tests/pkg/ver_clash/DiamondExample-C/lakefile.toml b/tests/pkg/ver_clash/DiamondExample-C/lakefile.toml
index 8375cb8761bd..7ddb8769be82 100644
--- a/tests/pkg/ver_clash/DiamondExample-C/lakefile.toml
+++ b/tests/pkg/ver_clash/DiamondExample-C/lakefile.toml
@@ -8,4 +8,3 @@ rev = "v2"
 
 [[lean_lib]]
 name = "DiamondExampleC"
-leanOptions.experimental.module = true
diff --git a/tests/pkg/ver_clash/DiamondExample-D/lakefile.toml b/tests/pkg/ver_clash/DiamondExample-D/lakefile.toml
index 58c2f348e037..9c28f01f27fe 100644
--- a/tests/pkg/ver_clash/DiamondExample-D/lakefile.toml
+++ b/tests/pkg/ver_clash/DiamondExample-D/lakefile.toml
@@ -13,4 +13,3 @@ rev = "v2"
 
 [[lean_lib]]
 name = "DiamondExampleD"
-leanOptions.experimental.module = true