Stream: Coq devs & plugin devs

Topic: coqide.dev package broken


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

view this post on Zulip Ralf Jung (Aug 18 2020 at 06:29):

yeah it is definitely broken already without the PR, just verified that locally

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

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