-
Notifications
You must be signed in to change notification settings - Fork 412
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[question] enabled_if in executable stanza? #1690
[question] enabled_if in executable stanza? #1690
Comments
This is related to #1445. That seems fine to me. |
Thanks @diml , I may try to give it a go then. |
I have no objection to |
It is already on its own package, however in a composed build some targets such as |
Note that indeed I am not strongly defending this; maybe a better system for package subsets [so we could write "build all .install but coqide.install"] could work better. The thing indeed is that the default target for Coq is usually the composed build [as we are fixing plugins] |
Yup, that's indeed a problem but Currently my proposal for this feature is something like: #1642 So you'd be able to do something like: The question is, how to create such a target? We basically would like to exclude any targets from an alias that depend on a missing optional library somehow. |
Indeed if we just kept |
@ejgallego Do you have a solution to your problem, that is currently implemented? |
@bobot for now we are using different packages and do I need to think a bit more about this but first I'd like to get the whole Coq universe building under Dune, and see what would be the best option to allow missing dependencies and still have an usable build. |
We can add |
|
Adding |
@voodoos this is a good thing to contribute if you have time |
…lugin, dune-private-libs and dune-glob (2.3.0) CHANGES: - Improve validation and error handling of arguments to `dune init` (ocaml/dune#3103, fixes ocaml/dune#3046, @shonfeder) - `dune init exec NAME` now uses the `NAME` argument for private modules (ocaml/dune#3103, fixes ocaml/dune#3088, @shonfeder) - Avoid linear walk to detect children, this should greatly improve performance when a target has a large number of dependencies (ocaml/dune#2959, @ejgallego, @aalekseyev, @Armael) - [coq] Add `(boot)` option to `(coq.theories)` to enable bootstrap of Coq's stdlib (ocaml/dune#3096, @ejgallego) - [coq] Deprecate `public_name` field in favour of `package` (ocaml/dune#2087, @ejgallego) - Better error reporting for "data only" and "vendored" dirs. Using these with anything else than a strict subdirectory or `*` will raise an error. The previous behavior was to just do nothing (ocaml/dune#3056, fixes ocaml/dune#3019, @voodoos) - Fix bootstrap on bytecode only switches on windows or where `-j1` is set. (ocaml/dune#3112, @xclerc, @rgrinberg) - Allow `enabled_if` fields in `executable(s)` stanzas (ocaml/dune#3137, fixes ocaml/dune#1690 @voodoos) - Do not fail if `ocamldep`, `ocamlmklib`, or `ocaml` are absent. Wait for them to be used to fail (ocaml/dune#3138, @rgrinberg) - Introduce a `strict_package_deps` mode that verifies that dependencies between packages in the workspace are specified correctly. (@rgrinberg, ocaml/dune#3117)
…lugin, dune-private-libs and dune-glob (2.3.0) CHANGES: - Improve validation and error handling of arguments to `dune init` (ocaml/dune#3103, fixes ocaml/dune#3046, @shonfeder) - `dune init exec NAME` now uses the `NAME` argument for private modules (ocaml/dune#3103, fixes ocaml/dune#3088, @shonfeder) - Avoid linear walk to detect children, this should greatly improve performance when a target has a large number of dependencies (ocaml/dune#2959, @ejgallego, @aalekseyev, @Armael) - [coq] Add `(boot)` option to `(coq.theories)` to enable bootstrap of Coq's stdlib (ocaml/dune#3096, @ejgallego) - [coq] Deprecate `public_name` field in favour of `package` (ocaml/dune#2087, @ejgallego) - Better error reporting for "data only" and "vendored" dirs. Using these with anything else than a strict subdirectory or `*` will raise an error. The previous behavior was to just do nothing (ocaml/dune#3056, fixes ocaml/dune#3019, @voodoos) - Fix bootstrap on bytecode only switches on windows or where `-j1` is set. (ocaml/dune#3112, @xclerc, @rgrinberg) - Allow `enabled_if` fields in `executable(s)` stanzas (ocaml/dune#3137, fixes ocaml/dune#1690 @voodoos) - Do not fail if `ocamldep`, `ocamlmklib`, or `ocaml` are absent. Wait for them to be used to fail (ocaml/dune#3138, @rgrinberg) - Introduce a `strict_package_deps` mode that verifies that dependencies between packages in the workspace are specified correctly. (@rgrinberg, ocaml/dune#3117) - Make sure the `@all` alias is defined when no `dune` file is present in a directory (ocaml/dune#2946, fix ocaml/dune#2927, @diml)
…lugin, dune-private-libs and dune-glob (2.3.0) CHANGES: - Improve validation and error handling of arguments to `dune init` (ocaml/dune#3103, fixes ocaml/dune#3046, @shonfeder) - `dune init exec NAME` now uses the `NAME` argument for private modules (ocaml/dune#3103, fixes ocaml/dune#3088, @shonfeder) - Avoid linear walk to detect children, this should greatly improve performance when a target has a large number of dependencies (ocaml/dune#2959, @ejgallego, @aalekseyev, @Armael) - [coq] Add `(boot)` option to `(coq.theories)` to enable bootstrap of Coq's stdlib (ocaml/dune#3096, @ejgallego) - [coq] Deprecate `public_name` field in favour of `package` (ocaml/dune#2087, @ejgallego) - Better error reporting for "data only" and "vendored" dirs. Using these with anything else than a strict subdirectory or `*` will raise an error. The previous behavior was to just do nothing (ocaml/dune#3056, fixes ocaml/dune#3019, @voodoos) - Fix bootstrap on bytecode only switches on windows or where `-j1` is set. (ocaml/dune#3112, @xclerc, @rgrinberg) - Allow `enabled_if` fields in `executable(s)` stanzas (ocaml/dune#3137, fixes ocaml/dune#1690 @voodoos) - Do not fail if `ocamldep`, `ocamlmklib`, or `ocaml` are absent. Wait for them to be used to fail (ocaml/dune#3138, @rgrinberg) - Introduce a `strict_package_deps` mode that verifies that dependencies between packages in the workspace are specified correctly. (@rgrinberg, ocaml/dune#3117) - Make sure the `@all` alias is defined when no `dune` file is present in a directory (ocaml/dune#2946, fix ocaml/dune#2927, @diml)
Would it make sense to add the
optional
/enabled_if
field to the executable stanza?The context is that in the default build of Coq, we may want to skip building some optional binaries [such as CoqIDE] if the right libraries are not present. Note that we are working on a composed build thus this seems like the simplest approach.
The text was updated successfully, but these errors were encountered: