feat: module system is no longer experimental (#11637)

This PR declares the module system as no longer experimental and makes
the `experimental.module` option a no-op, to be removed.

.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

script/lakefile.toml

@@ -1,5 +1,4 @@
 name = "scripts"
-leanOptions = { experimental.module = true }
 
 [[lean_exe]]
 name = "modulize"

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

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}]

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

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
 }

tests/lake/lakefile.toml

@@ -11,4 +11,3 @@ name = "lake"
 root = "LakeMain"
 needs = ["Lake"]
 supportInterpreter = true
-leanOptions.experimental.module = true

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
 

tests/lake/tests/module/dep/lakefile.toml

@@ -1,5 +1,4 @@
 name = "dep"
-leanOptions.experimental.module = true
 
 [[lean_lib]]
 name = "Dep.NoImportAll"

tests/lake/tests/module/lakefile.toml

@@ -1,6 +1,5 @@
 name = "test"
 defaultTargets = ["Test"]
-leanOptions.experimental.module = true
 
 [[lean_lib]]
 name = "Test"

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.*"]

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"

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 -/

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

tests/pkg/def_clash/deps/fooA/lakefile.toml

@@ -2,4 +2,3 @@ name = "fooA"
 
 [[lean_lib]]
 name = "FooA"
-leanOptions.experimental.module = true

tests/pkg/def_clash/deps/fooB/lakefile.toml

@@ -2,4 +2,3 @@ name = "fooB"
 
 [[lean_lib]]
 name = "FooB"
-leanOptions.experimental.module = true

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"

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"

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"

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"

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"

tests/pkg/mod_clash/lakefile.toml

@@ -2,7 +2,6 @@ name = "test"
 
 [[lean_lib]]
 name = "Test"
-leanOptions.experimental.module = true
 
 [[require]]
 name = "depA"

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 }

tests/pkg/rebuild/lakefile.toml

@@ -3,4 +3,3 @@ defaultTargets = ["Rebuild"]
 
 [[lean_lib]]
 name = "Rebuild"
-leanOptions = { experimental.module = true }

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"]

tests/pkg/ver_clash/DiamondExample-A/lakefile.toml

@@ -3,4 +3,3 @@ defaultTargets = ["DiamondExampleA"]
 
 [[lean_lib]]
 name = "DiamondExampleA"
-leanOptions.experimental.module = true

tests/pkg/ver_clash/DiamondExample-B/lakefile.toml

@@ -8,4 +8,3 @@ rev = "v1"
 
 [[lean_lib]]
 name = "DiamondExampleB"
-leanOptions.experimental.module = true

tests/pkg/ver_clash/DiamondExample-C/lakefile.toml

@@ -8,4 +8,3 @@ rev = "v2"
 
 [[lean_lib]]
 name = "DiamondExampleC"
-leanOptions.experimental.module = true

tests/pkg/ver_clash/DiamondExample-D/lakefile.toml

@@ -13,4 +13,3 @@ rev = "v2"
 
 [[lean_lib]]
 name = "DiamondExampleD"
-leanOptions.experimental.module = true