Stream: Coq devs & plugin devs

Topic: C-c on Eval native_compute in


view this post on Zulip Jason Gross (May 02 2021 at 21:24):

Is interrupting the native-compiler known-unsafe? I've managed to get coqtop into a state where Eval native_compute in foo gives

Error: This expression has type
         Nativevalues.t -> Nativevalues.t -> Nativevalues.t
       but an expression was expected of type 'a Lazy.t = 'a lazy_t
Finished failing transaction in 0.044 secs (0.007u,0.009s) (failure)
Error: Native compiler exited with status 2

view this post on Zulip Jason Gross (May 02 2021 at 21:26):

Actually, I get this error message in coqc too:

File "/tmp/Coq_native541a2e/Coq_native9525a6.native", line 149, characters 68-144:
149 |                                                                     NCrypto_Util_Strings_Show.const_NCrypto_Util_Strings_Show_PowersOfTwo_show_Z
                                                                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type
         Nativevalues.t -> Nativevalues.t -> Nativevalues.t
       but an expression was expected of type 'a Lazy.t = 'a lazy_t
Finished failing transaction in 0.05 secs (0.019u,0.s) (failure)
File "./src/UnsaturatedSolinasHeuristics/Tests.v", line 153, characters 0-1718:
Error: Native compiler exited with status 2

Is this likely to be a bug in Coq? Or just a transient issue with my build outputs?

view this post on Zulip Emilio Jesús Gallego Arias (May 02 2021 at 23:12):

@Jason Gross this is very related to the discussion we had in the Coq Call about async exceptions and how the current codebase is not structured to handle these properly due to lack of control for OCaml side-effects; IMHO the above issue is worth a bug report, but in general we have quite a bit of work ahead to improve the codebase on that.

view this post on Zulip Emilio Jesús Gallego Arias (May 02 2021 at 23:13):

There are many design patterns to help improve this, for example to require functions that need clenaup when interrupted to expose a finalizer interface

view this post on Zulip Emilio Jesús Gallego Arias (May 02 2021 at 23:14):

That being said, the concrete error you get could be due to some mismatch along the toolchain

view this post on Zulip Jason Gross (May 03 2021 at 00:20):

That being said, the concrete error you get could be due to some mismatch along the toolchain

I believe it only showed up after C-c during native_compute. Furthermore, the native_compute succeeded, which suggests to me that there's some failure to propagate errors from native compilation. (There's a similar issue in coq_makefile, where having native compilation fail with a stack overflow does not result in the .vo file being deleted, and so the build results get out of sync.) Doing find . -name ".coq-native" | xargs rm -rf fixed the issue.

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 00:39):

Interesting. For coq_makefile and native I'm afraid there are quite a few bugs [similar that the ones we used to have in the OCaml build] regarding to stale targets, this is TTOMK beyond make's capabilities and a reason to switch to systems with a more precise "target model"

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 00:40):

For native_compute , indeed proper finalizaton on async exceptions should fix this

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 00:40):

[I hope]

view this post on Zulip Paolo Giarrusso (May 03 2021 at 08:56):

To ask make to delete targets when commands fail, one should add the following (based on https://www.gnu.org/software/make/manual/html_node/Special-Targets.html);

.DELETE_ON_ERROR:

make's manual suggests _all_ Makefiles should use this; it's not a default for backward compatibility.

view this post on Zulip Paolo Giarrusso (May 03 2021 at 08:59):

But coqc must still _fail_ with a non-0 exit code to trigger that.

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 13:40):

This indeed can help, but note https://github.com/coq/coq/issues/13035 will still mean the solution is not complete for certain files.

view this post on Zulip Jason Gross (May 03 2021 at 20:17):

Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]

Why is this a warning? Why does it matter if my identifiers contain __? Can't they just be renamed? (This is particularly silly when I have let __ := ... in ...)

view this post on Zulip Emilio Jesús Gallego Arias (May 04 2021 at 00:00):

I'd swear @Jason Gross there is already a bug open for that.

view this post on Zulip Jason Gross (May 04 2021 at 00:16):

Ah, indeed, I reported this 4 years ago: https://github.com/coq/coq/issues/5397


Last updated: Oct 21 2021 at 21:03 UTC