Skip to content

configuration for ProofGeneral with a Dune build of UniMath and this satellite #160

@rmatthes

Description

@rmatthes

The provided file .dir-locals.el that configures ProofGeneral when visiting a file of this satellite is severely outdated. In particular, it still features the Rocq option -type-in-type.

More severely, it does not find the UniMath library in an installation through Dune following the organization suggested in issue #147 (with largecatmodules a sister directory of the child directory UniMath).

Here is a suggestion for a replacement of that file in case of a Dune build. This is not yet a suggestion for the organization of the GitHub repository. How to choose between old-style (Make) and Dune build? Probably, .dir-locals.el should always only be set during the installation process and not itself be part of the repository (just as for UniMath).

My suggestion tries to be a minimal modification of .dir-locals.el of UniMath. The variable unimath-topdir is calculated through the layout of issue #147, the physical mapping for largecatmodules seems to require option -R, not -Q.

The file name below has been suffixed with .txt so as to be acceptable as an attachment to this issue.
.dir-locals.el.txt

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