Stream: Coq users

Topic: _CoqProject file inside our outside of theories


view this post on Zulip Yannick Forster (Nov 19 2020 at 09:58):

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?

view this post on Zulip Théo Winterhalter (Nov 19 2020 at 10:03):

If the project is to be used with the current vscoq, then having at the root is a big help.

view this post on Zulip Ralf Jung (Nov 19 2020 at 10:06):

Iris also has it in the root (outside theories), but I do not recall if we even tried having it inside theories

view this post on Zulip Andrej Dudenhefner (Nov 19 2020 at 10:06):

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.

view this post on Zulip Théo Winterhalter (Nov 19 2020 at 10:06):

I think it makes more sense outside the theories directory because that's also where you keep your Makefile usually and everything.

view this post on Zulip Théo Winterhalter (Nov 19 2020 at 10:07):

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.

view this post on Zulip Paolo Giarrusso (Nov 19 2020 at 10:23):

intuitively, the folder I open in vscode is usually a whole git repo, so that’s where I expect _CoqProject

view this post on Zulip Paolo Giarrusso (Nov 19 2020 at 10:25):

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)

view this post on Zulip Fabian Kunze (Nov 19 2020 at 10:26):

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

view this post on Zulip Théo Winterhalter (Nov 19 2020 at 10:43):

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.

view this post on Zulip Fabian Kunze (Nov 19 2020 at 10:47):

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

view this post on Zulip Théo Winterhalter (Nov 19 2020 at 10:48):

Ah ok, that's cool. :)


Last updated: Feb 04 2023 at 22:29 UTC