0

The package coq-8.16.1ide (8.16.1-1~jammy~ppa191) is unusable, failing with error

Unpacking coq-8.16.1ide (8.16.1-1~jammy~ppa191) ...
dpkg: error processing archive /tmp/apt-dpkg-install-HG8l2q/08-coq-8.16.1ide_8.16.1-1~jammy~ppa191_amd64.deb (--unpack):
 trying to overwrite '/usr/bin/coqidetop.byte', which is also in package coq-8.16.1 8.16.1-1~jammy~ppa191

The launchpad build log supports this issue, listing

-rwxr-xr-x root/root  40656489 2022-11-26 19:09 ./usr/bin/coqidetop.byte
-rwxr-xr-x root/root  20789840 2022-11-26 19:09 ./usr/bin/coqidetop.opt

under both coq-8.16.1_8.16.1-1~jammy~ppa191_amd64.deb and coq-8.16.1ide_8.16.1-1~jammy~ppa191_amd64.deb. However, I did not list coqidetop in coq-8.16.1ide.install:

usr/bin/coqide
usr/share/man/man1/coqide*
usr/share/coq/coq.png
usr/share/coq/default.bindings
usr/share/coq/coq_style.xml
usr/share/coq/coq.lang
usr/share/coq/coq-ssreflect.lang
usr/lib/coqide/META
usr/lib/coqide/dune-package
usr/lib/coqide/opam
usr/doc/coqide/odoc-pages/index.mld  usr/share/doc/coqide/odoc-pages/index.mld
usr/doc/coqide/LICENSE   usr/share/doc/coqide/LICENSE
usr/doc/coqide/README.md usr/share/doc/coqide/README.md
usr/doc/coqide/FAQ       usr/share/doc/coqide/FAQ
debian/coqide.desktop    usr/share/applications

Moreover, nothing in rules writes to coq-8.16.1ide.install:

#!/usr/bin/make -f
# debian/rules for coq

# Uncomment this to turn on verbose mode.
#export DH_VERBOSE=1

# Build cache (for accelerating Debian debugging)
BUILDCACHE := $(wildcard ../coq.cache)

# This has to be exported to make some magic below work.
export CAML_LD_LIBRARY_PATH = $(shell pwd)/kernel/byterun

# Show full commands when building Coq
export VERBOSE=1

include /usr/share/ocaml/ocamlvars.mk

DESTDIR := $(CURDIR)/debian/tmp
ADDPREF := DESTDIR=$(DESTDIR)

PACKAGES := $(shell dh_listpackages)

COQ_VERSION := 8.16.1
COQ_ABI := $(COQ_VERSION)+$(OCAML_ABI)

CONFIGUREOPTS := -arch Linux -prefix /usr -mandir /usr/share/man \
  -configdir /etc/xdg/coq \
  -docdir /usr/doc \
   \


export OCAMLINIT_SED += \
  -e 's%@CoqVersion@%$(COQ_VERSION)%' \
  -e 's%@CoqABI@%$(COQ_ABI)%'

%:
        +dh $@ --with ocaml

# There is already a file named "build" in upstream sources, so the
# above rule is never called. We make it explicitly a phony rule here.
.PHONY: build
build:
        +dh $@ --with ocaml

.PHONY: override_dh_auto_configure
override_dh_auto_configure:
        ocamlfind query -format "%v" lablgtk3 || true
        ./configure $(CONFIGUREOPTS)

.PHONY: override_dh_auto_build
override_dh_auto_build:
ifeq ($(BUILDCACHE),)

# VALIDOPTS are the options given to coqchk; the value given here is
# the default one without -silent (-silent maybe cause buildd to
# timeout because of lack of output)

        $(MAKE) world STRIP=true
        $(MAKE) doc-stdlib-html
else
        rsync -a --exclude=debian --exclude=.git $(BUILDCACHE)/ .
endif
# Check that $(COQ_VERSION) has the right value
        ACTUAL_COQ_VERSION="$$(./bin/coqc --version | awk '/version/{print $$6}')"; \
        if [ "$$ACTUAL_COQ_VERSION" != "$(COQ_VERSION)" ]; then \
          echo "Please set COQ_VERSION to $$ACTUAL_COQ_VERSION in debian/rules"; \
          exit 2; \
        fi

.PHONY: override_dh_auto_test
override_dh_auto_test:
        $(MAKE) test-suite COMPLEXITY= || ( $(MAKE) -C test-suite report PRINT_LOGS=1; exit 1 ) || true

.PHONY: override_dh_auto_install
override_dh_auto_install::
        $(MAKE) $(ADDPREF) install
        find debian/tmp -regextype posix-awk \
          -regex '.*\.(cm[xiot]|cmxa|cmti|mli|ml|[ao])$$' \
          >> debian/libcoq-8.16.1-ocaml-dev.install
        find debian/tmp -regextype posix-awk \
          -regex '.*\.(vo|vos|v|glob)$$' -printf '%P\n' \
          >> debian/coq-8.16.1-theories.install
        find debian/tmp -name '*.cma' -printf '%P\n' \
          >> debian/libcoq-8.16.1-ocaml.install
        find debian/tmp -name '*.cmxs' -printf '%P\n' \
          >> debian/libcoq-8.16.1-ocaml.install

.PHONY: override_dh_install
override_dh_install:
        dh_install --fail-missing
        mkdir -p debian/coqide/usr/share/pixmaps && cp debian/coq.xpm debian/coqide/usr/share/pixmaps/coqide.xpm

.PHONY: override_dh_gencontrol
override_dh_gencontrol:
        for u in $(PACKAGES); do \
          echo 'F:OCamlABI=$(OCAML_ABI)' >> debian/$$u.substvars; \
          echo 'F:CoqABI=$(COQ_ABI)' >> debian/$$u.substvars; \
        done
        dh_gencontrol

.PHONY: override_dh_auto_clean
override_dh_auto_clean:
        dh_auto_clean || make distclean -k || make clean -k || true

#override_dh_auto_install::
#       find debian/tmp -name '*.cmxs' -printf '%P\n' \
#         >> debian/coq-8.16.1-theories.install

Is launchpad / debhelper / sbuild-package / dpkg-buildpackage somehow treating usr/bin/coqide as if it were usr/bin/coqide*? What's going on here, and how do I prevent the inclusion of usr/bin/coqidetop* in coq-8.16.1ide?

Jason Gross
  • 5,928
  • 1
  • 26
  • 53

0 Answers0