Failed compilation of `deriving` using docker coq action

[zunction]

Hi @arthuraa,

While using docker coq action to test my software development which involves using your deriving library, I encounter some problems.

With the following specifications in my .opam:

depends: [
  "coq" { >= "8.10" }
  "coq-mathcomp-ssreflect" {= "1.10.0" | (= "dev")}
  "coq-deriving" {= "dev"} 
]

and using the image mathcomp/mathcomp:1.10.0-coq-8.10 from https://hub.docker.com/r/mathcomp/mathcomp, my github action return the error message:

 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
  Error:  The compilation of coq-deriving failed at "/usr/bin/make -j 2".

  #=== ERROR while compiling coq-deriving.dev ===================================#
  # context              2.0.7 | linux/x86_64 | ocaml-base-compiler.4.05.0 | https://coq.inria.fr/opam/extra-dev#2021-01-02 16:50
  # path                 ~/.opam/4.05.0/.opam-switch/build/coq-deriving.dev
  # command              /usr/bin/make -j 2
  # exit-code            2
  # env-file             ~/.opam/log/coq-deriving-109-2dea01.env
  # output-file          ~/.opam/log/coq-deriving-109-2dea01.out
  ### output ###
  # [...]
  # *** Warning: in file theories/instances/order.v, library mathcomp.order is required and has not been found in the loadpath!
  # *** Warning: in file theories/instances/order.v, library mathcomp.order is required and has not been found in the loadpath!
  # COQC theories/base.v
  # COQC theories/ind.v
  # COQC theories/tactics.v
  # COQC theories/infer.v
  # File "./theories/infer.v", line 2, characters 60-65:
  # Error: Unable to locate library order with prefix mathcomp.
  # 
  # make[2]: *** [CoqMakefile:659: theories/infer.vo] Error 1
  # make[1]: *** [CoqMakefile:321: all] Error 2
  # make: *** [Makefile:13: invoke-coqmakefile] Error 2

  <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
  +- The following actions failed
  | - build coq-deriving dev
  +- 
  - No changes have been performed

I cannot fully appreciate the error message for me to resolve the issue, thus would you able to help advice/suggest how I can over come this error message?

Thanks!

[gares]

Wasnt order.v shipped with mathcomp 1.11?

[zunction]

Wasnt order.v shipped with mathcomp 1.11?

@gares Thanks for the comment, I updated my mathcomp version to 1.11.0 by changing the image to mathcomp/mathcomp:1.11.0-coq-8.10 and my problem got resolved.

Perhaps coq-mathcomp-ssreflect 1.10 lacks order.v which I cannot seem to find from https://github.com/math-comp/math-comp/blob/master/CHANGELOG.md#1100---2019-11-29, thus the error i encountered.

[arthuraa]

@zunction Thanks for the report! I had indeed forgotten to update the dependencies on ssreflect. It should be fixed now.