Skip to content
Snippets Groups Projects

Dune build compatible with Rocq 9.0.0.

Open Dune build compatible with Rocq 9.0.0.
rodolphe/dune-rocq into master
2 unresolved threads
Open Rodolphe Lepigre requested to merge rodolphe/dune-rocq into master
2 unresolved threads

Merge request reports

Merge request pipeline #121356 passed

Stage: build

Merge request pipeline passed for 9ec482a5

Ready to merge by members who can write to the target branch.
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
    • Rodolphe Lepigre
      Rodolphe Lepigre @lepigre
      Author Maintainer

      I just realized that this will not be compatible with earlier versions of Rocq, since they don't have an Stdlib theory. I'm not sure how to fix this without generating dune files, which I'd rather avoid.

    • Ralf Jung
      Ralf Jung @jung
      Owner

      Wait so one can't have dune files that are compatible with 8.20 and 9.0? That's terrible. I'll keep using makefiles for a while if this is how mature the dune stuff is...

      For this concrete PR, I consider you to be the maintainer of our dune files. So if you think it's fine to land this, I'm also fine with it. The changelog should explicitly call this out though.

    • Rodolphe Lepigre
      Rodolphe Lepigre @lepigre
      Author Maintainer

      Yep, you got this right...

      I think we should get this in, but I'll need to change CI so that the dune build runs on 9.0, as this is not the case at the moment.

    • Please register or sign in to reply
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
dune
5 5 (:standard ; Keeping the default flags.
6 6 ; Add custom flags (to be kept in sync with _CoqProject).
  • Ralf Jung
    Ralf Jung @jung
    Owner

    This does not change _CoqProject so presumably they are not in sync any more then?

    This is exactly why I didn't want a copy of these flags to begin with. ;)

  • Rodolphe Lepigre
    Rodolphe Lepigre @lepigre
    Author Maintainer

    Hehe :smile:

    I know how to fix this, but that require generating the _CoqProject file. Is that something you guys would be open to?

  • Rodolphe Lepigre
    Rodolphe Lepigre @lepigre
    Author Maintainer

    Actually, the _CoqProject had been modified without following the instructions to also fix the dune file. Not sure who did it, but I can't blame them. :wink:

  • Ralf Jung
    Ralf Jung @jung
    Owner

    I know how to fix this, but that require generating the _CoqProject file. Is that something you guys would be open to?

    That would add even more hacks to our Makefile I guess... not sure. I presume the list of .v files would then also be auto-generated, so this also depends on whether @robbertkrebbers would be fine with that. Either way, let's not do that in this MR.

    Another option might be to have a CI check which ensures consistency.

    Actually, the _CoqProject had been modified without following the instructions to also fix the dune file.

    oops

  • Please register or sign in to reply
  • Rodolphe Lepigre mentioned in merge request !604

    mentioned in merge request !604

    • Please register or sign in to reply