Skip to content
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

Remove rename_targets() #946

Closed
3 tasks done
wlandau opened this issue Jul 17, 2019 · 0 comments
Closed
3 tasks done

Remove rename_targets() #946

wlandau opened this issue Jul 17, 2019 · 0 comments

Comments

@wlandau
Copy link
Member

wlandau commented Jul 17, 2019

Prework

Description

Unfortunately, we cannot (at least, we should not) rename targets. We need to remove rename_targets() from drake.

Each target comes with its own random number generator seed, which is determined by the global seed (seed argument of make()) and the target name. There is simply no other way to generate a different reproducible RNG seed for each target. By renaming a target, we are changing the seed the target was supposed to have, which invalidates the value in the cache.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant