Hi,
Sorry for not following up on this earlier.
Those two packages (lib{mathcomp,ssreflect}-coq) only contain .vo files,
which are AFAIK architecture-independent.
Unfortunately, coq_makefile doesn't support not building .vo files
(I don't even know if it is possible), and I wouldn't feel comfortable
maintaining even more build-system patches.
It's a bit of a cop-out, but I would like to suggest moving forward
with this and opening a bug against mathcomp for not building arch-indep
packages.
Best,
nicoo
On Sun, Jul 31, 2016 at 11:56:15AM +0200, Stéphane Glondu wrote:
> On 30/07/2016 20:06, Ralf Treinen wrote:
> > > > 2) Another remark concerns the organisation of debian/rules. You now have
> > > > two Architecture=any packages, these will be build by the autobuilders.
> > > > These packages alone should be quick to compile. [...]
> > > > Do you think you can do this ? This would also allow you to move
> > > > some of the Build-Dependencies into Build-Depends-Indep.
> > >
> > > I'm not sure the coqdoc documentation can be built without building the
> > > rest, but I can try at some point.
> >
> > I don't unerstand. AFAICS, there is no coqdoc documentation in the
> > libsssreflect-ocaml[-dev] packages.
> >
> > My request was about building the architecture-dependant packages. There
> > is nothing to be gained from optimizing building the architecture-independant
> > packages.
>
> I think Ralf was talking about not building lib{mathcomp,ssreflect}-coq
> (which take most of the time) when only arch any packages are requested
> (which is the case on buildds).
>
> BTW, don't libmathcomp-coq and libssreflect-coq contain cmxs files? If so,
> they should be arch any. I ask because of this changelog entry in coq
> 8.5~beta2+dfsg-1:
>
> > [...]
> > * coq-theories is now arch any, since it contains .coq-native/ directories
> > (i.e. cmxs files for native compute)
> > [...]
>
> which made me think that, in general, theories should now be arch any.
> Enrico?
>
>
> Cheers,
>
> --
> Stéphane
>
Attachment:
signature.asc
Description: PGP signature