Question: how to run dune build @check without the IDE projects?

[MIvanchev]

Description of the problem

I am runnig

make dunestrap
dune build --display=short -p coq-core,coq-stdlib,coq
make check

which runs

dune build $(DUNEOPT) @check

However this results in

File "ide/coqide/dune", line 35, characters 54-74:
35 |  (libraries coqide-server.protocol coqide-server.core lablgtk3-sourceview3 platform_specific))
                                                           ^^^^^^^^^^^^^^^^^^^^
Error: Library "lablgtk3-sourceview3" not found.
-> required by library "coqide_gui" in _build/default/ide/coqide
-> required by _build/default/ide/coqide/coqide_os_stubs.o
-> required by alias ide/coqide/check

how do I exclude the IDE from the checks?

Coq Version

8.19

[SkySkimmer]

You can't, but is @check really what you want? It's for running ocaml typechecking on all ocaml files, typically to get faster errors than a full build while developing. Meanwhile build -p is the optimized build.

Coq Version
18.9

I don't know that version.

[MIvanchev]

You can't, but is @check really what you want? It's for running ocaml typechecking on all ocaml files, typically to get faster errors than a full build while developing. Meanwhile build -p is the optimized build.

Coq Version
18.9

I don't know that version.

It's 8.19 sorry. Otherwise thanks, I don't know if it's what I want, I'm just trying to follow the standard build process. Maybe I'll skip it.

[ejgallego]

The command you want is:

rm ide/coqide/dune

It'd be good to have a better way to do this, but dune build @check doesn't respect --packages-only=. Bug in dune.

[SkySkimmer]

We don't know if that's what he wants. "follow the standard build process" is too unspecific to deduce anything.

[MIvanchev]

Hello!

It'd be good to have a better way to do this, but dune build @check doesn't respect --packages-only=. Bug in dune.

Sadly I found this out the hard way. My current solution is to patch out everything related to coqide but will try rm ide/coqide/dune once I get everything else to build. Thanks @ejgallego!

We don't know if that's what he wants. "follow the standard build process" is too unspecific to deduce anything.

Void Linux has a process for releasing new packages and it includes a check phase which I don't want to skip unless there is a very good reason. If Coq runs the checks with a small patch I'll rather go this way than no checks at all. Anyhow I think I got it to build AND check and I'm very grateful!!!

[SkySkimmer]

You are assuming that what void linux calls check and what dune / our makefile calls check is the same thing. I think it's more likely that what void linux calls check is what we call test suite.

[ejgallego]

Indeed @SkySkimmer is correct, you don't want to run make check on a packaging setup, usually the check step in your case would be running the Coq's test-suite.

The @check Dune target is meant for developing Coq, and indeed, it does some special rule setup to try to give very fast feedback about problems to editors.

In the context @check is used, it doesn't make a lot of sense to skip the compilation of optional libraries, as developers need to submit patches to work with these anyways.

[MIvanchev]

OK, that's a good insight, so how do I run the test suite?

[ejgallego]

make -C test-suite should do the trick, I recommend you also build coqide-server package, but you can disable these tests by removing ide from the SUBSYSTEMS variable in test-suite/Makefile

[MIvanchev]

Thank you so much @ejgallego, that's exactly what I'll be going for + coqide as a sub-package :)