Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Coq documentation generation fails with Coq in the workspace #11016

Open
rlepigre opened this issue Oct 17, 2024 · 0 comments
Open

Coq documentation generation fails with Coq in the workspace #11016

rlepigre opened this issue Oct 17, 2024 · 0 comments
Labels
coq

Comments

@rlepigre
Copy link
Contributor

There seems to be an issue with the coqdoc rules when coq itself (and the standard library) are in the workspace. Unlike for the coqc or coqdep rules, it seems that the coqdoc rules are not passed the right variables / environment variables to locate the standard library.

To reproduce, one can do the following:

mkdir coqdoc_workspace_bug
cd coqdoc_workspace_bug

echo "(lang dune 3.8)" > dune-workspace

git clone git@github.com:coq/coq.git
mv coq/theories/dune.disabled coq/theories/dune
mv coq/user-contrib/Ltac2/dune.disabled coq/user-contrib/Ltac2/dune

mkdir -p test/theories
touch test/theories/test.v
echo "(lang dune 3.16)\n(using coq 0.8)\n(name test)" > test/dune-project
echo "(coq.theory (name test))" > test/theories/dune

dune build test/theories/test.vo
dune build @test/doc

The last command then fails with:

File "test/theories/dune", lines 1-2, characters 0-25:
1 | (coq.theory
2 |  (name test))
cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.
@maiste maiste added the coq label Oct 17, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
coq
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@rlepigre @maiste