Gaëtan Gilbert (Aug 12 2022 at 11:43): Gaëtan Gilbert (Aug 12 2022 at 11:43):it seems to be some mathcomp incompatibility
Gaëtan Gilbert (Aug 12 2022 at 11:43):eg https://gitlab.com/coq/coq/-/jobs/2844843761
Pierre-Marie Pédrot (Aug 12 2022 at 13:11):isn't this a problem with COQPATH instead?
Pierre-Marie Pédrot (Aug 12 2022 at 13:12):I had trouble already running the jasmin CI locally with the same error.
Pierre-Marie Pédrot (Aug 12 2022 at 13:12):Basically IIUC it's the only CI dev that uses dune install, so it puts the vo files in a different place.
Pierre-Marie Pédrot (Aug 12 2022 at 13:12):(I mean mathcomp-word, not jasmin)
Gaëtan Gilbert (Aug 12 2022 at 13:47):I don't know
it used to work though
Gaëtan Gilbert (Aug 12 2022 at 13:48):I guess it's https://github.com/jasmin-lang/coqword/commit/b94f0020377791cb3e1dbdc37731327f02b1355c
Pierre-Marie Pédrot (Aug 17 2022 at 14:24):I've written a quick sed-based PR, seems to work so far: https://github.com/jasmin-lang/jasmin/pull/223
Last updated: Oct 12 2024 at 12:01 UTC