coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] set_timeout in 8.8.0

From: Gabriel Scherer <gabriel.scherer AT gmail.com>
To: Łukasz Czajka <lukaszcz AT mimuw.edu.pl>
Cc: Coq Club <coq-club AT inria.fr>, Burak Ekici <ekcburak AT hotmail.com>
Subject: Re: [Coq-Club] set_timeout in 8.8.0
Date: Wed, 9 May 2018 16:25:32 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gabriel.scherer AT gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f174.google.com
Ironport-phdr: 9a23:h1CMehNMqBZ53mqlqAYl6mtUPXoX/o7sNwtQ0KIMzox0LfX5rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiCcfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZXMlRWSxPDI2/YYUSEeQOIf1VoJPhq1YUtxayGRWgCeHpxzRVhnH2x6o60+E5HA/HxgMvBMgOsHXKo9XxKawcTPy6zKnWwjXZcfxWwyr25Y/Hch87uv6MR7NwftTVyUU1DAPKklWQppL/PzyLzOQAqGeb7+96WuKuj24rsR1+oj+qxso1jITCm4Ebykjc+Cln3Io4Ice0RU17bNK+DpdcqiCXO5FrTs4gTGxlvjsxxKcctp6hZicKzYwqxx7BZPyDdIiF+hfjW/yQITd8nX5lYa6/iwqr/Uiu1+HxVMa53ExFripCldnMuXQN2ALJ5sebTft9+1+t2TeJ1w/N9uFJOV44mbbfJpI7wbM9loAfvVreEiL3gkn6ka2be0o89uit8evnY7HmppGGN49zjwHzKqsuldakDuQiMwgBQWyb9f6n1LL//U32Xq9KgeMskqTCv5DaIN4Upq+9AwNPzokj7BO/Ay+80NsEhXkHME5FeBWfgof1PFHOOen0Auu7g1Sxizhm3OvGP73kApXVNHfPirbhfbBn605d0gU/195f54gHQo0GddbuWUbqpuvzHBY7MAX8l+L6C9xmxIgMcWeOB7KGdq7erBmQ4rR8DfOLYdo6sTznKvUhr8XljXIjlEVVKaag14EWZXT+Bf9mLl+Ue1Ljh94AFSEBuQ9oH7+is0GLTTMGPyX6ZKk7/DxuTdv+Vd6SFLDou6SI2WKAJrMTY2lHDl6WFnKxLteLXv4NbGSZJcozy2VYB4jkcJco0FSVjCG/06Bud7OG9SgRtJal399wtbWKyEMCsAdsBsHY6FmjCmF5mmRSGW0z1aF75FVhkhKNiPckxfNfEtNX6rVCVQJobZM=

Contrarily to what I believed, there seems to be a bug in the OCaml runtime (MPR#7709, reported on the OCaml bugtracker by Jacques-Henri) that affects the Coq-side implement of the runtime function. Apologies for the incorrect remarks above -- and thanks to all for the extra precisions and references.

On Mon, May 7, 2018 at 1:17 PM, Łukasz Czajka <lukaszcz AT mimuw.edu.pl> wrote:

>> It seems generally well-known¹ that, following POSIX, "alarm" is process-level
>> and may deliver the SIGALRM signal to any thread² that does not
>> explicity block it -- I don't think the OCaml runtime is supposed to
>> give any stronger guarantees than POSIX on these system calls.
>>

Yes, from the pages you link to it seems that indeed OCaml runtime
behaves as it's supposed to here. So it seems it's a bug in Coq after
all. But there is a bug somewhere, because the timeout tactical does
not behave according to its specification.

[Coq-Club] set_timeout in 8.8.0, Burak Ekici, 05/02/2018
- Re: [Coq-Club] set_timeout in 8.8.0, Emilio Jesús Gallego Arias, 05/02/2018
  - Re: [Coq-Club] set_timeout in 8.8.0, Łukasz Czajka, 05/03/2018
    - Re: [Coq-Club] set_timeout in 8.8.0, Gabriel Scherer, 05/07/2018
      - Re: [Coq-Club] set_timeout in 8.8.0, Łukasz Czajka, 05/07/2018
        
        Re: [Coq-Club] set_timeout in 8.8.0, Łukasz Czajka, 05/07/2018
        
        Re: [Coq-Club] set_timeout in 8.8.0, Gabriel Scherer, 05/09/2018
        
        Re: [Coq-Club] set_timeout in 8.8.0, Xavier Leroy, 05/10/2018
        
        Re: [Coq-Club] set_timeout in 8.8.0, Tej Chajed, 05/07/2018
        
        Re: [Coq-Club] set_timeout in 8.8.0, Łukasz Czajka, 05/07/2018
      - Re: [Coq-Club] set_timeout in 8.8.0, Jacques-Henri Jourdan, 05/07/2018