metacoq icon indicating copy to clipboard operation
metacoq copied to clipboard

coq-metacoq-translations.dev failing in bench

Open SkySkimmer opened this issue 3 years ago • 3 comments

For instance https://gitlab.com/coq/coq/-/jobs/3054016499

- File "./sigma.v", line 2, characters 0-47:
- Error:
- Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"../template-coq/./src/template_coq.cmxs: cannot open shared object file: No such file or directory\")")
- Findlib paths:
- ../template-coq/
(many coq-core and user-contrib paths)
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq/PCUIC
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq/Erasure
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq/SafeChecker
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq/Template
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq/Template/common
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq/Template/utils
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq/Template/utils/canonicaltries
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/MetaCoq/Template/TemplateMonad
(more paths)
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Equations
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Equations/Type
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Equations/HoTT
- /home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Equations/Prop
(more paths)

SkySkimmer avatar Sep 21 '22 07:09 SkySkimmer

Ah yes, I know how to fix it

mattam82 avatar Sep 21 '22 07:09 mattam82

https://github.com/coq/opam-coq-archive/blob/3f9aee321cab92699fc724abd9ba269542319f77/extra-dev/packages/coq-metacoq-translations/coq-metacoq-translations.dev/opam#L14 should be using bash not sh

SkySkimmer avatar Sep 21 '22 13:09 SkySkimmer

@SkySkimmer This should be fixed now, can you check?

mattam82 avatar Sep 22 '22 12:09 mattam82