Christian Doczkal (Nov 17 2021 at 07:57): 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]).
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
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/5cc: 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
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
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.
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~" } ]
ah, then I understand. I think this can actually be handled by the current templates, the variable make_target.
Karl Palmskog (Dec 08 2021 at 11:48):I don't have time to do a PR now though, maybe later tonight.
Last updated: Oct 13 2024 at 01:02 UTC