As you know, the latest mathcomp is continuously rebuilt with coq-dev (until coq dev "diverges" and can't build the released mathcomp anymore).
Since today, it happens mathcomp:2.2.0-coq-dev's build fails because of elpi:
#6 90.35 The following actions will be performed:
#6 90.35 - install cppo 1.6.9 [required by ppx_deriving]
#6 90.35 - install ppx_derivers 1.2.1 [required by ppx_deriving]
#6 90.35 - install menhirLib dev [required by menhir]
#6 90.35 - install menhirSdk dev [required by menhir]
#6 90.35 - install easy-format 1.3.4 [required by atd]
#6 90.35 - install cmdliner 1.3.0 [required by atdts]
#6 90.35 - install seq base [required by re, yojson]
#6 90.35 - install ocaml-compiler-libs v0.12.4 [required by ppxlib]
#6 90.36 - install camlp-streams 5.0.1 [required by biniou]
#6 90.36 - install sexplib0 v0.16.0 [required by ppxlib]
#6 90.36 - install stdlib-shims 0.3.0 [required by coq-elpi]
#6 90.36 - install menhir dev [required by elpi]
#6 90.36 - install yojson 2.2.1 [required by atdgen]
#6 90.36 - install re 1.11.0 [required by elpi]
#6 90.36 - install biniou 1.2.2 [required by atdgen]
#6 90.36 - install ppxlib 0.32.1 [required by elpi]
#6 90.36 - install atd 2.15.0 [required by atdgen, atdts]
#6 90.36 - install atdgen-runtime 2.15.0 [required by atdgen]
#6 90.36 - install ppx_deriving 6.0.2 [required by elpi]
#6 90.36 - install atdts 2.15.0 [required by elpi]
#6 90.36 - install atdgen 2.15.0 [required by elpi]
#6 90.36 - install elpi 1.18.1 [required by coq-mathcomp-ssreflect]
#6 90.36 - install coq-elpi dev [required by coq-hierarchy-builder]
#6 90.36 - install coq-hierarchy-builder dev [required by coq-mathcomp-ssreflect]
#6 90.36 - install coq-mathcomp-ssreflect 2.2.0* [required by coq-mathcomp-fingroup]
#6 90.36 - install coq-mathcomp-fingroup 2.2.0* [required by coq-mathcomp-algebra]
#6 90.36 - install coq-mathcomp-algebra 2.2.0* [required by coq-mathcomp-solvable]
#6 90.36 - install coq-mathcomp-solvable 2.2.0* [required by coq-mathcomp-field]
#6 90.36 - install coq-mathcomp-field 2.2.0* [required by coq-mathcomp-character]
#6 90.36 - install coq-mathcomp-character 2.2.0*
…
#6 353.7 ### output ###
#6 353.7 # [...]
#6 353.7 # CAMLC -c src/coq_elpi_arg_HOAS.ml
#6 353.7 # CAMLC -c src/coq_elpi_builtins_arg_HOAS.ml
#6 353.7 # CAMLC -c src/coq_elpi_builtins_HOAS.ml
#6 353.7 # CAMLC -c src/coq_elpi_builtins_synterp.ml
#6 353.7 # CAMLC -c src/coq_elpi_builtins.ml
#6 353.7 # File "src/coq_elpi_builtins.ml", line 447, characters 28-32:
#6 353.7 # 447 | let nmiss = List.length miss in
#6 353.7 # ^^^^
#6 353.7 # Error: This expression has type Names.Name.t list * int
#6 353.7 # but an expression was expected of type 'a list
#6 353.7 # make[1]: *** [Makefile.coq:730: src/coq_elpi_builtins.cmo] Error 2
#6 353.7 # make: *** [Makefile:50: build-core] Error 2
#6 353.7
#6 356.1
#6 356.1
do you think this can be fixed?
(Cc @Enrico Tassi @Pierre Roux)
I've switched master to dune. The master branch builds with all supported coq versions via ppx_optcomp.
I may need to fix the coq-elpi.dev opam file, since the coq-master branch is soon to be dropped.
Sorry for the distruption.
Last updated: Oct 13 2024 at 01:02 UTC