Stream: math-comp devs

Topic: `bigenough` fails to build


view this post on Zulip Christian Doczkal (Nov 17 2021 at 07:57):

It looks to me that, as of last night, the bigenough package no longer builds against the current Coq master branch:

Error:  The compilation of coq-mathcomp-bigenough failed at "/usr/bin/make -j 2".
[...]
 # File "./bigenough.v", line 87, characters 46-52:
 # Error: Syntax error: [ident] expected after 'in' (in [hloc]).

view this post on Zulip Karl Palmskog (Dec 07 2021 at 13:08):

any chance to merge this (seemingly simple) PR soon? Would be nice to have opam archive CI working for a bunch of packages in extra-dev (including a current PR to the Coq opam archive): https://github.com/math-comp/bigenough/pull/5

cc: @Cyril Cohen @Kazuhiko Sakaguchi

view this post on Zulip Cyril Cohen (Dec 07 2021 at 16:27):

Karl Palmskog said:

any chance to merge this (seemingly simple) PR soon? Would be nice to have opam archive CI working for a bunch of packages in extra-dev (including a current PR to the Coq opam archive): https://github.com/math-comp/bigenough/pull/5

cc: Cyril Cohen Kazuhiko Sakaguchi

Hi, ... I'm pretty reluctant to merge without CI, I will merge as soon as a CI is added and passes

view this post on Zulip Pierre Roux (Dec 07 2021 at 19:45):

@Cyril Cohen I just added a Github action file to the PR, but you may have to do something to activate it : https://github.com/math-comp/bigenough/pull/5

view this post on Zulip Karl Palmskog (Dec 08 2021 at 11:38):

I have to admit I don't understand the problem with meta.yml brought up in https://github.com/coq/opam-coq-archive/pull/1975 -- everything seems to look good to me in the bigenough repo. However, the opam archive PR got stuck in linting for an old opam file that was modified.

view this post on Zulip Théo Zimmermann (Dec 08 2021 at 11:44):

I don't think this was the point raised by Cyril, but rather that the 1.0.0 version had:

build: [ make "-j" "%{jobs}%" "COQEXTRAFLAGS+=-native-compiler yes" {coq-native:installed & coq:version < "8.13~" } ]

view this post on Zulip Karl Palmskog (Dec 08 2021 at 11:47):

ah, then I understand. I think this can actually be handled by the current templates, the variable make_target.

view this post on Zulip Karl Palmskog (Dec 08 2021 at 11:48):

I don't have time to do a PR now though, maybe later tonight.


Last updated: Aug 11 2022 at 02:03 UTC