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

Last updated: Feb 06 2023 at 00:03 UTC