Stream: Coq devs & plugin devs

Topic: Dune and Coqdoc


view this post on Zulip Guillaume Melquiond (Feb 08 2022 at 17:26):

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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Feb 08 2022 at 17:30):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Feb 08 2022 at 17:36):

it tells you to run configure
so do it

view this post on Zulip Guillaume Melquiond (Feb 08 2022 at 17:37):

But I wanted to use Dune!

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 17:40):

the target is stdlib-html

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 17:40):

make -f Makefile.dune stdlib-html

view this post on Zulip 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: Feb 02 2023 at 13:03 UTC