Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007883OCamlruntime system and C interfacepublic2018-12-21 13:522019-02-02 11:24
ReporterSkySkimmer 
Assigned Tojacques-henri.jourdan 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.08.0+dev/beta1 
Summary0007883: Please add signals_are_pending to compatibility.h
Descriptionsignals_are_pending got renamed to signals_might_be_pending in https://github.com/ocaml/ocaml/commit/1c82c481a5b33987e05012be61893c03f59ef361 [^] (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 [^])
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0019513)
gasche (administrator)
2018-12-21 16:41

A change is in discussion, see

  https://github.com/ocaml/ocaml/pull/2104#issuecomment-449395279 [^]

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?).
(0019516)
jacques-henri.jourdan (manager)
2018-12-21 23:10

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.
(0019517)
jacques-henri.jourdan (manager)
2018-12-21 23:11

See https://github.com/ocaml/ocaml/pull/2211 [^] for the proposed fix.
(0019518)
ejgallego (reporter)
2018-12-22 00:30

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.
(0019576)
jacques-henri.jourdan (manager)
2019-02-02 11:22

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

- Issue History
Date Modified Username Field Change
2018-12-21 13:52 SkySkimmer New Issue
2018-12-21 16:41 gasche Note Added: 0019513
2018-12-21 16:41 gasche Assigned To => jacques-henri.jourdan
2018-12-21 16:41 gasche Status new => assigned
2018-12-21 23:10 jacques-henri.jourdan Note Added: 0019516
2018-12-21 23:11 jacques-henri.jourdan Note Added: 0019517
2018-12-22 00:30 ejgallego Note Added: 0019518
2019-02-02 11:22 jacques-henri.jourdan Note Added: 0019576
2019-02-02 11:24 jacques-henri.jourdan Status assigned => resolved
2019-02-02 11:24 jacques-henri.jourdan Fixed in Version => 4.08.0+dev/beta1
2019-02-02 11:24 jacques-henri.jourdan Resolution open => fixed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker