Stream: Coq devs & plugin devs

Topic: fiat-parser CI


view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:53):

are we properly testing fiat-parser in our CI?

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:53):

it's not using the right template since the 8.14 branch

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:53):

I've added the set of files for 8.15 but I now get weird errors

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:54):

File "./src/QueryStructure/Specification/Representation/Tuple.v", line 21, characters 0-28:
Error: Argument heading is a trailing implicit, so it can't be declared non
maximal. Please use { } instead of [ ].

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:54):

cc @Jason Gross

view this post on Zulip Jason Gross (Jul 20 2021 at 23:26):

The overlay seems to work fine on Coq's CI though? Is this an error you're getting locally? Note that the fiat CI uses targets fiat-core parsers and Coq's CI uses fiat-core parsers parsers-examples; perhaps you're trying the build with a larger target which AFAIK we haven't supported since 8.9?

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 08:56):

Ah, this is probably it.

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 08:56):

it's a bit weird to have code around that is known not to compile though

view this post on Zulip Jason Gross (Jul 22 2021 at 00:50):

Yeah, this is the issue with maintaining a CI for mostly legacy reasons out of a larger legacy codebase


Last updated: Oct 16 2021 at 02:03 UTC