Jason Gross (May 02 2021 at 21:24): 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
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?
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.
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
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
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.
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"
Emilio Jesús Gallego Arias (May 03 2021 at 00:40):For native_compute , indeed proper finalizaton on async exceptions should fix this
Emilio Jesús Gallego Arias (May 03 2021 at 00:40):[I hope]
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.
Paolo Giarrusso (May 03 2021 at 08:59):But coqc must still _fail_ with a non-0 exit code to trigger that.
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.
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 ...)
Emilio Jesús Gallego Arias (May 04 2021 at 00:00):I'd swear @Jason Gross there is already a bug open for that.
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: Apr 18 2024 at 11:02 UTC