Skip to content

coq-prog-name disregarded and overwritten #869

@hendriktews

Description

@hendriktews

Assume an environment that has coqtop with some version 8 and rocq with some version 9. After merging PR #841 PG will always run rocq, even if one configures coq-prog-name to "coqtop".

When coq-prog-name is configured to "coqtop", then after visiting the first .v file, coq-prog-name and proof-prog-name both still have the value "coqtop". However, when starting Coq/Rocq when the first line is asserted, both are overwritten to "rocq".

PG should support a feature, where the user can configure the Coq/Rocq binary via file or directory local variables.

Does anybody remember the reason why PG overwrites coq-prog-name?

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions