Move _CoqProject one folder up (`./` instead `./theories/`)?
Closed this issue · 7 comments
If we would move _CoqProject and Make one folder up, we could eliminate an duplicated "Makefile" (in ./ and ./theories) and make it such that in e.g. vscode, we can open the project at top-level (not in theories) and still step into coq-files.
One would need to:
- update _Coq_roject by prepending /theories before all files
- update the CI files
What are your thoughts?
I prefer the current theories encapsulation because inside it is purely Coq (no CI, website). As a result I like to open vscode in theories. Also, it feels like _CoqProject belongs to the Coq part.
As points of comparison, I checked iris where the _CoqProject file is top-level, math-comp where it is in theories, and MetaCoq where it is top-level for all subprojects.
I'm in favour of moving the file up, but have no strong opinion.
Why do CI files have to be changed though? They only issue a make.
I asked on Zulip whether people have negative / positive experiences: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/_CoqProject.20file.20inside.20our.20outside.20of.20theories/near/217248155
Alternatively, we can remove theories/Makefile and port all the logic in there to Makefile.
Drawback for both moving the _CoqProject up and deleting theories/Makefile: You can't type make anymore in the theories directory, which might be annoying.
inspired by the zulip, i just changed vscoq: coq-community/vscoq#179
Based on the zulip answers the key question is: do we want to open and use IDEs like vscode in root?
My current workflow does not touch files outside theories which (if included) would clutter my vscode file and search panels.
However, I can see others working in vscode on html/js/CI/readme files, so I would not oppose the change.
I came to the workarround of using code ../README.md in teh vscode-terminal to open the files from above inside the IDE, so I don;t need this anymore.