Dune: Dune-based Coq projects FTBFS since coq/coq#8642

Created on 4 Nov 2019 · 4Comments · Source: ocaml/dune

Kind: bug

Since https://github.com/coq/coq/pull/8642, coqdep outputs another line involving .vos files:

$ cat _build/default/BigN/BigN.v.d
BigN/BigN.vo BigN/BigN.glob BigN/BigN.v.beautified BigN/BigN.required_vo: BigN/BigN.v SpecViaZ/NSig.vo SpecViaZ/NSigNAxioms.vo BigN/NMake.vo
BigN/BigN.vio: BigN/BigN.v SpecViaZ/NSig.vio SpecViaZ/NSigNAxioms.vio BigN/NMake.vio
BigN/BigN.vos BigN/BigN.vok BigN/BigN.required_vos: BigN/BigN.v SpecViaZ/NSig.vos SpecViaZ/NSigNAxioms.vos BigN/NMake.vos

As Dune's (using coq 0.1) is not aware of these .vos files, building any Dune-based Coq project (e.g. coq-bignums) with a recent coq.dev will now fail here…

Cc @ejgallego @charguer FYI

Source

erikmd

Most helpful comment

I think we should:

make Dune's coqdep parsing more resilient.
restore old coqdep behavior, so it only produces the rules when the .vos mode is enabled, this will allow dune 1.x to work with Coq's 8.11

ejgallego on 4 Nov 2019

👍3

All 4 comments

Correct me if I'm wrong, but I suspect that Dune's coq_rules ought to be version dependent somehow, else there is no way it can deal with evolution of the coqdep tool. Doesn't this qualify as a Dune bug?

charguer on 4 Nov 2019

I think we should:

make Dune's coqdep parsing more resilient.
restore old coqdep behavior, so it only produces the rules when the .vos mode is enabled, this will allow dune 1.x to work with Coq's 8.11

ejgallego on 4 Nov 2019

👍3