-
Notifications
You must be signed in to change notification settings - Fork 415
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
Stricter hygiene by default? #1882
Comments
We should wait for a major release to change this warning into an error by default, though in the meantime we can add an option in the dune-project file to make it an error right now. Alternatively, we could also make it an error when using Thoughts? |
Any of the two choices would be great for us; maybe the main question is: even today, does this use case makes sense? Is there anyone relying on picking targets from the source tree for their project to build OK? |
Originally the rule was silently ignored. i.e. |
I see, other kind of files may indeed be a problem [I was somehow only worried about ML object files] I guess the warning has been there long enough but without testing it is hard to tell. Thus in principle an option could be better, on the other hand that would introduce "option creep", I dunno. |
I suggest that we make it an error from version 1.8 of the dune language then: we get the better behavior in newer projects and we don't introduce a new option. It is technically a breaking change in the language which means that upgrading from |
Yup, it seems not pain-free but on the other hand would any project be affected it pretty easy to add the missing |
Indeed, do you want to take a stab at implementing this? Something like |
I'll be happy to take care of this when my "working on Dune" slot comes, in practice that means in two weeks due to other deadlines so if someone feels like doing it before please do so! |
@ejgallego fixing this doesn't seem like a priority, so we're happy to let you tackle it. Will assign you. |
I ended up doing that in #2068 |
Thanks for the update @diml, this was not far from the top of my todo list, sorry I didn't get to do it sooner. |
No problem, it was quite natural to do as part of the other changes |
Fixed by #2068 then. |
The nº 1 problem developers migrating to Dune face in Coq is one of having a dirty build tree:
IMHO this warning is very confusing and is making new dune users lose a lot of time at first.
Should the warning be finally be made an error, and the message changed to something such as "your source tree is dirty, this is an error. Please remove any object files from it and try again".
[^^ the current wording is super bad I know, but you get the idea]
The text was updated successfully, but these errors were encountered: