Stream: Coq devs & plugin devs

Topic: coqdep anomaly on trivial error

view this post on Zulip Karl Palmskog (May 09 2022 at 09:12):

Here is coqdep on 8.15.1:

$ coqdep foo
No such file or directory

And here is coqdep on master:

coqdep foo
*** Error: Anomaly
           "Uncaught exception Coqdeplib.Common.Cannot_stat_file("foo", 20)."
           Please report at http://coq.inria.fr/bugs/.

Is this really a reasonable output? You may get a lot of bug reports this way.

view this post on Zulip Enrico Tassi (May 09 2022 at 09:16):

maybe an oversight of https://github.com/coq/coq/pull/15953

view this post on Zulip Enrico Tassi (May 09 2022 at 09:17):

@Ali Caglayan

view this post on Zulip Ali Caglayan (May 09 2022 at 09:23):

Thanks for the report, I'll work on a patch today.

view this post on Zulip Ali Caglayan (May 09 2022 at 10:18):

https://github.com/coq/coq/pull/16003

Last updated: Sep 09 2024 at 06:02 UTC