Here are some adjustments to Dune builds to follow best practices. I also added tests corresponding to test-plugin and test-tactics. Regular Make builds are untouched.
Note that Dune does not allow running tests separately unless the files are located in different directories (unlike tests/tactics_test.v and tests/plugin_test.v). So maybe the tests directory could be partitioned into tests/tactics and tests/plugin? I can add this to the PR if such a change would be welcome.
Here are some adjustments to Dune builds to follow best practices. I also added tests corresponding to
test-plugin
andtest-tactics
. Regular Make builds are untouched.Note that Dune does not allow running tests separately unless the files are located in different directories (unlike
tests/tactics_test.v
andtests/plugin_test.v
). So maybe thetests
directory could be partitioned intotests/tactics
andtests/plugin
? I can add this to the PR if such a change would be welcome.