Ralf Jung (May 11 2022 at 14:30): 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.)
Paolo Giarrusso (May 11 2022 at 14:40):That option was removed in 8.15
Paolo Giarrusso (May 11 2022 at 14:41):You need coq_makefile -docroot option now, and that option is not specifiable in _CoqProject.
Ana de Almeida Borges (May 11 2022 at 15:39):-docroot is specifiable in the _CoqProject. Cf. the refman.
Ana de Almeida Borges (May 11 2022 at 15:40):See also this zulip thread about INSTALLDEFAULTROOT.
Paolo Giarrusso (May 11 2022 at 15:41):Oh, thanks for the correction
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...
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: May 31 2023 at 17:01 UTC