add support for depending on installed targets #1155
Labels
Comments
|
@ejgallego, could you confirm that you've encountered this issue as well? I think it would be nice if |
|
Supporting |
I think that would be useful to copy files around indeed... |
|
BTW, we already extend the |
|
@rgrinberg indeed, thanks! I think that would be useful for us. Sphinx documentation in Coq depends on This would simplify for example splitting the documentation to its own OPAM package [as it has non-trivial build-deps] |
Is that true? I thought this only worked for public binaries. Also, I would prefer a more fine grained PATH for actions. For example, I think it would be best that we only appended |
So does
It is guaranteed that the action in the second dune file will see the local version of
Note that it's not restricted to the search path, currently it's the case for all files. For instance, if a command states that it depends only on files a and b in the current directory, it will still see all the other files that happen that happen to be there when the command is executed. |
|
Note, I am faking this by inserting a dummy |
|
Yup, you've understood correctly. I understand that we can't create proper sandboxes for these actions, but I think that we can at least be careful about the local additions to the PATH that we make to dune. |
|
How would you implement it? |
|
A simple approach would be the following:
|
|
Note that it would be useful for us not to be able to depend only in |
|
We have |
|
I get the same |
|
BTW, this might be relevant to this discussion: #1185. This + the |
|
Another thing that would be useful for us is to be able to depend on Hopefully we wouldn't need in the future when all the binaries of Coq's test-suite are built by dune themselves, but it would help with the plumbing. Consider this as not very important tho. |
What are the use case for this? I think it's always preferably to depend on the concrete artifacts when possible. |
Interaction with legacy make-based targets, that expect The thing is that in Coq we ought to have a transition phase, the project and ecosystem is too large as not to be able to afford that. On the other hand, we can find workarounds so not big deal. |
|
And |
|
|
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Oct 13, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Oct 13, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Oct 13, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Oct 14, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Oct 14, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Oct 14, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Oct 18, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Oct 18, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Oct 23, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
|
I think the design phase for this feature, has ended. For now, let's just implement the least controversial bits that we agree on. That means we can throw out the sandboxing features for now. Summary of the concrete plan:
@ejgallego are those two features satisfactory for you? @emillon @diml unless there's disapproval, I will start working on this. |
|
No objection, however it's not clear to me how I don't find this particularly intuitive, it would seem simpler to me to just say that an executable is available everywhere via the |
Sure, thanks, I think that would improve developer workflow quite a bit. The problem is that Coq doesn't know how to locate things that are not installed. So when you want to run a test, you need to depend on the installed I think that any simple solution that allows us to do that would work. For binaries we could do with a very simple We could also solve our problem by depending on the build object themselves, and having something like #1185 available, but maybe the way proposed here is simpler. |
That was the idea.
Note that this isn't flexible enough. It's common enough that you want to use a different executable under the same name in a single project. The If it's the magic of However, I don't think the behavior that I'm proposing is so magical. Unless the current behavior with public executables is considered magical. |
|
Not magical, but not necessarily intuitive either. It seems odd to me that using a percent form would modify the execution context in this way. Using a specific action seems better, however the name should reflect that it is modifying the execution context, for instance
I feel like this is too local though. Doing this via the |
|
@ejgallego would the following work for you: And note that action rules under this environment would now be able to use the local binary names for dependencies: |
|
Using env looks a bit strange doesn't it? It seems like it would need a bit of duplication but I need to think. Why does |
It shouldn't be so bad as the env stanza applies to all stanzas in its directory recursively. So if your tests are in 1 dir, that's all you will need.
That's a separate issue. We'll fix that regardless. Note that |
Still feels to me a bit out of place, imagine I have a rule: using the env I cannot reflect that |
|
So to be clear our problem really is implicit dependencies on installed targets, [for example Sphinx depending on coqtop] In actions where the name of the executable appears we tend to be OK using their private version. |
|
@ejgallego the idea is that you'd write something like this: (env (_ (bins (../x/foo.exe as foo))))
(rule
(deps %{bin:foo})
(action (run some-prog-that-needs-foo)))
(rule
(deps %{bin:foo})
(action (run some-prog-that-needs-foo)))
...Because of the |
Ah, very cool then, thanks very much! We only depend on public binaries / data files but indeed i can see how this is useful in tests [currently indeed we are installing a couple of test-only binaries for this reason] [small off tangent, in our root Dune file, we cannot do: as indeed the wildcard doesn't take effect here. Does this merit a bug?] |
|
Yh, this merits a bug. Currently, the semantic is: use the first matching pattern. But we could allow to have several env stanzas in the same file for this case for instance. |
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Nov 6, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Nov 7, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Nov 7, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Nov 12, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Nov 13, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Nov 13, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Nov 17, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
ejgallego
added a commit
to ejgallego/coq
that referenced
this issue
Nov 21, 2018
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
rgrinberg
added a commit
to rgrinberg/opam-repository
that referenced
this issue
Nov 29, 2018
CHANGES: - Expand variables in `install` stanzas (ocaml/dune#1354, @mseri) - Add predicate language support for specifying sub directories. This allows the use globs, set operations, and special values in specifying the sub directories used for the build. For example: `(dirs :standard \ lib*)` will use all directories except those that start with `lib`. (ocaml/dune#1517, ocaml/dune#1568, @rgrinberg) - Add `binaries` field to the `(env ..)` stanza. This field sets and overrides binaries for rules defined in a directory. (ocaml/dune#1521, @rgrinberg) - Fix a crash caused by using an extension in a project without dune-project file (ocaml/dune#1535, fix ocaml/dune#1529, @diml) - Allow `%{bin:..}`, `%{exe:..}`, and other static expansions in the `deps` field. (ocaml/dune#1155, fix ocaml/dune#1531, @rgrinberg) - Fix bad interaction between on-demand ppx rewriters and using multiple build contexts (ocaml/dune#1545, @diml) - Fix handling of installed .dune files when the backend is declared via a `dune` file (ocaml/dune#1551, fixes ocaml/dune#1549, @diml) - Add a `--stats` command line option to record resource usage (ocaml/dune#1543, @diml) - Fix `dune build @doc` deleting `highlight.pack.js` on rebuilds, after the first build (ocaml/dune#1557, @aantron). - Allow targets to be directories, which Dune will treat opaquely (ocaml/dune#1547, @jordwalke) - Support for OCaml 4.08: `List.t` is now provided by OCaml (ocaml/dune#1561, @ejgallego) - Exclude the local esy directory (`_esy`) from the list of watched directories (ocaml/dune#1578, @andreypopp) - Fix the output of `dune external-lib-deps` (ocaml/dune#1594, @diml) - Introduce `data_only_dirs` to replace `ignored_subdirs`. `ignored_subdirs` is deprecated since 1.6. (ocaml/dune#1590, @rgrinberg)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
It would be useful to be able to depend on installed targets in other dune files, for example for use in aliases. One example is in the OCaml Platform repository (which vendors common build tools). We currently have this in our toplevel dune file:
but it would be much nicer to be able to address the dependencies via
(bin opam)to reflect their installed locations. Trying to use%{bin:opam}currently results inError: %{bin:..} isn't allowed in this position.The text was updated successfully, but these errors were encountered: