Skip to content

Commit 6f7ce27

Browse files
robsimmonstydeu
andauthored
chore: bump to 2026-07-12 (#887)
depHash and depTrace module facets are now documented, presetup is not as its doc comments indicate it is intended only for internal use --------- Co-authored-by: Mac Malone <tydeu@hatpress.net>
1 parent 7301a2b commit 6f7ce27

2 files changed

Lines changed: 12 additions & 1 deletion

File tree

Manual/BuildTools/Lake.lean

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -474,6 +474,8 @@ module.c
474474
module.c.o
475475
module.c.o.export
476476
module.c.o.noexport
477+
module.depHash
478+
module.depTrace
477479
module.deps
478480
module.dynlib
479481
module.exportInfo
@@ -498,6 +500,7 @@ module.olean
498500
module.olean.private
499501
module.olean.server
500502
module.precompileImports
503+
module.presetup
501504
module.setup
502505
module.transImports
503506
-/
@@ -520,6 +523,14 @@ The facets available for modules are:
520523

521524
The module's dependencies (e.g., imports or shared libraries).
522525

526+
: `depHash`
527+
528+
A hash of a module's build dependencies (e.g., imports, source, plugins).
529+
530+
: `depTrace`
531+
532+
A Lake build trace data structure (i.e., composite hash and modification time) of a module's build dependencies (e.g., imports, source, plugins).
533+
523534
: `olean`
524535

525536
The module's {tech}[`.olean` file]. {TODO}[Once module system lands fully, add docs for `olean.private` and `olean.server`]

lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:nightly-2026-07-11
1+
leanprover/lean4:nightly-2026-07-12

0 commit comments

Comments
 (0)