You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Let's check that we can build, test and format cleanly in a pre-commit hook.
If you want to ignore warnings when developing, we should add a make target/flag that passes the --profile release option to dune.
https://github.com/CuiCui66:
I'm more in favor of leaving the default profile dev without warnings, and then create a --profile commit that is called by the pre-commit hook and that has the warning as error thing. This is for multiple reasons:
The compiling command you call the most of time (and by hand) is the one you use when you developing new code/experimenting, So it's good if that's the default (and the profile is named dev).
The --profile release is not intended at all for removing warnings but for releasing (as the name indicate) and therefore has (or will have) more release related effect like not passing the -g option, disabling assertions, compiling with -O3 on the flambda compiler, ...
And then the pre-commit hook can call dune with --profile commit
And last but not least, I'm not sure this should be done at the commit level. I often do commits with name "WIP" and random code that do not even compile, then I erase/squash them and make a clean commit to send upstream, so this should probably be at PR level (Checking that the code builds without warning, tests and formats properly)
The text was updated successfully, but these errors were encountered:
Let's check that we can build, test and format cleanly in a pre-commit hook.
If you want to ignore warnings when developing, we should add a make target/flag that passes the
--profile release
option to dune.https://github.com/CuiCui66:
I'm more in favor of leaving the default profile
dev
without warnings, and then create a--profile commit
that is called by the pre-commit hook and that has the warning as error thing. This is for multiple reasons:dev
).--profile release
is not intended at all for removing warnings but for releasing (as the name indicate) and therefore has (or will have) more release related effect like not passing the-g
option, disabling assertions, compiling with-O3
on the flambda compiler, ...What I suggest is something like:
And then the pre-commit hook can call dune with
--profile commit
And last but not least, I'm not sure this should be done at the commit level. I often do commits with name "WIP" and random code that do not even compile, then I erase/squash them and make a clean commit to send upstream, so this should probably be at PR level (Checking that the code builds without warning, tests and formats properly)
The text was updated successfully, but these errors were encountered: