What is the proper way of running Coqdoc over the standard library nowadays?
$ 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
Makefile.doc is not meant to be used through -f
make doc-stdlib-html (
-f Makefile.make if you have
COQ_USE_DUNE in your environment variables)
$ 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.
it tells you to run configure
so do it
But I wanted to use Dune!
the target is stdlib-html
make -f Makefile.dune stdlib-html
sorry we still have the two systems, hopefully next week we can finally remedy that
Last updated: May 31 2023 at 15:01 UTC