Stream: Coq devs & plugin devs

Topic: jasmin failing in CI


view this post on Zulip Gaëtan Gilbert (Aug 12 2022 at 11:43):

it seems to be some mathcomp incompatibility

view this post on Zulip Gaëtan Gilbert (Aug 12 2022 at 11:43):

eg https://gitlab.com/coq/coq/-/jobs/2844843761

view this post on Zulip Pierre-Marie Pédrot (Aug 12 2022 at 13:11):

isn't this a problem with COQPATH instead?

view this post on Zulip Pierre-Marie Pédrot (Aug 12 2022 at 13:12):

I had trouble already running the jasmin CI locally with the same error.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Aug 12 2022 at 13:12):

(I mean mathcomp-word, not jasmin)

view this post on Zulip Gaëtan Gilbert (Aug 12 2022 at 13:47):

I don't know
it used to work though

view this post on Zulip Gaëtan Gilbert (Aug 12 2022 at 13:48):

I guess it's https://github.com/jasmin-lang/coqword/commit/b94f0020377791cb3e1dbdc37731327f02b1355c

view this post on Zulip 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: Feb 01 2023 at 15:04 UTC