Skip to content

Commit 1f80b3f

Browse files
KhaKha
authored
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.
1 parent de388a7 commit 1f80b3f

File tree

29 files changed

+23
-57
lines changed

29 files changed

+23
-57
lines changed

‎.github/workflows/build-template.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -220,7 +220,7 @@ jobs:
220220
path: pack/*
221221
- name: Lean stats
222222
run: |
223-
build/$TARGET_STAGE/bin/lean --stats src/Lean.lean -Dexperimental.module=true
223+
build/$TARGET_STAGE/bin/lean --stats src/Lean.lean
224224
if: ${{ !matrix.cross }}
225225
- name: Test
226226
id: test

‎script/lakefile.toml‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
name = "scripts"
2-
leanOptions = { experimental.module = true }
32

43
[[lean_exe]]
54
name = "modulize"

‎src/Lean/Language/Lean.lean‎

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -355,10 +355,10 @@ private def getNiceCommandStartPos? (stx : Syntax) : Option String.Pos.Raw := do
355355
stx := stx[1]
356356
stx.getPos?
357357

358-
/-- Allow use of module system -/
358+
/-- No-op, deprecated -/
359359
register_builtin_option experimental.module : Bool := {
360360
defValue := false
361-
descr := "Allow use of module system (experimental)"
361+
descr := "no-op, deprecated"
362362
}
363363

364364
/--
@@ -494,11 +494,6 @@ where
494494

495495
let startTime := (← IO.monoNanosNow).toFloat / 1000000000
496496
let mut opts := setup.opts
497-
-- HACK: no better way to enable in core with `USE_LAKE` off
498-
if setup.mainModuleName.getRoot ∈ [`Init, `Std, `Lean, `Lake, `LakeMain] then
499-
opts := experimental.module.setIfNotSet opts true
500-
if !stx.raw[0].isNone && !experimental.module.get opts then
501-
throw <| IO.Error.userError "`module` keyword is experimental and not enabled here"
502497
-- allows `headerEnv` to be leaked, which would live until the end of the process anyway
503498
let (headerEnv, msgLog) ← Elab.processHeaderCore (leakEnv := true)
504499
stx.startPos setup.imports setup.isModule setup.opts .empty ctx.toInputContext

‎src/lakefile.toml.in‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -40,8 +40,6 @@ leanLibDir = "lib/lean"
4040
# Destination for static libraries
4141
nativeLibDir = "lib/lean"
4242

43-
leanOptions = { experimental.module = true }
44-
4543
# Additional options derived from the CMake configuration
4644
# For example, CI will set `-DwarningAsError=true` through this
4745
moreLeanArgs = [${LEAN_EXTRA_OPTS_TOML}]

‎tests/bench/speedcenter.exec.velcom.yaml‎

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -18,42 +18,42 @@
1818
run_config:
1919
<<: *time
2020
cwd: ../../src
21-
cmd: lean -Dexperimental.module=true Init/Prelude.lean
21+
cmd: lean Init/Prelude.lean
2222
- attributes:
2323
description: Init.Data.List.Sublist async
2424
tags: [other]
2525
run_config:
2626
<<: *time
2727
cwd: ../../src
28-
cmd: lean -Dexperimental.module=true Init/Data/List/Sublist.lean
28+
cmd: lean Init/Data/List/Sublist.lean
2929
- attributes:
3030
description: Std.Data.Internal.List.Associative
3131
tags: [other]
3232
run_config:
3333
<<: *time
3434
cwd: ../../src
35-
cmd: lean -Dexperimental.module=true Std/Data/Internal/List/Associative.lean
35+
cmd: lean Std/Data/Internal/List/Associative.lean
3636
- attributes:
3737
description: Std.Data.DHashMap.Internal.RawLemmas
3838
tags: [other]
3939
run_config:
4040
<<: *time
4141
cwd: ../../src
42-
cmd: lean -Dexperimental.module=true Std/Data/DHashMap/Internal/RawLemmas.lean
42+
cmd: lean Std/Data/DHashMap/Internal/RawLemmas.lean
4343
- attributes:
4444
description: Init.Data.BitVec.Lemmas
4545
tags: [other]
4646
run_config:
4747
<<: *time
4848
cwd: ../../src
49-
cmd: lean -Dexperimental.module=true Init/Data/BitVec/Lemmas.lean
49+
cmd: lean Init/Data/BitVec/Lemmas.lean
5050
- attributes:
5151
description: Init.Data.List.Sublist re-elab -j4
5252
tags: [other]
5353
run_config:
5454
<<: *time
5555
cwd: ../../src
56-
cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/List/Sublist.lean 10 -j4 -Dexperimental.module=true
56+
cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/List/Sublist.lean 10 -j4
5757
max_runs: 2
5858
parse_output: true
5959
- attributes:
@@ -62,7 +62,7 @@
6262
run_config:
6363
<<: *time
6464
cwd: ../../src
65-
cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/BitVec/Lemmas.lean 3 -j4 -Dexperimental.module=true
65+
cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/BitVec/Lemmas.lean 3 -j4
6666
max_runs: 2
6767
parse_output: true
6868
- attributes:
@@ -71,7 +71,7 @@
7171
run_config:
7272
<<: *time
7373
cwd: ../../src
74-
cmd: lean --run ../script/benchReelabWatchdogRss.lean lean Init/Data/List/Sublist.lean 10 -j4 -Dexperimental.module=true
74+
cmd: lean --run ../script/benchReelabWatchdogRss.lean lean Init/Data/List/Sublist.lean 10 -j4
7575
max_runs: 2
7676
parse_output: true
7777
# This benchmark uncovered the promise cycle in `realizeConst` (#11328)
@@ -81,7 +81,7 @@
8181
run_config:
8282
<<: *time
8383
cwd: ../../src
84-
cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/List/Basic.lean 10 -j4 -Dexperimental.module=true
84+
cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/List/Basic.lean 10 -j4
8585
max_runs: 2
8686
parse_output: true
8787
- attributes:
@@ -471,7 +471,7 @@
471471
tags: [other]
472472
run_config:
473473
<<: *time
474-
cmd: lean -Dexperimental.module=true workspaceSymbols.lean
474+
cmd: lean workspaceSymbols.lean
475475
max_runs: 2
476476
- attributes:
477477
description: bv_decide_realworld
@@ -620,16 +620,16 @@
620620
tags: [other]
621621
run_config:
622622
<<: *time
623-
cmd: lean -Dexperimental.module=true ../lean/run/grind_bitvec2.lean
623+
cmd: lean ../lean/run/grind_bitvec2.lean
624624
- attributes:
625625
description: grind_list2.lean
626626
tags: [other]
627627
run_config:
628628
<<: *time
629-
cmd: lean -Dexperimental.module=true ../lean/run/grind_list2.lean
629+
cmd: lean ../lean/run/grind_list2.lean
630630
- attributes:
631631
description: grind_ring_5.lean
632632
tags: [other]
633633
run_config:
634634
<<: *time
635-
cmd: lean -Dexperimental.module=true ../lean/run/grind_ring_5.lean
635+
cmd: lean ../lean/run/grind_ring_5.lean

‎tests/common.sh‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ function lean_has_llvm_support {
2525
}
2626

2727
function compile_lean_c_backend {
28-
lean -Dexperimental.module=true --c="$f.c" "$f" || fail "Failed to compile $f into C file"
28+
lean --c="$f.c" "$f" || fail "Failed to compile $f into C file"
2929
leanc ${LEANC_OPTS-} -O3 -DNDEBUG -o "$f.out" "$@" "$f.c" || fail "Failed to compile C file $f.c"
3030
}
3131

@@ -34,7 +34,7 @@ function compile_lean_llvm_backend {
3434
rm "*.ll" || true # remove debugging files.
3535
rm "*.bc" || true # remove bitcode files
3636
rm "*.o" || true # remove object files
37-
lean -Dexperimental.module=true --bc="$f.linked.bc" "$f" || fail "Failed to compile $f into bitcode file"
37+
lean --bc="$f.linked.bc" "$f" || fail "Failed to compile $f into bitcode file"
3838
leanc ${LEANC_OPTS-} -O3 -DNDEBUG -o "$f.out" "$@" "$f.linked.bc" || fail "Failed to link object file '$f.linked.bc'"
3939
set +o xtrace
4040
}

‎tests/lake/lakefile.toml‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,4 +11,3 @@ name = "lake"
1111
root = "LakeMain"
1212
needs = ["Lake"]
1313
supportInterpreter = true
14-
leanOptions.experimental.module = true

‎tests/lake/tests/cache/lakefile.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,7 @@ package test where
77

88
lean_lib Test
99

10-
lean_lib Module where
11-
leanOptions := #[⟨`experimental.module, true⟩]
10+
lean_lib Module
1211

1312
lean_lib Ignored
1413

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
name = "dep"
2-
leanOptions.experimental.module = true
32

43
[[lean_lib]]
54
name = "Dep.NoImportAll"

‎tests/lake/tests/module/lakefile.toml‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
name = "test"
22
defaultTargets = ["Test"]
3-
leanOptions.experimental.module = true
43

54
[[lean_lib]]
65
name = "Test"

0 commit comments

Comments
 (0)