chore: move Tests.v to test/ folder

[Alizter]

These won't be built when doing dune build and can be very noisy. Instead these will be built when doing dune test which we do in the CI. The opam jobs should catch any failing tests. The makefile will build all of them.

We further improve performance by splitting the tests file into multiple separate files.

We also add a README detailing some conventions we can use on tests.

@jdchristensen This also makes the main build silent.

[jdchristensen]

This is great. Is there a way to run the tests with make as well? If so, the instructions should be added to the README.md.

Separately, I think we should also link to this README.md from STYLE.md.

[Alizter]

@jdchristensen I've updated our _CoqProject script to also include the tests, I don't see an easy way to split these up currently. This means that they will always be run with make. Not worse than before however.

I've also updated the STYLE.md file to point to test/README.md.

[Alizter]

I've annotated (oo)ExtendableAlong_Over and made sure that dune build avoids test/.

[jdchristensen]

LGTM

[jdchristensen]

It seems like `dune build' doesn't work from a subfolder anymore. I'm pretty sure it used to work, right?

[Alizter]

Which folder are you trying it from? It appears to work for me. If you are trying it in test/ it will not work, you will need to use dune test. If it is a folder that is not contrib or test then you will need to add it to the alias stanza in the dune file of the project root. That's where I am overriding @default to mean everything but tests.

[jdchristensen]

If I try it within the WildCat folder, it doesn't build anything, but gives no errors.

[jdchristensen]

It works within the theories folder, or one up from that.

[Alizter]

That's very strange, are you sure it isn't building anything? One way you can test this is by doing dune clean and then dune build --cache disabled within your Wildcat folder. You can inspect the build in _build/default/theories/Wildcat checking for vo.

Also which version of Dune are you using?

I am using 3.10 and I can build everything like you describe just fine.

Also if you paste the _build/log here for the build that did nothing, we can inspect what is going on.

[jdchristensen]

Oh, I see what is happening. If I run dune build within the WildCat folder, it only tries to build things in that folder. Is that how it is supposed to be? (I'm using 3.10 too.)

[Alizter]

@jdchristensen Yes that's what it is supposed to do. You can build outside the folder with dune build ../...

[jdchristensen]

Thanks. Is dune also supposed to rebuild the emacs TAGS file? (Sorry to clutter this PR...)

[Alizter]

@jdchristensen I did not add such a rule, but I can add one if you would like.

[jdchristensen]

@Alizter That would be great!

[Alizter]

If you want a continuous build with the new tags rule #1754 you can do something like dune build @default TAGS -w which will build the @default alias (in dune aliases are like sets of targets) together with the new TAGS target, all in -w watch mode. In watch mode the build will restart as soon as there are source changed.

[jdchristensen]

That's where I am overriding @default to mean everything but tests.

It seems like @default does include the tests:

$ dune build @default --display=short
      coqdep theories/.HoTT.theory.d    
        coqc theories/Idempotents.{glob,vo}
        coqc test/Idempotents.{glob,vo}
...

But just dune build --display=short doesn't build them. I'm asking about this because I'd like to build the TAGS and everything else except the tests, but dune build @default TAGS also builds the tests.

[Alizter]

@jdchristensen Ah thats my miatake. TAGS is pulling in the tests too. I can fix that tomorrow. If you want to fix it, replace the deps field of that TAGS rule with two (glob_files_rec) for theories and contrib only rather than all vo diles starting from the root.

[Alizter]

@jdchristensen Actually that had nothing to do with it. The reason is as follows: @default is a recursive alias meaning that it is really every default alias in each subdirectory. When we run dune build we are actually doing dune build @@default which is the non-recursive kind, doing the default alias only in the current directory. Perhaps a better way to write the command I mentioned above would be the following:

dune build theories/ contrib/ TAGS -w

That is clearer to understand and you don't need to know about aliases. You can read this as: Build all the targets in theories/, contrib/ and the target TAGS all in watch mode.