Stream: Coq devs & plugin devs

Topic: Status of VAR = NAME in _CoqProject?


view this post on Zulip Ralf Jung (May 11 2022 at 14:30):

I see that https://github.com/coq/coq/pull/14558 improved the documentation of the _CoqProject format. :tada:
However, NAME = VAR lines are not mentioned. They also have not been removed though, at least according to the changelog. So what is the status of those?
(FWIW I had used coq_makefile for years before realizing such assignments exist. I had to figure them out to set that INSTALLDEFAULTROOT option to silence a warning.)

view this post on Zulip Paolo Giarrusso (May 11 2022 at 14:40):

That option was removed in 8.15

view this post on Zulip Paolo Giarrusso (May 11 2022 at 14:41):

You need coq_makefile -docroot option now, and that option is not specifiable in _CoqProject.

view this post on Zulip Ana de Almeida Borges (May 11 2022 at 15:39):

-docroot is specifiable in the _CoqProject. Cf. the refman.

view this post on Zulip Ana de Almeida Borges (May 11 2022 at 15:40):

See also this zulip thread about INSTALLDEFAULTROOT.

view this post on Zulip Paolo Giarrusso (May 11 2022 at 15:41):

Oh, thanks for the correction

view this post on Zulip Ralf Jung (May 13 2022 at 07:59):

Paolo Giarrusso said:

That option was removed in 8.15

so was INSTALLDEFAULTROOT the only "NAME = VAR" thing? the changelog doesnt even mention that it got removed...

view this post on Zulip Ralf Jung (May 13 2022 at 08:07):

it just says

Added: coq_makefile now takes the -docroot option as alternative to the INSTALLCOQDOCROOT variable

"alternative" would imply that both options should work (and "Added" implies this is additive)


Last updated: Feb 06 2023 at 20:02 UTC