1  # src/examples/lean-continuity/BUCK
 2  #
 3  # Continuity: The Straylight Build Formalization
 4  #
 5  # A formal proof that the Continuity build system maintains correctness
 6  # across content-addressed derivations, typed toolchains, and isolation
 7  # boundaries.
 8  #
 9  # STATUS: This target requires Mathlib which is managed by Lake.
10  #         Lake builds are non-hermetic and disabled in Buck2.
11  #
12  # To build this project, use Lake directly:
13  #
14  #     cd src/examples/lean-continuity
15  #     lake build
16  #
17  # Or manage Mathlib via Nix overlay for hermetic builds.
18  # See: nix/overlays/ for examples.
19  
20  # Placeholder target that documents the situation
21  genrule(
22      name = "continuity",
23      out = "README.txt",
24      cmd = """
25          echo "This target requires Mathlib (Lake dependency)." > $OUT
26          echo "Lake builds are non-hermetic and disabled in Buck2." >> $OUT
27          echo "" >> $OUT
28          echo "Build with: cd src/examples/lean-continuity && lake build" >> $OUT
29      """,
30      visibility = ["PUBLIC"],
31  )