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
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-topdiris calculated through the layout of issue #147, the physical mapping forlargecatmodulesseems to require option-R, not-Q.The file name below has been suffixed with
.txtso as to be acceptable as an attachment to this issue..dir-locals.el.txt