Derive inhabited and make ext grind-able

[petros-marko]

For structures emitted to lean

• derive Inhabited (we already require type params to be Inhabited)
• add a grind . annotation to the struct extensionality theorem

[nilehmann]

D:

[petros-marko]

D:

Yeah, I'm curious what happened there. I'll fix.

[petros-marko]

D:

Yeah, I'm curious what happened there. I'll fix.

Interesting, this works fine locally for me. Could you try it out @nilehmann?

[nilehmann]

@petros-marko is there anything pining the lean version?

[petros-marko]

@petros-marko is there anything pining the lean version?

In lean_encoding.rs when we create the lean project we do lake +v4.28.0 new ... which I thought does the pinning.

[nilehmann]

@petros-marko I ran on a fresh clone of flux-to-lean-demo and got a different error

[petros-marko]

Ah, I thought that might happen. Adding in grind annotations for the extensionality theorems probably makes each call to grind slightly more expensive.

[nilehmann]

CI is not calling ./runlean.sh. That may be it

  lean-demo:
    strategy:
      matrix:
        os: [ubuntu-latest, macos-latest]
    runs-on: ${{ matrix.os }}
    steps:
      - uses: actions/checkout@v4

      - name: Install Lean via elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
          echo "$HOME/.elan/bin" >> $GITHUB_PATH
      - name: Install fixpoint
        uses: ./.github/actions/install-fixpoint
        env:
          GITHUB_TOKEN:
            ${{ secrets.GITHUB_TOKEN }}

            # Older versions hang
      - name: Install Z3
        uses: cda-tum/setup-z3@v1.6.6
        with:
          version: 4.15.3

      - name: Rust Cache
        uses: Swatinem/rust-cache@v2.8.0

      - name: Install Flux
        run: |
          cargo x install
          echo ~/.cargo/bin >> $GITHUB_PATH
      - name: Clone flux-to-lean-demo
        run: |
          git clone https://github.com/flux-rs/flux-to-lean-demo
      - name: Generate Lean Project
        continue-on-error: true
        working-directory: flux-to-lean-demo
        run: |
          cargo flux
      - name: Copy proofs
        working-directory: flux-to-lean-demo
        run: |
          cp -r LeanUserProofs/* lean_proofs/LeanProofs/User/
      - name: Run lean
        working-directory: flux-to-lean-demo
        run: |
          cd lean_proofs && lake build
      - name: Check proofs in flux
        run: |
          cargo flux

[nilehmann]

hmmm, although it looks like it's doing the same

[nilehmann]

According to copilot

Key configuration mismatch

CI is not reproducing runlean.sh.

CI does:

    cp -r LeanUserProofs/* lean_proofs/LeanProofs/User/

That creates:

    lean_proofs/LeanProofs/User/Lib/...
    lean_proofs/LeanProofs/User/User/...
    lean_proofs/LeanProofs/User/lakefile.toml

So CI does not:

    replace generated stubs in LeanProofs/User/...
    install LeanProofs/Lib/... in the right place
    replace root lean_proofs/lakefile.toml

By contrast, runlean.sh does:

    copy User and Lib into lean_proofs/LeanProofs/
    copy LeanUserProofs/lakefile.toml to lean_proofs/lakefile.toml
    run lake update