Use ppx_inline_test for unit tests

[ineol]

As suggested by @ejgallego in #613, use inline tests instead of alcotest.

[ejgallego]

Amazing, thanks so much!

Nix CI seems to need a tweak, I'll have a look later, but please feel free to merge yourself if you find a solution first.

[Alizter]

Nix is easy, just replace the alcotest in flake.nix with ppx_inline_test.

[ejgallego]

Nix is easy, just replace the alcotest in flake.nix with ppx_inline_test.

The PR seems to do that already, that's why I'm confused actually.

[Alizter]

Need to add it here too

coq-lsp/flake.nix

Line 69 in 008c6c2

inherit (ocamlPackages) yojson cmdliner uri dune-build-info;

It was only added to the devShell but you have to add it to the actual package that gets built too.

[ejgallego]

I see, we are not running the tests on Nix, that's why the previous PR worked.

[Alizter]

This adds the test library as a dependency to the executable, which is probably not what you want. I think it would be better to have a separate test library like before.

[ejgallego]

Does it? I think dune handles this properly.

[Alizter]

We shouldn't be adding test libraries as build dependencies anyhow. They should live in a separate library as they currently do with alcotest.

[ejgallego]

We shouldn't be adding test libraries as build dependencies anyhow. They should live in a separate library as they currently do with alcotest.

Why? The whole idea of inline tests is to have the code next to the libraries, it is true that some people use a policy of splitting test libs , but so far this is a matter of taste.

Myself I'm fine with the tests living next to the use.

See official dune docs https://dune.readthedocs.io/en/stable/tests.html#inline-tests

[Alizter]

@ejgallego Yes, but you are adding another build dependency just so you are aware.

[ejgallego]

@ejgallego Yes, but you are adding another build dependency just so you are aware.

Yes; as it was the way it was done, I suggest we keep it this way.

But indeed if we find a problem with the new setup, we can just do a follow-up PR and split the tests to their own file.

I like (it's a personal preference, of course) when tests (and proofs) are near their corresponding definitions.

But indeed, an extra dep is a non trivial cost to pay.