Skip to content

Install instructions do not work, due to missing dune 3.16.1 -- have to use script from main instead #489

@edwintorok

Description

@edwintorok

I'm getting the same error as in https://proofassistants.stackexchange.com/a/5162, with dune-configurator 3.16.1 unavailable:

===== INSTALL PREREQUISITES (PARALLEL) =====
[ERROR] Package dune-configurator has no version 3.16.1.

This can be worked around as in the above link by cloning main instead and using the script from there.

However I think that the instructions at https://github.com/rocq-prover/platform/blob/2025.01.0/doc/README_Linux.md#installation-by-compiling-from-sources-using-scripts--opam (linked from https://rocq-prover.org/install should be updated.

They currently say:

Get the Coq Platform scripts via either of these methods

Most users should download and extract https://github.com/coq/platform/archive/refs/tags/2025.01.0.zip.
Users which intend to contribute to Coq Platform should use git clone --branch 2025.01.0 https://github.com/coq/platform.git.

However I think neither of those instructions work anymore, the 2025.1.0 branch should probably backport the linked patch (744d339#diff-e37348a52bd0b2342185b88de810e2461ce134ec8e1e25a79737619ef79c197c?), otherwise new users will get an installation error.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions