Karl Palmskog (Aug 18 2020 at 00:06): Karl Palmskog (Aug 18 2020 at 00:06):coqide.dev in coq-core-dev on opam is likely broken:
#=== ERROR while installing coqide.dev ========================================#
Some files in /builds/coq/opam-coq-archive/opam-root-4.09.0-2.0.6-plain/4.09.0/.opam-switch/install/coqide.install couldn't be installed:
- /builds/coq/opam-coq-archive/opam-root-4.09.0-2.0.6-plain/4.09.0/.opam-switch/build/coqide.dev/ide/coq_style.xml to /builds/coq/opam-coq-archive/opam-root-4.09.0-2.0.6-plain/4.09.0/share
- /builds/coq/opam-coq-archive/opam-root-4.09.0-2.0.6-plain/4.09.0/.opam-switch/build/coqide.dev/ide/coq.png to /builds/coq/opam-coq-archive/opam-root-4.09.0-2.0.6-plain/4.09.0/share
- /builds/coq/opam-coq-archive/opam-root-4.09.0-2.0.6-plain/4.09.0/.opam-switch/build/coqide.dev/ide/coq-ssreflect.lang to /builds/coq/opam-coq-archive/opam-root-4.09.0-2.0.6-plain/4.09.0/share
- /builds/coq/opam-coq-archive/opam-root-4.09.0-2.0.6-plain/4.09.0/.opam-switch/build/coqide.dev/ide/coq.lang to /builds/coq/opam-coq-archive/opam-root-4.09.0-2.0.6-plain/4.09.0/share
For example, see this build.
And by broken, I mean something has likely changed in the Makefile task the package calls on Coq master.
Ralf Jung (Aug 18 2020 at 06:29):yeah it is definitely broken already without the PR, just verified that locally
Ralf Jung (Aug 18 2020 at 06:30):these files are probably installed because of that directive in files/coqide.install:
share_root: [
"ide/coq.lang" {"coq/coq.lang"}
"ide/coq-ssreflect.lang" {"coq/coq-ssreflect.lang"}
"ide/coq.png" {"coq/coq.png"}
"ide/coq_style.xml" {"coq/coq_style.xml"}
]
I do not know what share_root means.
Hugo Herbelin (Aug 18 2020 at 07:31):As discussed at https://github.com/coq/opam-coq-archive/pull/1389, the ide/ should then be changed to ide/coqide/ in this coqide.install file.
Last updated: Dec 01 2023 at 07:01 UTC