fix: run the HTML phase again when the analysis of its inputs changes

lakefile.lean

@@ -184,6 +184,21 @@ module_facet srcUri.file (mod) : String := makeModuleSrcUriFacet mod `srcUri.fil
 /-- The URI of the source code of the module, respecting `DOCGEN_SRC`. -/
 module_facet srcUri (mod) : String := makeModuleSrcUriFacet mod `srcUri
 
+/--
+Writes the marker file of a build step. The file contains the running hash computed as part of the
+current trace.
+
+When Lake builds a file with `buildFileUnlessUpToDate'`, it replaces the current trace with one that
+contains only the file. This means that downstream dependents of the file are not rebuilt if the
+file's dependencies change without the file itself changing (e.g., the private part of a module
+changes but the public interface is untouched). Marker files are proxies for a build having taken
+place, so they need to include data that changes whenever that build needs repeating, which is
+efficiently represented by the hash of the trace.
+-/
+def writeMarker (markerFile : FilePath) : JobM Unit := do
+  createParentDirs markerFile
+  IO.FS.writeFile markerFile (toString (← getTrace).hash)
+
 target bibPrepass : FilePath := do
   let exeJob ← «doc-gen4».fetch
   let buildDir := (← getRootPackage).buildDir
@@ -218,9 +233,9 @@ def coreTarget (component : Lean.Name) : FetchM (Job FilePath) := do
   let buildDir := (← getRootPackage).buildDir
   -- Building the core targets adds their information to the database file. While it would be
   -- possible to hash just the relevant content of the database (e.g. using SQLite's SHA3 module)
-  -- and write the result to a file, this adds a significant overhead. Instead, we create an empty
-  -- "marker file" to indicate that the database content has been inserted, and rely on its trace
-  -- changing to trigger rebuilds.
+  -- and write the result to a file, this adds a significant overhead. Instead, `writeMarker` writes
+  -- a marker file whose content is the hash of the dependency trace, so that the steps that depend
+  -- on the marker run again when the inputs change.
   let markerFile := buildDir / "doc-data" / s!"core-{component}.doc"
   bibPrepassJob.bindM fun _ => do
     exeJob.mapM fun exeFile => do
@@ -230,8 +245,7 @@ def coreTarget (component : Lean.Name) : FetchM (Job FilePath) := do
           args := #["genCore", "--build", buildDir.toString, component.toString, "api-docs.db"]
           env := ← getAugmentedEnv
         }
-        createParentDirs markerFile
-        IO.FS.writeFile markerFile ""
+        writeMarker markerFile
       return markerFile
 
 /--
@@ -262,9 +276,9 @@ module_facet docInfo (mod) : FilePath := do
   -- Building the documentation info for the module adds or updates the relevant content in the
   -- database. If the dependencies change, then this needs to be re-done. While it would be possible
   -- to hash just the relevant content of the database (e.g. using SQLite's SHA3 module) and write
-  -- the result to a file, this adds a significant overhead. Instead, we create an empty "marker
-  -- file" to indicate that the database content has been inserted, and rely on its Lake trace
-  -- changing to trigger rebuilds.
+  -- the result to a file, this adds a significant overhead. Instead, `writeMarker` writes a marker
+  -- file whose content is the hash of the dependency trace, so that the steps that depend on the
+  -- marker run again when the inputs change.
   let markerFile := buildDir / "doc-data" / s!"{mod.name}.doc"
   coreJob.bindM fun _ => do
     depDocJobs.bindM fun _ => do
@@ -279,8 +293,7 @@ module_facet docInfo (mod) : FilePath := do
                 args := #["single", "--build", buildDir.toString, mod.name.toString, "api-docs.db", srcUri]
                 env := ← getAugmentedEnv
               }
-              createParentDirs markerFile
-              IO.FS.writeFile markerFile ""
+              writeMarker markerFile
             return markerFile
 
 /--
@@ -323,8 +336,7 @@ library_facet docsHeader (lib) : FilePath := do
           cmd := exeFile.toString
           args := #["headerData", "--build", buildDir.toString]
         }
-        createParentDirs markerFile
-        IO.FS.writeFile markerFile ""
+        writeMarker markerFile
       return dataFile
 
 
@@ -381,8 +393,7 @@ def generateHtmlDocs (markerName : String) (rootMods : Array Module) (descriptio
               args := #["fromDb", "--build", buildDir.toString, "--manifest", manifestFile.toString, dbPath.toString] ++ rootNames.map (·.toString)
               env := ← getAugmentedEnv
             }
-            createParentDirs markerFile
-            IO.FS.writeFile markerFile ""
+            writeMarker markerFile
           let traces ← staticFiles.mapM computeTrace
           addTrace <| mixTraceArray traces
           -- We read the manifest to determine which HTML files were generated because we only

test/test-multi-lib-docs.sh

@@ -1,8 +1,15 @@
 #!/usr/bin/env bash
 #
-# Regression test: verify that building docs for multiple libraries in one
-# `lake build` produces HTML for all of them, and that an incremental build
-# of a third library doesn't remove the first two.
+# Regression test for the `docs` facet. It verifies that:
+#   * one `lake build` of several libraries produces HTML for all of them;
+#   * an incremental build of a third library keeps the pages of the first two;
+#   * a change in a module reaches the HTML, whether the module is a library
+#     root or an import of one;
+#   * a removed declaration and a changed docstring reach the HTML;
+#   * a rebuild with no change leaves the build up to date;
+#   * a change in one library leaves the docs of the other libraries up to date;
+#   * building the docInfo facet again for unchanged modules leaves the HTML
+#     up to date.
 #
 # Usage: run from the doc-gen4 repo root (or pass it as $1).
 #   ./test/test-multi-lib-docs.sh
@@ -36,11 +43,19 @@ lean_lib LibB
 lean_lib LibC
 EOF
 
+mkdir -p "$TEST_DIR/LibA"
 cat > "$TEST_DIR/LibA.lean" << 'EOF'
+import LibA.Basic
+
 /-- A greeting from LibA -/
 def libAGreeting := "hello from A"
 EOF
 
+cat > "$TEST_DIR/LibA/Basic.lean" << 'EOF'
+/-- A greeting from LibA.Basic -/
+def libABasicGreeting := "hello from A.Basic"
+EOF
+
 cat > "$TEST_DIR/LibB.lean" << 'EOF'
 /-- A greeting from LibB -/
 def libBGreeting := "hello from B"
@@ -54,6 +69,7 @@ EOF
 export LEAN_ABORT_ON_PANIC=1
 export DOCGEN_SRC=file
 DOC_DIR="$TEST_DIR/.lake/build/doc"
+DOC_DATA_DIR="$TEST_DIR/.lake/build/doc-data"
 
 check_html() {
   local fail=0
@@ -72,6 +88,17 @@ check_html() {
   fi
 }
 
+check_up_to_date() {
+  for lib in "$@"; do
+    if (cd "$TEST_DIR" && lake build "$lib:docs" --no-build); then
+      echo "OK: $lib:docs is up to date"
+    else
+      echo "FAIL: $lib:docs is out of date"
+      exit 1
+    fi
+  done
+}
+
 # --- Phase 1: build LibA and LibB concurrently ---
 
 echo "=== Building LibA:docs and LibB:docs ==="
@@ -84,4 +111,84 @@ echo "=== Building LibC:docs incrementally ==="
 (cd "$TEST_DIR" && lake build LibC:docs)
 check_html LibA LibB LibC
 
+# --- Phase 3: modify LibA, ensure that the change shows up in the HTML ---
+
+echo "=== Adding a declaration to LibA and building LibA:docs again ==="
+cat >> "$TEST_DIR/LibA.lean" << 'EOF'
+
+/-- A second greeting from LibA -/
+def libAGreetingAgain := "hello again from A"
+EOF
+(cd "$TEST_DIR" && lake build LibA:docs)
+if grep -q 'libAGreetingAgain' "$DOC_DIR/LibA.html"; then
+  echo "OK: the page of LibA shows the new declaration"
+else
+  echo "FAIL: the page of LibA does not show libAGreetingAgain"
+  exit 1
+fi
+
+# --- Phase 4: ensure that all three libraries are up to date now that LibA:docs is rebuilt ---
+
+echo "=== Checking that no library needs a rebuild ==="
+check_up_to_date LibA LibB LibC
+
+# --- Phase 5: ensure that changes in non-root modules are reflected in HTML ---
+
+echo "=== Adding a declaration to LibA/Basic.lean and building LibA:docs again ==="
+cat >> "$TEST_DIR/LibA/Basic.lean" << 'EOF'
+
+/-- A second greeting from LibA.Basic -/
+def libABasicGreetingAgain := "hello again from A.Basic"
+EOF
+(cd "$TEST_DIR" && lake build LibA:docs)
+if grep -q 'libABasicGreetingAgain' "$DOC_DIR/LibA/Basic.html"; then
+  echo "OK: the page of LibA.Basic shows the new declaration"
+else
+  echo "FAIL: the page of LibA.Basic does not show libABasicGreetingAgain"
+  exit 1
+fi
+check_html LibA LibB LibC
+
+# --- Phase 6: remove a declaration and change a docstring, ensure that the HTML is updated ---
+
+echo "=== Removing a declaration from LibA, changing a docstring, and building LibA:docs again ==="
+cat > "$TEST_DIR/LibA.lean" << 'EOF'
+import LibA.Basic
+
+/-- A revised greeting from LibA -/
+def libAGreeting := "hello from A"
+EOF
+(cd "$TEST_DIR" && lake build LibA:docs)
+if grep -q 'libAGreetingAgain' "$DOC_DIR/LibA.html"; then
+  echo "FAIL: the page of LibA still shows the removed libAGreetingAgain"
+  exit 1
+else
+  echo "OK: the page of LibA omits the removed declaration"
+fi
+if grep -q 'A revised greeting from LibA' "$DOC_DIR/LibA.html"; then
+  echo "OK: the page of LibA shows the new docstring"
+else
+  echo "FAIL: the page of LibA does not show the new docstring"
+  exit 1
+fi
+if grep -q 'A greeting from LibA' "$DOC_DIR/LibA.html"; then
+  echo "FAIL: the page of LibA still shows the old docstring"
+  exit 1
+else
+  echo "OK: the page of LibA omits the old docstring"
+fi
+
+# --- Phase 7: build the docInfo facet again for unchanged modules, ensure that the HTML stays up to date ---
+
+echo "=== Removing the docInfo markers of LibA and building LibA:docInfo again ==="
+rm "$DOC_DATA_DIR/LibA.doc" "$DOC_DATA_DIR/LibA.Basic.doc"
+(cd "$TEST_DIR" && lake build LibA:docInfo)
+for marker in LibA.doc LibA.Basic.doc; do
+  if [ ! -f "$DOC_DATA_DIR/$marker" ]; then
+    echo "FAIL: $marker was not written again"
+    exit 1
+  fi
+done
+check_up_to_date LibA
+
 echo "SUCCESS: All three libraries have HTML documentation"