[coq] Default for mode vo/native according to coqc configuration#4722
[coq] Default for mode vo/native according to coqc configuration#4722proux01 wants to merge 1 commit intoocaml:mainfrom
Conversation
cf00923 to
0ca2a18
Compare
|
I'm afraid this is unsound at several levels; think that coqc may be produced by a rule itself and not present in the path. Actually in Dune 3.0 you may be able to write this correctly as the rules may depend on the build action of
Thus, no conditionals anymore, other than indeed the corresponding top level alias or install file which can be triggered by the user at will. |
|
Would we like to solve this directly, then we would have to compute the mode inside the build monad, so we should obtain native mode as a build rule [which is then correctly tracked by the dependencies]. Note also that As I mentioned, for native this is IMHO overkill, but could be cool as to add support for other stuff such as a |
|
Thanks for your comments and ideas. I agree this PR is way too broken. I also agree coqnative and the split package solution is the long term way to go. Unfortunately, this still requires some work on the opam repo side that noone is doing now (I may take a look but probably not soon). Meanwhile, any package switching to dune breaks coq-native (we already have the issue with multinomials). Here is a simpler idea : make the default value configurable at dune build time, just like for coqc. Things would then remain exactly as now, except when the coq-native package is installed in which case (mode native) would become the default. Since coqc is built the exact same way, dune and coqc should remain in sync. That could constitue a reasonnable short term solution until we actually switch to coqnative. |
|
Closing as this PR was mostly useful for discussion. It's not permitted to run external commands in dune this way. |
|
@rgrinberg sure but the problem remains: dune is stil incompatible with the coq-native OPAM package. This is IMHO the main obstacle to the use of dune to build any Coq library that could potentially be used with native (which, in practice, means virtually any Coq library). Or at least not without painful hacks and adding a confiure phase to tweak the dune files (see https://github.com/math-comp/multinomials ). I was told by @ejgallego this could be fixed with Dune 3.0 but since I don't know how, I'm unable to do it myself. Unfortunately today, due to this issue, we have no other solution than to recommend not to use dune to build Coq libraries. So to sum up, the PR is indeed wrong but the problem it adressed remains. |
|
@proux01 I added the infrastructure for Dune to see the Coq configuration in 3.4. Notably we can see if native is configured. It should be straightforward to use this. |
|
@Alizter great! I should have a look. Would you have a more precise pointer to the feature? |
|
@proux01 If you open an issue detailing how Dune should act depending on the output of the native config var from Coq I can implement it (maybe even this week). We should be releasing 3.6 soon too FYI. Notably #6049 exposes the variable to users in their dune file and as a side effect, gives us a way of checking the condition internally in Dune. However it might not be the smoothest API atm. |
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in #6049. This continues and finishes an earlier attempt to do someting similar in #4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
This is probably not perfect but is already making dune work with the coq-native OPAM package.