Compilation failed about hydra-battles HOT 14 CLOSED

from hydra-battles.

Indeed, it looks like the first compiled file is OrdinalNotations/ON_omega.v which requires
ON_Generic. This module requires Prelude/OrdNotations.v, which is not compiled yet (on Nix/CI).
The compilation succeeds on my computer.

from hydra-battles.

This is a very strange error. For the record, here is what I have at the moment:

• In the log we can see that the failed builds are missing the COQDEP VFILES step. Then, the Coq files are built in the wrong order (with respect to the dependencies between files) which conducts to the observed error.
• I was able to reproduce the problem with the latest commit on master (5a60041) by running make within nix-shell. I couldn't reproduce the error with earlier commits and if I remove theories/gaia/T1bridge_use.v from the _CoqProject file, the error goes away. At this point, I would think this is a coq_makefile bug.
• But (!) the error has also happened on an earlier commit (566b696) before the addition of this file to _CoqProject and I am unable to reproduce the error on this commit.
• Furthermore, every time that hydra-battles-single has failed with this error, gaia-hydras (which is built with Dune) has failed as well with error Error: Unable to locate library T1. Therefore, I don't expect that restarting the failed pipelines would make them succeed, but I will try anyway.
• I will also try building with Coq 8.13 to see if that makes a difference.

from hydra-battles.

Actually, I know why the pipeline fails on commit 566b696. I see that the first attempt succeeded and it was a second attempt, triggered by @Casteran after commit 5a60041 was pushed, that failed. This is a bug in the selection of the commit to be built: it always tries the latest commit on the branch instead of the exact commit on which it is called!

I'll open an issue and try to fix this bug. But for the time being we can focus on the actual bug, which is that adding theories/gaia/T1bridge_use.v to _CoqProject has broken coq_makefile (which doesn't call coqdep anymore).

from hydra-battles.

Or that rather what looks like a coqdep bug, since we also have a problem when building gaia-hydras with Dune.

from hydra-battles.

The bug also happens with Coq 8.13.

@Casteran are you sure you don't get this bug on your computer if you run make clean first?

from hydra-battles.

from hydra-battles.

from hydra-battles.

The error moved to gaia-hydras. I test a small changes in the Requirecommands in T1Bridge_use

from hydra-battles.

The error was already there, and I would have been surprised if a change to _CoqProject had fixed it since Dune didn't use it.

from hydra-battles.

Indeed, I think that your last commit is a correct fix for Dune.

from hydra-battles.

It's all green now ! Sorry for the Mac issue !

from hydra-battles.

No worries. You helped me discover another issue related to Nix CI in passing. But something that I still find weird is that the casing issue produced this behavior (very difficult to debug).

from hydra-battles.

I've reported the coq_makefile issue on the Coq bug tracker and I've fixed the Nix CI issue in coq-community/coq-nix-toolbox#68 and #101, so I think we can close this.

from hydra-battles.