Skip to content

Filter for the run-test: field of the OPAM file #128

@pi8027

Description

@pi8027

I have a Coq development where the test suite fails only with Coq 8.17, seemingly because of a bug in Coq or Paramcoq, or an interaction issue between Equations and Paramcoq. Since I think that the issue is not worth investigating further, I would like to add the filter below to turn off the test suite only with Coq 8.17.

run-test: [ [make "-j%{jobs}%" "build-misc" ] { coq:version < "8.17" | "8.18" <= coq:version } ]

However, Coq-community templates do not seem to provide the functionality to produce this line, and I had to edit the OPAM file by hand. See also: pi8027/stablesort#25 (comment)

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions