Stream: Coq devs & plugin devs

Topic: Dune and Coqdoc

Guillaume Melquiond (Feb 08 2022 at 17:26):

What is the proper way of running Coqdoc over the standard library nowadays?

Guillaume Melquiond (Feb 08 2022 at 17:29):

$ make -f Makefile.doc doc-stdlib-html
rm -rf _build_vo/default/doc/stdlib/html/
p _build_vo/default/doc/stdlib/html/
make: p: Command not found

Gaëtan Gilbert (Feb 08 2022 at 17:30):

Makefile.doc is not meant to be used through -f

Gaëtan Gilbert (Feb 08 2022 at 17:31):

just make doc-stdlib-html (-f Makefile.make if you have COQ_USE_DUNE in your environment variables)

Guillaume Melquiond (Feb 08 2022 at 17:34):

$ make doc-stdlib-html
Please run ./configure first to continue building with make
or pass option "-f Makefile.dune" to let dune manage the build
make: *** [Makefile.make:126 : noconfig] Erreur 1

$ make -f Makefile.dune doc-stdlib-html
make: *** No rule to make target 'doc-stdlib-html'.  Stop.

Gaëtan Gilbert (Feb 08 2022 at 17:36):

it tells you to run configure
so do it

Guillaume Melquiond (Feb 08 2022 at 17:37):

But I wanted to use Dune!

Emilio Jesús Gallego Arias (Feb 08 2022 at 17:40):

the target is stdlib-html

Emilio Jesús Gallego Arias (Feb 08 2022 at 17:40):

make -f Makefile.dune stdlib-html

Emilio Jesús Gallego Arias (Feb 08 2022 at 17:40):

sorry we still have the two systems, hopefully next week we can finally remedy that

Last updated: Oct 13 2024 at 01:02 UTC