-
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
[PROPOSAL] Env Defaults #1073
Comments
Just a small data point in favor of this proposal: I've run into the need to fall back to OCaml-syntax dune files due to a preprocessor needing different flags in different profiles (e.g. |
I don't think we should allow any field in It makes sense to put things such as compilation flags, preprocessing flags, or even list of preprocessors in env, given that some preprocessors are just used to instrument the code, but for the rest it doesn't make sense to me. |
I don't feel so strongly about libraries as I don't see the use case there either. Also, it's clear that this feature will certainly not work for all fields, so there's no harm in excluding things that we see little use in setting the default for. But what about things like enabled_if, dynlink, modes, the upcoming no_cross_module_inlining, mode? I see that being able to set all of these in one go as very useful. |
For For |
This will make it so that users cannot enable this optimization for a single library if there are other stanzas defined in the dir. Obviously this isn't a huge deal, they can just shuffle their directories around to make it work. But the fact that you have to do that, and also the fact that the user can't really gain intuition about what is customizable via env or a stanza is concerning to me. I agree that a project might overuse
Yeah, this also bothers me but we should be able to fix it once we have the better conditional syntax. In which case, the profile matching form of env won't be necessary. |
Ok, agreed. Regarding this feature in general, maybe it would help to formalize things a bit more. For instance what is a field, value etc... and then have a general notion of setting the default value of a field and a generic notion for composing fields with their default value, when it makes sense. |
A common request in Coq is to have a fast build mode which means a byte-only build. Would that be possible to implement with this proposal? |
In coq#8900 a quicker build target is requested, this PR does provide such a target for the set of files that I think make sense for developers. I think that this approach is simple and effective enough for now. Dune does indeed support a "build everything" mode that would indeed be an alternative to this PR, but we are blocked on a [planned] improvement to Dune: - profiles should support proper constraining to byte only mode. - coq_dune should be aware of the "quick" mode as to: + not generate build rules for .vo files, + use `coqtop.byte` instead of `coqtop`. The changes to `coq_dune` are trivial so we should follow the Dune issue upstream ocaml/dune#1073 and maybe move to this approach.
In conjunction of a workspace file, it would be possible. But I don't think it would be the best way to achieve your goal. Can't you just collect all the bytecode executables you need under a |
Indeed that's what we are doing now; just wondering what would the best way be. Keep in mind that Coq pervasively uses plugins so collecting And indeed, it is very common to compose the main Coq build with some 3rd party plugin, in this case the |
I see. So you'd like to rely on the plugins being present in
Yeah, that's a good point. Although note What is your workflow when working with a bytecode coq? Do you use it interactively and load some plugins? I wonder if it would make sense to bake something coq specific in a plugin to make this truly work well. |
It should be tested by whomever is depending on it right? Otherwise a non-public plugin wouldn't make a lot of sense I think.
Bytecode Coq has several uses; in this case we just want to build it as Main use of bytecode Coq these days is for debugging purposes indeed [ |
In coq#8900 a quicker build target is requested, this PR does provide targets towards that goal. - `check`, introduced in Dune 1.5.0, will build all ml files in a fast way, - `quick`, does build a set of hand-picked targets in a fast way. Further improvements could come from having `coq_dune` use `coqtop.byte` when appropriate, taking advantage from ocaml/dune#1073, and not generating rules for `.vo` files.
Well, private libraries and private executables have found their uses. This might not translate to coq however.
For this there's already the This is all unrelated to this thread, but the root of the problem seems to be defining and maintaining aliases is too troublesome for users. It's a bit similar to the issue of defining many tests that all follow the same pattern. Setting |
In coq#8900 a quicker build target is requested, this PR does provide targets towards that goal. - `check`, introduced in Dune 1.5.0, will build all ml files in a fast way, - `quick`, does build a set of hand-picked targets in a fast way. Further improvements could come from having `coq_dune` use `coqtop.byte` when appropriate, taking advantage from ocaml/dune#1073, and not generating rules for `.vo` files.
In coq#8900 a quicker build target is requested, this PR does provide targets towards that goal. - `check`, introduced in Dune 1.5.0, will build all ml files in a fast way, - `quick{byte,opt}`, does build a set of relevant hand-picked targets. Further improvements could come from having `coq_dune` use `coqtop.byte` when appropriate, taking advantage from ocaml/dune#1073, and not generating rules for `.vo` files.
In coq#8900 a quicker build target is requested, this PR does provide targets towards that goal. - `check`, introduced in Dune 1.5.0, will build all ml files in a fast way, - `quick{byte,opt}`, does build a set of relevant hand-picked targets. Further improvements could come from having `coq_dune` use `coqtop.byte` when appropriate, taking advantage from ocaml/dune#1073, and not generating rules for `.vo` files.
In coq#8900 a quicker build target is requested, this PR does provide targets towards that goal. - `check`, introduced in Dune 1.5.0, will build all ml files in a fast way, - `quick{byte,opt}`, does build a set of relevant hand-picked targets. Further improvements could come from having `coq_dune` use `coqtop.byte` when appropriate, taking advantage from ocaml/dune#1073, and not generating rules for `.vo` files.
Discussing this with the other maintainers, we find that this feature doesn't have so many use cases after all. It should not be used for preprocessors, libraries, and is really only useful for static configuration options such as:
@diml does that sound right? |
@rgrinberg maybe you could consider adding |
Flags are already definable via the env actually. We might have forgotten to generalize this to a few fields (such as jsoo), but those should be reported separately. |
In fact, we should think about how this will work for plugins. For example, we'd like the coq plugin to be able to reuse this functionality for its own flags for example. |
Ah sorry, I got confused; I was thinking of inheritance, not of I meant:
vs
|
@rgrinberg yep |
Problem
This proposal is coming out of my general annoyance of having to work harder than necessary to allow to customization of the same option at the stanza and the environment level. Clearly, both mechanisms are useful (see flags for example), and ideally this mechanism would work for pretty much every option as well:
no_dynlink
,preprocess
,modes
, etc.Solution
Allow for defining all optional fields inside inside the env stanza. For example:
To specify the defaults for a particular stanza, we can:
Where the stanza could be
test
,executable
,library
,alias
, and possibly things likebuildable
as well. We could also entertain setting defaults for multiple stanzas at once but that isn't necessary for a first version.Implementation
This is the most difficult part, and I haven't yet thought about this too much in the hopes that others might suggest productive ideas. But here are some points that I'd like to mention:
Easiest way to implement this feature would be the parse the defaults when parsing the stanzas and inserting them into the correct
~default
args. But this is also wrong and will make implementing polling mode harder.All fields that have a default value today will basically need to be options. This is unfortunate as we'll need a layer of indirection to access the values of things once the default values have been set. I wonder if we could save ourselves from this massive refactoring by parameterizing the types appropriately - by using a functor for example.
The interaction of
:standard
with the default value. Should we make it official that:standard
will henceforth refer to the current default. Perhaps it should be renamed to:default
then? (with a deprecation cycle of course).The text was updated successfully, but these errors were encountered: