For the coq-library-undecidability
we're contemplating whether the _CoqProject
file should go inside or outside the theories
directory. Until now it seems to me that this doesn't really make a difference. Iris seems to have it at toplevel, MetaCoq as well for each subproject, coq-ext-lib
as well on top-level, math-comp has it as part of the mathcomp
directory, which corresponds to a theories
directory. Do any of you have very negative or very positive experiences with any of the two choices?
If the project is to be used with the current vscoq, then having at the root is a big help.
Iris also has it in the root (outside theories
), but I do not recall if we even tried having it inside theories
If the project is to be used with the current vscoq, then having at the root is a big help.
Is this also true if you do not want to touch the files outside theories
from vscoq? I would imagine that file search in vscoq would then return useless root results.
I think it makes more sense outside the theories
directory because that's also where you keep your Makefile
usually and everything.
Andrej Dudenhefner said:
If the project is to be used with the current vscoq, then having at the root is a big help.
Is this also true if you do not want to touch the files outside
theories
from vscoq? I would imagine that file search in vscoq would then return useless root results.
Right, but when dealing with a project you sometimes want to open the README
or so.
intuitively, the folder I open in vscode is usually a whole git repo, so that’s where I expect _CoqProject
but maybe it’s just because I’m used to Iris — since projects are not consistent, vscoq users will sooner or later run into this, with no obvious solution (hopefully we have an issue)
Editing the readme was also one of my main concerns.
Théo Winterhalter said:
If the project is to be used with the current vscoq, then having at the root is a big help.
with this PR, this is not longer needed:
https://github.com/coq-community/vscoq/pull/179
This is cool, thanks! :)
The best would be something like CoqIDE or PG I guess which will discover _CoqProject
files in parent directories but that will already be a big help.
Théo Winterhalter said:
This is cool, thanks! :)
The best would be something like CoqIDE or PG I guess which will discover_CoqProject
files in parent directories but that will already be a big help.
i think ../
in the option for the location should work with that PR, althought I have not tested it. And if one changes the workspace
setting, one would only need to do this once
Ah ok, that's cool. :)
Last updated: Oct 13 2024 at 01:02 UTC