hbb-lean/build_with_announcements.sh at main · anoma/hbb-lean · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
#!/bin/bash
# Build with progress announcements for protocol verification

# Track which announcements have been printed
thyHBB1_done=false
thyHBB2_done=false
thyHBB3_done=false

# Run lake build with verbose output and monitor for protocol completion
# Filter out trace lines to keep output clean
while IFS= read -r line; do
    # Skip trace lines
    if [[ "$line" == trace:* ]]; then
        continue
    fi

    echo "$line"

    # Check for ThyHBB1 completion
    if [[ "$line" == *"ModalDistribution.Examples.ThyHBB1.Liveness_Two"* ]] && [ "$thyHBB1_done" = false ]; then
        echo ""
        echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
        echo "✓ Correctness properties of ThyHBB1 proved."
        echo "  • Agreement property"
        echo "  • Liveness property 1"
        echo "  • Liveness property 2"
        echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
        echo ""
        thyHBB1_done=true
    fi

    # Check for ThyHBB2 completion
    if [[ "$line" == *"ModalDistribution.Examples.ThyHBB2.Liveness_Two"* ]] && [ "$thyHBB2_done" = false ]; then
        echo ""
        echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
        echo "✓ Correctness properties of ThyHBB2 proved."
        echo "  • Agreement property"
        echo "  • Liveness property 1"
        echo "  • Liveness property 2"
        echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
        echo ""
        thyHBB2_done=true
    fi

    # Check for ThyHBB3 completion
    if [[ "$line" == *"ModalDistribution.Examples.ThyHBB3.Liveness_Two"* ]] && [ "$thyHBB3_done" = false ]; then
        echo ""
        echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
        echo "✓ Correctness properties of ThyHBB3 proved."
        echo "  • Agreement property"
        echo "  • Liveness property 1"
        echo "  • Liveness property 2"
        echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
        echo ""
        thyHBB3_done=true
    fi

    # Finish announcement
    if [[ "$line" == *"Build completed successfully"* ]]; then
        echo ""
        echo "╔════════════════════════════════════════════════════════════╗"
        echo "║  Verification of paper \"Heterogeneous trust in reliable    ║"
        echo "║  broadcast via modal logic and history structures\"         ║"
        echo "║  complete.                                                 ║"
        echo "╚════════════════════════════════════════════════════════════╝"
        echo ""
    fi
done < <(lake build --verbose 2>&1)

exit $BUILD_EXIT