Skip to content

Update CompPoly toolchain to Lean 4.23 to support integration with hax Lean backend #43

@klausnat

Description

@klausnat

Request: consider updating CompPoly’s toolchain to leanprover/lean4:v4.23.0 (or a compatible 4.23.* version).

  • hax Lean backend is pinned to Lean 4.23 since PR #1696.
  • CompPoly currently pins leanprover/lean4:v4.22.0-rc2.

As a result, it is currently not possible to:

  • build the hax Lean prelude (extraction backend) in a project that uses CompPoly, or
  • directly connect Rust code extracted via hax to CompPoly specifications in the same Lean project.

Updating CompPoly to Lean 4.23 would enable the end-to-end pipeline:
Rust → hax → CompPoly spec → proofs (without splitting across incompatible Lean versions).

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or requesthelp wantedExtra attention is neededphase 1 - theoryPhase 1 of the roadmap, focusing on theory completeness

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions