Stream: Coq devs & plugin devs

Topic: itauto broken


view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 13:04):

due to parallel pr merge
I'll make the fix
EDIT upstream independently made a fix for the Tacticals.New change

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 13:34):

actually something looks deeply messed up in the build system
https://gitlab.com/coq/coq/-/jobs/1783077180

COQC theories/PatriciaR.v
COQC theories/PatriciaR.v
File "./theories/PatriciaR.v", line 4338, characters 0-44:
Warning: Removed file ./theories/PatriciaR.vo
Error: Anomaly "Uncaught exception End_of_file."
Please report at http://coq.inria.fr/bugs/.

view this post on Zulip Karl Palmskog (Nov 15 2021 at 13:35):

hmm, could that be related to the use of multiple _CoqProject-like files?

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 13:35):

also it seems itauto has no CI
perhaps it should be removed from coq's CI until that's changed

view this post on Zulip Gaëtan Gilbert (Mar 16 2023 at 11:43):

eg https://gitlab.com/coq/coq/-/jobs/3940699733
it seems to be due to the switch to dune (https://gitlab.inria.fr/fbesson/itauto/-/commit/ad31f305f281d89b7a9cf5f809062bd7ffd6e445)
What would be a correct fix for this?
cc @Emilio Jesús Gallego Arias

view this post on Zulip Karl Palmskog (Mar 16 2023 at 11:46):

have you opened an issue in the repo? We can also ping Frédéric here.

view this post on Zulip Gaëtan Gilbert (Mar 16 2023 at 11:50):

I pinged him in private messages to avoid subscribing him to the stream

view this post on Zulip Frédéric Besson (Mar 16 2023 at 14:13):

I have rerun my Coq CI, it runs... https://gitlab.inria.fr/fbesson/itauto/-/jobs/2957313
Am I doing something wrong?

view this post on Zulip Gaëtan Gilbert (Mar 16 2023 at 14:14):

it's specifically when used in coq CI, something about being built in a subdirectory of a project that also uses dune I guess

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2023 at 14:28):

It is because dune build will detect the workspace root as the Coq folder.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2023 at 14:29):

Unfortunately this is not very well structured in Dune, best solution is to never vendor, so indeed your testing workspace containts a checkout of every project and no submodules

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2023 at 14:30):

In Coq we should actually set DUNE_ROOT= to the right root before calling sub-scripts in CI

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2023 at 14:30):

however I'm not sure Dune offers such a variable

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2023 at 14:30):

The fix we have in other projects is to use --root . , but that's a PITA for other reasons

view this post on Zulip Frédéric Besson (Mar 16 2023 at 15:05):

So a fix would be dune build --root . ?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2023 at 15:06):

Yes, --root . or the corresponding path where the main root is located

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2023 at 15:06):

but indeed we should change our CI layout

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2023 at 15:10):

You could actually improve the workflow a bit, as you are interested in having the binary in the source folder, you can do dune build --root . mlpatch, and add a promotion rule so dune will copy it from the build directory, that way you don't have to guess these kind of _build/default/patch/foo.exe

view this post on Zulip Frédéric Besson (Mar 16 2023 at 17:30):

Thanks. This should be fixed by https://gitlab.inria.fr/fbesson/itauto/-/commit/ce158859ce74c49b0c7a668582ca9b00e8403d6f

view this post on Zulip Gaëtan Gilbert (Mar 17 2023 at 12:53):

to those who notice that it still fails, cf https://github.com/coq/coq/pull/17399

view this post on Zulip Frédéric Besson (Mar 17 2023 at 14:14):

I had no reason to not use dune 2.9
https://gitlab.inria.fr/fbesson/itauto/-/commit/a5a6f8e9887f40d526c087d72b56e094622aab2f should solve the issue.

view this post on Zulip Karl Palmskog (Mar 17 2023 at 14:35):

@Frédéric Besson but the Dune 2.9 thing would have been fixed by the PR of @Gaëtan Gilbert I believe... Can't the Dune 3.6 features be kept?

view this post on Zulip Karl Palmskog (Mar 17 2023 at 14:35):

my understanding is that flambda CI of Coq uses Dune 3.6

view this post on Zulip Frédéric Besson (Mar 17 2023 at 16:08):

I did not pay attention to the dune number. I see no reason to require 3.6 if 2.9 is enough. And this does not prevent anyone from using dune 3.6 if they wish. Or am I missing something, again?

view this post on Zulip Karl Palmskog (Mar 17 2023 at 16:08):

OK, so you were not using any specific features from Dune 3.6?

view this post on Zulip Karl Palmskog (Mar 17 2023 at 16:09):

I was reading https://gitlab.inria.fr/fbesson/itauto/-/commit/a5a6f8e9887f40d526c087d72b56e094622aab2f and thinking something had changed w.r.t. testing of mathcomp-ssreflect

view this post on Zulip Karl Palmskog (Mar 17 2023 at 16:11):

(in addition, if I remember correctly the opam build property should not be used for dune, i.e., I think the convention is to use simply "dune" {>= "2.9"})

view this post on Zulip Gaëtan Gilbert (Jun 05 2023 at 07:20):

https://gitlab.inria.fr/fbesson/itauto/-/merge_requests/11 got merged early so it will be broken in CI until https://github.com/coq/coq/pull/17664 is merged (it still needs a coqhammer overlay, I'll do it later today)


Last updated: May 24 2024 at 23:01 UTC