Bug#1056062: coq: FTBFS in sid (dune update?)

[julien.puydt@gmail.com]

Hi,

Le jeudi 16 novembre 2023 à 16:45 +0100, Gianfranco Costamagna a
écrit :
> Source: coq
> Version: 8.17.0+dfsg-1
> Severity: serious
> 
> Hello,
> 
> https://tests.reproducible-builds.org/debian/rb-pkg/unstable/amd64/coq.html
> 
> As said here, there is a build failure due to probably new dune or
> something similar.
> 
>
> I can reproduce locally, but not always, looks some concurrency issue
> but also running dune with -j1 doesn't fix the issue.


I couldn't reproduce your failure even after several compilation tries,
neither with the current 8.17.0+dfsg-1 nor with the next 8.18.0+dfsg-1.

> $ (cd _build/default && /usr/bin/bash -e -u -o pipefail -c
> 'doc/stdlib/make-library-index doc/stdlib/index-list.html
> doc/stdlib/hidden-files')
> Building file index-list.prehtml... Error: none of doc/stdlib/index-
> list.html and doc/stdlib/hidden-files mention
> theories/Arith/Between.v
> grep: tmp: No such file or directory
> grep: tmp: No such file or directory
> 
> This is probably the culprit of the issue, but I don't really
> understand why this is not found
> 

I checked doc/stdlib/index-list.html.template in both 8.17.0+dfsg-1 and
8.18.0+dfsg-1, and they *do* mention theories/Arith/Between.v... how
could that line disappear? Is it always theories/Arith/Between.v or
sometimes another file? The compilation of the .html.template to .html
might fail silently for you and then you see a later breakage?

> and also why running it manually works
> bash -e -u -o pipefail -c 'doc/stdlib/make-library-index
> doc/stdlib/index-list.html doc/stdlib/hidden-files'
> Building file index-list.prehtml...
> Done
> 
> Sorry for not providing a patch, but I really don't have much
> knowledge about this build system, and despite my efforts I'm still
> failing

The fact that the only error message doesn't make sense and the problem
isn't guaranteed to happen is puzzling.

I'm using sbuild to compile my sources, with an unstable schroot I keep
up to date, and it now uses ocaml-dune 3.11.1-1 to compile, just like
in your failure log :-/

Thanks,

JP