I have a project that is installed and in the LoadPath. Now, in the same opam switch, I work on a copy of the source of that project.
Should the standard coq_makefile approach "prefere" the files mentioned in _CoqProject
of my local coptyover the ones in the LoadPath?
Is there a way to make one of the three main editros (vscoq, PG, coqIDE) aware to prefere the "local" compiled files over the ones installed in the switch?
Or do seasoned Coq users just create a new opam switch in this scenario to make sure nothing bad happens?
highly recommended to either change namespace of "local code" or use a new opam switch
I haven't bothered with either change... But those options are both extremely expensive
AFAICS, loading a mix of the two libraries would be detected and fail.
(however, I'm not sure what happens if you have modified the Loadpath; I just used the standard installation into user-contrib)
However, what can happen (and be a problem) is that installed files are loaded if your local copy is only partially compiled... I said that'd be detected, but only if the stray files load parts of your library.
Temporarily moving the library outside of user-contrib sounds like a cheaper way to disable it, if you're worried, and don't want to leave these concerns to CI.
Last updated: Oct 13 2024 at 01:02 UTC