Pierre-Marie Pédrot (Jul 20 2021 at 15:53): Pierre-Marie Pédrot (Jul 20 2021 at 15:53):are we properly testing fiat-parser in our CI?
Pierre-Marie Pédrot (Jul 20 2021 at 15:53):it's not using the right template since the 8.14 branch
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
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 [ ].
cc @Jason Gross
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?
Pierre-Marie Pédrot (Jul 21 2021 at 08:56):Ah, this is probably it.
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
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 13 2024 at 01:02 UTC