integer-mult-bounds/.github/workflows/verify.yml at main · d-cs/integer-mult-bounds · 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
81
82
83
84
85
name: Verify research artifacts

on:
  push:
  pull_request:
  workflow_dispatch:

permissions:
  contents: read

jobs:
  verify:
    runs-on: ubuntu-24.04
    timeout-minutes: 35
    strategy:
      fail-fast: false
      matrix:
        python-version: ['3.11', '3.13', '3.14']
        group: [community, producers, certificates, ternary, research, tests, strips, clones, positive, joint, pair, partial-gauge, three-stage-cover, paired-cube, recycled-bit, entrance-banks]
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
        with:
          persist-credentials: false
      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7
        with:
          python-version: ${{ matrix.python-version }}
      - name: Install headers for the exact enlarged-frame profiler
        if: matrix.group == 'positive'
        run: |
          if ! test -f /usr/include/boost/multiprecision/cpp_int.hpp; then
            sudo apt-get update
            sudo apt-get install -y libboost-dev
          fi
      - name: Check arithmetic, source hashes, finite identities, and patches
        run: make verify-${{ matrix.group }}
      - name: Require reproducible certificates and patches
        run: git diff --exit-code

  ranked-pair-finite:
    runs-on: ubuntu-24.04
    timeout-minutes: 20
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
        with:
          persist-credentials: false
      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7
        with:
          python-version: '3.13'
      - name: Fetch immutable PR62 construction sources
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
        with:
          repository: CrocSwap/integer-mult-bounds
          ref: ad0f25ff7b23cff7f08ad237c2254e6ecf74257e
          path: build/ranked-pair-upstream
          persist-credentials: false
      - name: Independently replay words and rebuild exact CRT profiles
        run: make ranked-pair-verify UPSTREAM=build/ranked-pair-upstream
      - name: Require unchanged tracked artifacts
        run: git diff --exit-code

  formal:
    runs-on: ubuntu-24.04
    timeout-minutes: 45
    strategy:
      fail-fast: false
      matrix:
        package: [historical, gaussian, matrix]
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
        with:
          persist-credentials: false
      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7
        with:
          python-version: '3.13'
      - name: Install elan; each project pins its Lean toolchain
        run: |
          curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/leanprover/elan/0e36a07b9bbcc5381fa6250df109f9a4f94d7bac/elan-init.sh -o /tmp/elan-init.sh
          sh /tmp/elan-init.sh -y --default-toolchain none
          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
      - name: Fetch pinned Mathlib build cache
        if: matrix.package == 'historical'
        working-directory: formal/lean
        run: lake exe cache get
      - name: Check formal package and theorem axiom dependencies
        run: make formal-${{ matrix.package }}-verify