Bug#1070787: coq-corn: produces empty binary

[julien . puydt]

Hi,

Le jeudi 09 mai 2024 à 09:45 +0200, Gianfranco Costamagna a écrit :
> Source: coq-corn
> Version: 8.19.0-1
> Severity: serious
> 
> Hello, looks like there are at least two issues:
> 1) fta directory was stripped on tarball import, not sure how and
> why, because the upstream repo still contains it
> (this makes autopkgtest fail)
> 
> 2) the produced binary package looks empty
> 
> https://packages.debian.org/sid/amd64/libcoq-corn/filelist
> /usr/share/doc/libcoq-corn/changelog.Debian.gz
> /usr/share/doc/libcoq-corn/copyright
> /var/lib/coq/md5sums/libcoq-corn.checksum
> 
> For sure changes in configure.sh are a possible culprit

What happened?

I ran "uscan -v" in my ~/Debian/ocaml/ directory. At one point coq-
corn's tarball got downloaded as 8.19.0.tar.gz and symlinked to coq-
corn_8.19.0.tar.gz ; then later coq-math-classes' tarball got
downloaded as 8.19.0.tar.gz and symlinked to coq-math-
classes_8.19.0.tar.gz (they use the same version as the latest Coq they
target...).

The end result is that the final 8.19.0.tar.gz was really the coq-math-
classes tarball, but there were two symlinks to it! So when I imported
the tarballs (gbp import-orig ../correct-package-source-
name_8.19.0.tar.gz) and updated the packages, I ended up with the wrong
sources in the coq-corn directory! And since the Debian packages for
both look pretty much the same, I didn't notice anything amiss when
compiling.

That is really stupid ; perhaps I should file a bug report against
uscan because it's a sort of race condition...

In any case, thanks for the report, I'll fix the mess!

Cheers,

J.Puydt

Bug#1070787: coq-corn: produces empty binary

[Gianfranco Costamagna]

Source: coq-corn
Version: 8.19.0-1
Severity: serious

Hello, looks like there are at least two issues:
1) fta directory was stripped on tarball import, not sure how and why, because 
the upstream repo still contains it
(this makes autopkgtest fail)

2) the produced binary package looks empty

https://packages.debian.org/sid/amd64/libcoq-corn/filelist
/usr/share/doc/libcoq-corn/changelog.Debian.gz
/usr/share/doc/libcoq-corn/copyright
/var/lib/coq/md5sums/libcoq-corn.checksum


For sure changes in configure.sh are a possible culprit

diff --git a/configure.sh b/configure.sh
index fae7a08..c696c8f 100755
--- a/configure.sh
+++ b/configure.sh
@@ -1,11 +1,3 @@
-#!/usr/bin/env sh
-
-# Produce files Make and Makefile
-
-cp -f Make.in Make
-
-DIRECTORIES="algebra complex coq_reals fta ftc liouville logic metrics model raster 
reals tactics transc order metric2 stdlib_omissions util classes ode"
-
-find $DIRECTORIES -name "*.v" >>Make
-
-${COQBIN}coq_makefile -f Make -o Makefile
+#!/bin/sh
+cp -f _CoqProject.in _CoqProject
+find . -name "*.v" |grep -v misc/benchmarks_nobuild.v >> _CoqProject

thanks for having a look

Gianfranco


OpenPGP_signature.asc
Description: OpenPGP digital signature