search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.87k stars 656 forks source link

Installing coq-doc from opam fails with File not found: ../../theories/Init/Prelude.vo The path for Coq libraries is wrong. #19533

Open JasonGross opened 2 months ago

JasonGross commented 2 months ago

Description of the problem

$ opam pin add git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon -y --confirm-level=unsafe-yes
This will pin the following packages: coq-core, coq-doc, coq-stdlib, coq, coqide-server, coqide. Continue? [y/n] y
[NOTE] Package coq-core is currently pinned to git+https://github.com/coq/coq#44155b062e6c384cc3ca36293b99dcd13f9cb085 (version dev).
coq-core is now pinned to git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon (version dev)
Package coq-doc does not exist, create as a NEW package? [y/n] y
coq-doc is now pinned to git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon (version dev)
[NOTE] Package coq-stdlib is currently pinned to git+https://github.com/coq/coq#44155b062e6c384cc3ca36293b99dcd13f9cb085 (version dev).
coq-stdlib is now pinned to git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon (version dev)
coq is now pinned to git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon (version dev)
[NOTE] Package coqide-server is currently pinned to git+https://github.com/coq/coq#44155b062e6c384cc3ca36293b99dcd13f9cb085 (version dev).
coqide-server is now pinned to git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon (version dev)
coqide is now pinned to git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon (version dev)

The following actions will be performed:
=== recompile 5 packages
  - recompile coq                     dev (pinned)
  - recompile coq-bignums             dev          [uses coq]
  - recompile coq-core                dev (pinned)
  - recompile coq-stdlib              dev (pinned)
  - recompile coqide-server           dev (pinned)
=== install 14 packages
  - install   cairo2                  0.6.4        [required by coqide]
  - install   camlp-streams           5.0.1        [required by lablgtk3-sourceview3]
  - install   conf-adwaita-icon-theme 2            [required by coqide]
  - install   conf-cairo              1            [required by cairo2]
  - install   conf-findutils          1            [required by coqide]
  - install   conf-gtk3               18           [required by lablgtk3]
  - install   conf-gtksourceview3     0+2          [required by lablgtk3-sourceview3]
  - install   conf-python-3           9.0.0        [required by coq-doc]
  - install   coq-doc                 dev (pinned)
  - install   coqide                  dev (pinned)
  - install   csexp                   1.5.2        [required by dune-configurator]
  - install   dune-configurator       3.16.0       [required by cairo2]
  - install   lablgtk3                3.1.5        [required by lablgtk3-sourceview3]
  - install   lablgtk3-sourceview3    3.1.5        [required by coqide]

The following system packages will first need to be installed:
    adwaita-icon-theme libcairo2-dev libexpat1-dev libgtk-3-dev libgtksourceview-3.0-dev
[...]
-> removed   coq-bignums.dev
-> removed   coq.dev
-> removed   coq-stdlib.dev
-> removed   coqide-server.dev
-> removed   coq-core.dev
-> installed coq-core.dev
-> installed coqide-server.dev
-> installed coqide.dev
-> installed coq-stdlib.dev
-> installed coq.dev
Error:  The compilation of coq-doc.dev failed at "dune build -p coq-doc -j 3 @install".
-> installed coq-bignums.dev

#=== ERROR while compiling coq-doc.dev ========================================#
context              2.2.1 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.13.1+options | pinned(git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon#b999f458037563317ddbb8ab6e3ecf9e1986077d)
path                 ~/.opam/4.13.1+flambda/.opam-switch/build/coq-doc.dev
command              ~/.opam/4.13.1+flambda/bin/dune build -p coq-doc -j 3 @install
exit-code            1
env-file             ~/.opam/log/coq-doc-568-5758e8.env
output-file          ~/.opam/log/coq-doc-568-5758e8.out
### output ###
[...]
38 |   (env_var SPHINXWARNOPT))
39 |  (action
40 |   (run env sphinx-build -q %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets})))
(cd _build/default/doc && /usr/bin/env sphinx-build -q -W -b html sphinx refman-html)
/usr/bin/env: 'sphinx-build': No such file or directory
(cd _build/default && /usr/bin/bash -e -u -o pipefail -c 'doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files')
Building file index-list.prehtml... Done
(cd _build/default/doc/stdlib && /usr/bin/bash -e -u -o pipefail -c '/home/coq/.opam/4.13.1+flambda/bin/coqdoc -q -d html --with-header ../common/styles/html/coqremote/header.html --with-footer ../common/styles/html/coqremote/footer.html --multi-index --html -g -coqlib ../.. -R ../../theories Stdlib -Q ../../user-contrib/Ltac2 Ltac2 $(find ../../theories ../../user-contrib -name *.v)')
File not found: ../../theories/Init/Prelude.vo
The path for Coq libraries is wrong.
Coq libraries are shipped in the coq-stdlib package.
Please check the COQLIB env variable or the -coqlib option.

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-doc dev
+- 
+- The following changes have been performed
| - recompile coq                     dev
| - recompile coq-bignums             dev
| - recompile coq-core                dev
| - recompile coq-stdlib              dev
| - recompile coqide-server           dev
| - install   cairo2                  0.6.4
| - install   camlp-streams           5.0.1
| - install   conf-adwaita-icon-theme 2
| - install   conf-cairo              1
| - install   conf-findutils          1
| - install   conf-gtk3               18
| - install   conf-gtksourceview3     0+2
| - install   conf-python-3           9.0.0
| - install   coqide                  dev
| - install   csexp                   1.5.2
| - install   dune-configurator       3.16.0
| - install   lablgtk3                3.1.5
| - install   lablgtk3-sourceview3    3.1.5
+-

Small Coq file to reproduce the bug

No response

Version of Coq where this bug occurs

No response

Last version of Coq where the bug did not occur

No response

Zimmi48 commented 2 months ago

Could it be that the latest error message misguides us in debugging the error? I see that we also have:

/usr/bin/env: 'sphinx-build': No such file or directory

earlier in the log, which seems to indicate that you don't have the Sphinx dependency installed. I have no idea if this is something that could be fixed by adding a conf-... package.

I also haven't tried to reproduce this locally. It would be interesting to know if this is just a dependency problem, and if not, if this is a regression compared to a previously working state.