tropical-types/.github/workflows/lean.yml at main · hyperpolymath/tropical-types · 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
71
72
73
74
75
76
77
78
79
80
# This workflow is managed by gh actions-lock.
# SPDX-License-Identifier: MPL-2.0
# This workflow is managed by gh actions-lock.
# lean.yml — build the Lean 4 tropical proofs and audit their axioms.
#
# Load-bearing build workflow (kept standalone in-repo, not in the shared
# governance bundle): `lake build` over both order-reversing twins, then a
# `#print axioms` audit asserting no `sorry`/`Classical.choice` crept in.
# Toolchain is pinned by ./lean-toolchain (leanprover/lean4:v4.35.0); no Mathlib.

name: Lean

on:
  push:
    branches: [main, master]
  pull_request:
  workflow_dispatch:

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

permissions:
  contents: read

jobs:
  lake-build:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4.4.0

      - name: Install elan (Lean toolchain manager)
        run: |
          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o elan-init.sh
          sh elan-init.sh -y --default-toolchain none
          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

      - name: Show toolchain (pinned via lean-toolchain)
        run: lean --version

      - name: lake build
        run: lake build

      - name: Axiom audit — no sorry; propext/Quot.sound only
        run: |
          cat > /tmp/axcheck.lean <<'EOF'
          import TropicalSessionTypes
          import TropicalAdapterPath
          import Resource
          #print axioms Hyperpolymath.Tropical.soundness
          #print axioms Hyperpolymath.Tropical.tropical_grade_le_sequentialTotal
          #print axioms Hyperpolymath.ProtocolSquisher.Tropical.pathCost_mono
          #print axioms Hyperpolymath.ProtocolSquisher.Tropical.hub_ceiling
          #print axioms Hyperpolymath.ProtocolSquisher.Tropical.dualGrade_invol
          #print axioms Hyperpolymath.ProtocolSquisher.Tropical.dual_tcAdd_is_max
          #print axioms Hyperpolymath.ProtocolSquisher.Tropical.dual_tcMul_is_min
          -- Resource-grade axis: interface, transport theorem, instances, stress test
          #print axioms Resource.parametric_resource_transport
          #print axioms Resource.resource_laws_sufficient_for_consumers
          #print axioms Resource.ResourceAlgebra.ofIdempotentAdd
          #print axioms Resource.Instances.Linear.instResourceAlgebra
          #print axioms Resource.Instances.Affine.instResourceAlgebra
          #print axioms Resource.Instances.MaxPlus.instResourceAlgebra
          #print axioms Resource.Instances.MinPlus.MinPlus.instResourceAlgebra
          #print axioms Resource.Instances.MinMax.MinMax.instResourceAlgebra
          #print axioms Resource.Instances.infinite_maxPlus
          #print axioms Resource.Instances.infinite_minPlus
          #print axioms Resource.Instances.infinite_minMax
          #print axioms Resource.echoResidueAsMaxPlusCost
          -- Bridges: the two original twins as instances of the axis
          #print axioms Resource.Bridge.grade_le_sequential
          #print axioms Resource.Bridge.hub_ceiling_le
          #print axioms Resource.Bridge.embed_tcZero_ne_zero
          EOF
          out="$(lake env lean /tmp/axcheck.lean 2>&1)"
          echo "$out"
          if echo "$out" | grep -qiE 'sorry|Classical\.choice'; then
            echo "::error::axiom audit failed — sorry or Classical.choice present"
            exit 1
          fi