Stream: Coq users

Topic: Compiling a library that is already installed


view this post on Zulip Fabian Kunze (Oct 22 2020 at 08:30):

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?

view this post on Zulip Karl Palmskog (Oct 22 2020 at 08:33):

highly recommended to either change namespace of "local code" or use a new opam switch

view this post on Zulip Paolo Giarrusso (Oct 22 2020 at 12:06):

I haven't bothered with either change... But those options are both extremely expensive

view this post on Zulip Paolo Giarrusso (Oct 22 2020 at 12:07):

AFAICS, loading a mix of the two libraries would be detected and fail.

view this post on Zulip Paolo Giarrusso (Oct 22 2020 at 12:08):

(however, I'm not sure what happens if you have modified the Loadpath; I just used the standard installation into user-contrib)

view this post on Zulip Paolo Giarrusso (Oct 22 2020 at 12:10):

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.

view this post on Zulip Paolo Giarrusso (Oct 22 2020 at 12:11):

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: Jan 29 2023 at 03:28 UTC