Skip to content

Commit d30347c

Browse files
david-christiansendavid-christiansen
authored
chore: bump to nightly-2026-09-06 (#938)
1 parent 435f881 commit d30347c

4 files changed

Lines changed: 29 additions & 5 deletions

File tree

‎Manual/BuildTools/Lake.lean‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -728,6 +728,7 @@ root = "Tests"
728728
weakLinkArgs := #[],
729729
backend := Lake.Backend.default,
730730
platformIndependent := none,
731+
precompileImports := false,
731732
dynlibs := #[],
732733
plugins := #[],
733734
requiresModuleSystem := false,
@@ -793,6 +794,7 @@ root = "Tests"
793794
weakLinkArgs := #[],
794795
backend := Lake.Backend.default,
795796
platformIndependent := none,
797+
precompileImports := false,
796798
dynlibs := #[],
797799
plugins := #[],
798800
requiresModuleSystem := false,
@@ -828,6 +830,7 @@ root = "Tests"
828830
weakLinkArgs := #[],
829831
backend := Lake.Backend.default,
830832
platformIndependent := none,
833+
precompileImports := false,
831834
dynlibs := #[],
832835
plugins := #[],
833836
requiresModuleSystem := false,
@@ -893,6 +896,7 @@ lean_exe «my-package-tests» where
893896
weakLinkArgs := #[],
894897
backend := Lake.Backend.default,
895898
platformIndependent := none,
899+
precompileImports := false,
896900
dynlibs := #[],
897901
plugins := #[],
898902
requiresModuleSystem := false,
@@ -958,6 +962,7 @@ lean_exe «my-package-tests» where
958962
weakLinkArgs := #[],
959963
backend := Lake.Backend.default,
960964
platformIndependent := none,
965+
precompileImports := false,
961966
dynlibs := #[],
962967
plugins := #[],
963968
requiresModuleSystem := false,
@@ -993,6 +998,7 @@ lean_exe «my-package-tests» where
993998
weakLinkArgs := #[],
994999
backend := Lake.Backend.default,
9951000
platformIndependent := none,
1001+
precompileImports := false,
9961002
dynlibs := #[],
9971003
plugins := #[],
9981004
requiresModuleSystem := false,
@@ -1098,6 +1104,7 @@ root = "Lint"
10981104
weakLinkArgs := #[],
10991105
backend := Lake.Backend.default,
11001106
platformIndependent := none,
1107+
precompileImports := false,
11011108
dynlibs := #[],
11021109
plugins := #[],
11031110
requiresModuleSystem := false,
@@ -1163,6 +1170,7 @@ root = "Lint"
11631170
weakLinkArgs := #[],
11641171
backend := Lake.Backend.default,
11651172
platformIndependent := none,
1173+
precompileImports := false,
11661174
dynlibs := #[],
11671175
plugins := #[],
11681176
requiresModuleSystem := false,
@@ -1198,6 +1206,7 @@ root = "Lint"
11981206
weakLinkArgs := #[],
11991207
backend := Lake.Backend.default,
12001208
platformIndependent := none,
1209+
precompileImports := false,
12011210
dynlibs := #[],
12021211
plugins := #[],
12031212
requiresModuleSystem := false,
@@ -1264,6 +1273,7 @@ lean_exe «my-package-lint» where
12641273
weakLinkArgs := #[],
12651274
backend := Lake.Backend.default,
12661275
platformIndependent := none,
1276+
precompileImports := false,
12671277
dynlibs := #[],
12681278
plugins := #[],
12691279
requiresModuleSystem := false,
@@ -1329,6 +1339,7 @@ lean_exe «my-package-lint» where
13291339
weakLinkArgs := #[],
13301340
backend := Lake.Backend.default,
13311341
platformIndependent := none,
1342+
precompileImports := false,
13321343
dynlibs := #[],
13331344
plugins := #[],
13341345
requiresModuleSystem := false,
@@ -1364,6 +1375,7 @@ lean_exe «my-package-lint» where
13641375
weakLinkArgs := #[],
13651376
backend := Lake.Backend.default,
13661377
platformIndependent := none,
1378+
precompileImports := false,
13671379
dynlibs := #[],
13681380
plugins := #[],
13691381
requiresModuleSystem := false,

‎Manual/BuildTools/Lake/Config.lean‎

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ These options control the top-level directory layout of the package and its buil
9696
Further paths specified by libraries, executables, and targets within the package are relative to these directories.
9797
:::
9898

99-
:::tomlFieldCategory "Building and Running" defaultTargets leanLibDir platformIndependent precompileModules moreServerOptions moreGlobalServerArgs buildType leanOptions moreLeanArgs weakLeanArgs moreLeancArgs weakLeancArgs moreLinkArgs weakLinkArgs extraDepTargets
99+
:::tomlFieldCategory "Building and Running" defaultTargets leanLibDir platformIndependent precompileModules precompileImports moreServerOptions moreGlobalServerArgs buildType leanOptions moreLeanArgs weakLeanArgs moreLeancArgs weakLeancArgs moreLinkArgs weakLinkArgs extraDepTargets
100100

101101
These options configure how code is built and run in the package.
102102
Libraries, executables, and other {tech}[targets] within a package can further add to parts of this configuration.
@@ -158,6 +158,7 @@ name = "example-package"
158158
weakLinkArgs := #[],
159159
backend := Lake.Backend.default,
160160
platformIndependent := none,
161+
precompileImports := false,
161162
dynlibs := #[],
162163
plugins := #[],
163164
requiresModuleSystem := false,
@@ -250,6 +251,7 @@ name = "Sorting"
250251
weakLinkArgs := #[],
251252
backend := Lake.Backend.default,
252253
platformIndependent := none,
254+
precompileImports := false,
253255
dynlibs := #[],
254256
plugins := #[],
255257
requiresModuleSystem := false,
@@ -315,6 +317,7 @@ name = "Sorting"
315317
weakLinkArgs := #[],
316318
backend := Lake.Backend.default,
317319
platformIndependent := none,
320+
precompileImports := false,
318321
dynlibs := #[],
319322
plugins := #[],
320323
requiresModuleSystem := false,
@@ -326,6 +329,7 @@ name = "Sorting"
326329
libPrefixOnWindows := false,
327330
needs := #[],
328331
extraDepTargets := #[],
332+
precompileLibrary := false,
329333
precompileModules := false,
330334
defaultFacets := #[`lean_lib.leanArts],
331335
nativeFacets := #<fun>,
@@ -354,6 +358,7 @@ name = "Sorting"
354358
weakLinkArgs := #[],
355359
backend := Lake.Backend.default,
356360
platformIndependent := none,
361+
precompileImports := false,
357362
dynlibs := #[],
358363
plugins := #[],
359364
requiresModuleSystem := false,
@@ -365,6 +370,7 @@ name = "Sorting"
365370
libPrefixOnWindows := false,
366371
needs := #[],
367372
extraDepTargets := #[],
373+
precompileLibrary := false,
368374
precompileModules := false,
369375
defaultFacets := #[`lean_lib.leanArts],
370376
nativeFacets := #<fun>,
@@ -589,6 +595,7 @@ name = "TacticTools"
589595
weakLinkArgs := #[],
590596
backend := Lake.Backend.default,
591597
platformIndependent := none,
598+
precompileImports := false,
592599
dynlibs := #[],
593600
plugins := #[],
594601
requiresModuleSystem := false,
@@ -600,6 +607,7 @@ name = "TacticTools"
600607
libPrefixOnWindows := false,
601608
needs := #[],
602609
extraDepTargets := #[],
610+
precompileLibrary := false,
603611
precompileModules := false,
604612
defaultFacets := #[`lean_lib.leanArts],
605613
nativeFacets := #<fun>,
@@ -634,6 +642,7 @@ precompileModules = true
634642
weakLinkArgs := #[],
635643
backend := Lake.Backend.default,
636644
platformIndependent := none,
645+
precompileImports := false,
637646
dynlibs := #[],
638647
plugins := #[],
639648
requiresModuleSystem := false,
@@ -645,6 +654,7 @@ precompileModules = true
645654
libPrefixOnWindows := false,
646655
needs := #[],
647656
extraDepTargets := #[],
657+
precompileLibrary := false,
648658
precompileModules := true,
649659
defaultFacets := #[`lean_lib.leanArts],
650660
nativeFacets := #<fun>,
@@ -687,6 +697,7 @@ name = "trustworthytool"
687697
weakLinkArgs := #[],
688698
backend := Lake.Backend.default,
689699
platformIndependent := none,
700+
precompileImports := false,
690701
dynlibs := #[],
691702
plugins := #[],
692703
requiresModuleSystem := false,
@@ -737,6 +748,7 @@ exeName = "tt"
737748
weakLinkArgs := #[],
738749
backend := Lake.Backend.default,
739750
platformIndependent := none,
751+
precompileImports := false,
740752
dynlibs := #[],
741753
plugins := #[],
742754
requiresModuleSystem := false,
@@ -958,7 +970,7 @@ The fields of {keywordOf Lake.DSL.leanExeCommand}`lean_exe` are those of the {na
958970

959971
Because external libraries may be written in any language and require arbitrary build steps, they are defined as programs written in the {name Lake.FetchM}`FetchM` monad that produce a {name Lake.Job}`Job`.
960972
External library targets should produce a build job that carries out the build and then returns the location of the resulting static library.
961-
For the external library to link properly when {name Lake.PackageConfig.precompileModules}`precompileModules` is on, the static library produced by an {keyword}`extern_lib` target must follow the platform's naming conventions for libraries (i.e., be named foo.a on Windows or libfoo.a on Unix-like systems).
973+
For the external library to link properly when {name Lake.LeanConfig.precompileImports}`precompileImports` or {name Lake.PackageConfig.precompileModules}`precompileModules` is on, the static library produced by an {keyword}`extern_lib` target must follow the platform's naming conventions for libraries (i.e., be named `foo.a` on Windows or `libfoo.a` on Unix-like systems).
962974
The utility function {name}`Lake.nameToStaticLib` converts a library name into its proper file name for current platform.
963975

964976
:::syntax command (title := "External Library Targets")

‎lake-manifest.json‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "",
8-
"rev": "796cfdb6eb682e191fb0ccc7da9de4b018dd7f0d",
8+
"rev": "9b1360c8452066f24c19c09892a16c59a01b5a03",
99
"name": "verso",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": "nightly-testing",
@@ -55,7 +55,7 @@
5555
"type": "git",
5656
"subDir": null,
5757
"scope": "",
58-
"rev": "fda188f7329fa18ce4b2e8cc96c9b0a8f0c78c46",
58+
"rev": "9b90b7f938d6169246325df002351014f49945ef",
5959
"name": "subverso",
6060
"manifestFile": "lake-manifest.json",
6161
"inputRev": "main",

‎lean-toolchain‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:nightly-2026-09-05
1+
leanprover/lean4:nightly-2026-09-06

0 commit comments

Comments
 (0)