Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

native_compute makes coqc uninterruptible #11101

Open
JasonGross opened this issue Nov 12, 2019 · 0 comments
Open

native_compute makes coqc uninterruptible #11101

JasonGross opened this issue Nov 12, 2019 · 0 comments

Comments

@JasonGross
Copy link
Member

JasonGross commented Nov 12, 2019

Description of the problem

If I have an invocation of native_compute which results in a call to ocamlopt that takes many seconds or minutes, coqc seems to ignore ctrl+c during that time. It should not.

(It's possible that this is a mis-report, and there's some other interaction with make going on causing lack of interrupt. If you can't reproduce this even with very long-running compilations on native_compute calls, feel free to resolve as invalid or worksforme or whatever.)

Coq Version

8.10

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant