WORKING DIRECTORY: LEAN_PROJECT
START UTC: 2026-09-05T23:16:19.9197670Z
COMMAND: & 'WORKSPACE\tmp\lean_library_definition_audit_2026-09-05\lean-4.34.0-rc2-windows\bin\lake.exe' '--no-cache' 'env' 'lean' '-j1' '-M8192' 'verification/independent-audit-2026-09-05/TraceDependencies.lean'
TERMINAL OUTPUT:
verification/independent-audit-2026-09-05/TraceDependencies.lean:59:2: error: Type mismatch
  liftIO (IO.FS.createDirAll outputDirectory)
has type
  CommandElabM Unit
but is expected to have type
  MetaM Unit
verification/independent-audit-2026-09-05/TraceDependencies.lean:60:17: error: Type mismatch
  liftIO (IO.FS.Handle.mk (outputDirectory / { toString := "dependency_nodes.jsonl" }) IO.FS.Mode.write)
has type
  CommandElabM IO.FS.Handle
but is expected to have type
  MetaM ?m.53
verification/independent-audit-2026-09-05/TraceDependencies.lean:61:17: error: Type mismatch
  liftIO (IO.FS.Handle.mk (outputDirectory / { toString := "dependency_edges.jsonl" }) IO.FS.Mode.write)
has type
  CommandElabM IO.FS.Handle
but is expected to have type
  MetaM ?m.60
verification/independent-audit-2026-09-05/TraceDependencies.lean:62:19: error: Type mismatch
  liftIO (IO.FS.Handle.mk (outputDirectory / { toString := "dependency_direct.jsonl" }) IO.FS.Mode.write)
has type
  CommandElabM IO.FS.Handle
but is expected to have type
  MetaM ?m.67
verification/independent-audit-2026-09-05/TraceDependencies.lean:83:6: error: Type mismatch
  liftIO (jsonLine nodeFile [("name", toJson name.toString), ("status", toJson "missing_checked_constant")])
has type
  CommandElabM Unit
but is expected to have type
  MetaM Unit
verification/independent-audit-2026-09-05/TraceDependencies.lean:117:6: error: Type mismatch
  liftIO (jsonLine nodeFile node)
has type
  CommandElabM Unit
but is expected to have type
  MetaM Unit
verification/independent-audit-2026-09-05/TraceDependencies.lean:136:10: error: Type mismatch
  liftIO (jsonLine edgeFile fields)
has type
  CommandElabM Unit
but is expected to have type
  MetaM Unit
verification/independent-audit-2026-09-05/TraceDependencies.lean:140:12: error: Type mismatch
  liftIO
    (jsonLine directFile
      (fields ++
        [("origin_module", toJson (Option.map (fun n => n.toString) dependencyOrigin)),
          ("project_owned", toJson (Option.any projectModule dependencyOrigin)),
          ("kind", toJson (Option.map kind dependencyInfo))]))
has type
  CommandElabM Unit
but is expected to have type
  MetaM Unit
verification/independent-audit-2026-09-05/TraceDependencies.lean:176:2: error: Type mismatch
  liftIO (IO.FS.writeFile (outputDirectory / { toString := "kernel_dependency_summary.json" }) summary.pretty)
has type
  CommandElabM Unit
but is expected to have type
  MetaM Unit
verification/independent-audit-2026-09-05/TraceDependencies.lean:177:2: error: Type mismatch
  liftIO
    (IO.FS.writeFile (outputDirectory / { toString := "dependency_trace.txt" })
      (toString "Target: " ++ toString target ++ toString "\nType: " ++ toString targetType.pretty ++
                                                    toString "\nExpanded target type: " ++
                                                  toString expandedTargetType.pretty ++
                                                toString "\nTraversal complete: " ++
                                              toString complete ++
                                            toString "\nChecked constants: " ++
                                          toString checkedCount ++
                                        toString "\nProject constants: " ++
                                      toString localCount ++
                                    toString "\nEdges: " ++
                                  toString edgeCount ++
                                toString "\nDirectly traversed axioms: " ++
                              toString actualAxioms ++
                            toString "\nStock collectAxioms: " ++
                          toString expectedAxioms ++
                        toString "\nAxiom lists agree: " ++
                      toString axiomAgreement ++
                    toString "\nMissing constants: " ++
                  toString (sortedNames missing) ++
                toString "\nMissing expected bodies: " ++
              toString (sortedNames missingBodies) ++
            toString "\nLocal suspicious constants: " ++
          toString localSuspicious.size ++
        toString
          "\nRaw nodes: dependency_nodes.jsonl\nRaw typed edges: dependency_edges.jsonl\nDirect references: dependency_direct.jsonl\nStructured summary: kernel_dependency_summary.json\n"))
has type
  CommandElabM Unit
but is expected to have type
  MetaM Unit
verification/independent-audit-2026-09-05/TraceDependencies.lean:191:0: error: Aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.

To attempt to evaluate anyway despite the risks, use the '#eval!' command.
EXIT CODE: 1
END UTC: 2026-09-05T23:16:39.1493197Z