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

Please add signals_are_pending to compatibility.h #7883

Closed
vicuna opened this Issue Dec 21, 2018 · 5 comments

Comments

Projects
None yet
1 participant
@vicuna
Copy link
Collaborator

vicuna commented Dec 21, 2018

Original bug ID: 7883
Reporter: SkySkimmer
Assigned to: @jhjourdan
Status: resolved (set by @jhjourdan on 2019-02-02T10:24:03Z)
Resolution: fixed
Priority: normal
Severity: minor
Fixed in version: 4.08.0+dev/beta1/beta2
Category: runtime system and C interface
Monitored by: @nojb

Bug description

signals_are_pending got renamed to signals_might_be_pending in 1c82c48 (4.08)
A compatibility #define should be added to compatibility.h

Context: we use it in Coq (https://github.com/coq/coq/blob/d501e6f301f1c023e57f14ee3441553c530d9394/kernel/byterun/coq_interp.c#L429)

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Dec 21, 2018

Comment author: @gasche

A change is in discussion, see

#2104 (comment)

of course, it is arguably a bad idea for Coq to be relying on private internals of the OCaml runtime, and it would be more future-proof to reimplement your own signal-handling logic (possibly asking Jacques-Henri for help?).

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Dec 21, 2018

Comment author: @jhjourdan

Frankly, I thought a bit about that, and I am not sure what's best: on the one side, Coq has to hijack OCaml's internal mechanisms, but on the other side, it is rather hard to design a signal handling mechanism in C which properly handles all signals and interferes properly with OCaml's mechanism.

Note that Coq already greatly hijack's OCaml's internals in order to have an efficient implementation of te VM...

Perhaps the actual "proper" answer to this issue is to provide a /public/ #define macro in OCaml header which one can call periodically to handle signals.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Dec 21, 2018

Comment author: @jhjourdan

See #2211 for the proposed fix.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Dec 21, 2018

Comment author: @ejgallego

We could also use #ifdef in Coq + <caml/version.h> to workaround that as we are talking about C code.

IMVHO, Coq's VM should not rely on this in the medium-long term. Instead, we must redesign the way signals are handled in Coq so low-level components don't have to care so much.

For example, another problematic point are UIs / coqtop / XML protocol dying on Ctrl-C.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Feb 2, 2019

Comment author: @jhjourdan

The patch in question has been reverted, and its replacement does no longer have this problem.

@vicuna vicuna closed this Feb 2, 2019

@vicuna vicuna added stdlib bug labels Mar 14, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.