Source: mathcomp-analysis
Version: 0.6.4-3
Severity: serious
Justification: FTBFS
Tags: trixie sid ftbfs
User: lucas@debian.org
Usertags: ftbfs-20240115 ftbfs-trixie

Hi,

During a rebuild of all packages in sid, your package failed to build
on amd64.


Relevant part (hopefully):

make[2]: Entering directory '/<<PKGBUILDDIR>>'
COQDEP VFILES
COQC classical/boolp.v
COQC classical/mathcomp_extra.v
COQC theories/forms.v
COQC theories/altreals/xfinmap.v
File "./classical/mathcomp_extra.v", line 7, characters 9-28:
Error: The reference choice.Choice.mixin was not found in the current environment.

make[3]: *** [Makefile.coq:838: classical/mathcomp_extra.vo] Error 1

The full build log is available from: http://qa-logs.debian.net/2024/01/15/mathcomp-analysis_0.6.4-3_unstable.log

All bugs filed during this archive rebuild are listed at: https://bugs.debian.org/cgi-bin/pkgreport.cgi?tag=ftbfs-20240115;users=lucas@debian.org
or: https://udd.debian.org/bugs/?release=na&merged=ign&fnewerval=7&flastmodval=7&fusertag=only&fusertagtag=ftbfs-20240115&fusertaguser=lucas@debian.org&allbugs=1&cseverity=1&ctags=1&caffected=1#results

A list of current common problems and possible solutions is available at http://wiki.debian.org/qa.debian.org/FTBFS . You're welcome to contribute!

If you reassign this bug to another package, please mark it as 'affects'-ing this package. See https://www.debian.org/Bugs/server-control#affects

If you fail to reproduce this, please provide a build log and diff it with mine so that we can identify if something relevant changed in the meantime.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

This is a multi-part message in MIME format...

Your message dated Mon, 29 Jan 2024 09:35:04 +0000
with message-id <E1rUO2i-004wwJ-T1@fasolo.debian.org>
and subject line Bug#1060988: fixed in mathcomp-analysis 1.0.0-1
has caused the Debian Bug report #1060988,
regarding mathcomp-analysis: FTBFS: make[3]: *** [Makefile.coq:838: classical/mathcomp_extra.vo] Error 1
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)


--
1060988: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1060988
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems

Received: (at submit) by bugs.debian.org; 16 Jan 2024 19:45:13 +0000 X-Spam-Checker-Version: SpamAssassin 3.4.6-bugs.debian.org_2005_01_02
(2021-04-09) on buxtehude.debian.org
X-Spam-Level:
X-Spam-Status: No, score=-106.9 required=4.0 tests=BAYES_00,DKIMWL_WL_HIGH,
DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,FOURLA,
FROMDEVELOPER,SPF_HELO_NONE,SPF_NONE,T_SCC_BODY_TEXT_LINE,
UNPARSEABLE_RELAY,USER_IN_DKIM_WELCOMELIST,USER_IN_DKIM_WHITELIST
autolearn=ham autolearn_force=no
version=3.4.6-bugs.debian.org_2005_01_02
X-Spam-Bayes: score:0.0000 Tokens: new, 18; hammy, 150; neutral, 106; spammy,
0. spammytokens:
hammytokens:0.000-+--Hx-spam-relays-external:sk:stravin,
0.000-+--H*RT:sk:stravin, 0.000-+--Hx-spam-relays-external:311,
0.000-+--H*RT:108, 0.000-+--H*RT:311
Return-path: <lucas@debian.org>
Received: from stravinsky.debian.org ([20