Stream: Elpi users & devs

Topic: mathcomp/mathcomp:2.2.0-coq-dev FTBFS since today b/o elpi


view this post on Zulip Erik Martin-Dorel (Jun 24 2024 at 21:01):

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)

view this post on Zulip Enrico Tassi (Jun 24 2024 at 21:05):

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