Stream: Dune devs & users

Topic: include_subdirs qualified

view this post on Zulip Rudi Grinberg (Jun 10 2022 at 15:11):

Hello,

The current state of include_subdirs bothers me. I see a couple of issues:

  1. coq doesn't support unqualified mode and never will
  2. the setting is per directory and affects both OCaml and Coq

Previously, I suggested the workaround of making include_subdirs separate for OCaml and Coq. Today, I don't like the idea anymore for the simple reason that coq users shouldn't need to know about this incantation at all.

With this in mind, I propose the following:

  1. include_subdirs will stop affecting coq stanzas
  2. declaring a coq.theory will also read subdirectories by default. This will only affect coq sources

Do you like this simplification?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 10 2022 at 15:12):

Indeed it sounds reasonable that we don't need to do include_subdirs for Coq

view this post on Zulip Emilio Jesús Gallego Arias (Jun 10 2022 at 15:13):

IMHO, I think we should move towards whatever direction we'd like to be when in using coq 2.0we break compatiblity with the current system

view this post on Zulip Emilio Jesús Gallego Arias (Jun 10 2022 at 15:14):

I guess that keeping the "Haskell style" structure sounds good

view this post on Zulip Rudi Grinberg (Jun 10 2022 at 15:30):

To be clear, this isn't a breaking change (as far as I can tell). It would just mean that (include_subdirs qualified) would be redundant

Last updated: Oct 13 2024 at 01:02 UTC