search

coq-community / coq-ext-lib

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
https://coq-community.org/coq-ext-lib/
BSD 2-Clause "Simplified" License
129 stars 46 forks source link

Use replace instead of cutrewrite. #101

Closed Zimmi48 closed 4 years ago

Zimmi48 commented 4 years ago

Compatibility with coq/coq#12993.

Zimmi48 commented 4 years ago

The 8.12 test failed during the coqdoc build step with:

File "./theories/Data/Option.v", line 183, characters 0-34:
Warning: Removed file ./theories/Data/Option.vo
Error: Anomaly "Uncaught exception End_of_file."
Please report at http://coq.inria.fr/bugs/.

File "./theories/Data/Option.v", line 183, characters 0-34:
Warning: Removed file ./theories/Data/Option.vo
Error: System error: "./theories/Data/Option.vo: No such file or directory"

@liyishuai Have you seen this before?

Zimmi48 commented 4 years ago

Ah, we restarted it at the same time it seems.

Zimmi48 commented 4 years ago

The second run also led to the non-deterministic failure. Maybe the third will be the good one?

BTW is this something that should be reported as an issue to Coq?

Zimmi48 commented 4 years ago

Nope. I've tried a fourth time.

Zimmi48 commented 4 years ago

OK this time it looks like it is going to pass.

liyishuai commented 4 years ago

Found a similar issue with Coqdoc: https://sympa.inria.fr/sympa/arc/coq-club/2014-03/msg00039.html Not sure if parallel compilation caused this failure.

Zimmi48 commented 4 years ago

OK, if that's the same error, it doesn't look very new. I was worried to see it happen 3 times in a row but on 8.12 only that this could be some problem that would have been introduced recently. Anyway, that might still be worth to report if you wish.