coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] set_timeout in 8.8.0

From: Łukasz Czajka <lukaszcz AT mimuw.edu.pl>
To: Gabriel Scherer <gabriel.scherer AT gmail.com>
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: Mon, 7 May 2018 13:17:53 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lukaszczz AT gmail.com; spf=Pass smtp.mailfrom=lukaszczz AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f176.google.com
Ironport-phdr: 9a23:4FNsdRawsS8605DACJlfZnz/LSx+4OfEezUN459isYplN5qZoMu6bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58axlVAHnhzsGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7WYNEUSndbXstJVSNBDIOyYYUMAeQcI+hXs4bzqkASrRunHwSgGP/jxiNKi3LwwKY00/4hEQbD3AE4GdwOrXfUo8/uNKYTSe+40qjJwi/Bb/NVwzj29Y/FchQ8ofGPR71wasvQxlUuFg7ei1WQqInlPy6b1+gXrWeU8vdgWfi3i24jsgx8pCWkyMQ0ioTRmI4Z1lTJ+T96zYs1P9G0VlB3bNC+HJdNtSyXNo17Sd44TW5yoiY10LgGtIa7fCcUzJQnwAbSa/mdfIiJ5hLvTeeRITBkiH58drKzmhS//Em6xu3zUcm011lKri5bndXWqn8N0BnT5tCGSvt74EihxS6C2x7P5uxAO0w5lqrWJ4Q/zrIumJcfq1nPEy33lUnuia+ZbEQk+uym6+T9ZbXmo4eRN4tpigH9KKsugc2+Dvg5MwkPRGWb9uG826fi/U39WrlFkvo2kqzBvJDAOcsbvrK5AxNS0os79xm/CC6m3M0EknkDMVJKYwmKj5PpOlHLOPD3F+2zg1WqkDdxxvDJJKftApvXLiuLrLC0Ur938U9RzEIIxtBS/Z9OQuUOKfjpW0L18sfTDhIjPhaczOPuCdE73YQbDzGhGKicZYfPslaT9NUEMeCOZ4Zd7DLgKPE+9fX8pXo4nEICO6SlwN0PbCbrTbxdP0yFbC+00Z86GmAQs197FbSy0QzQYXtof3+3GpkEyHQ+AYOiA53EQ9n00rOE1Sa/WJZRYzIfUwzeITLTb4yBHsw0RmeKOMY4y24LULGgT8kq0hT87FanmYoiFfLd/2gjjbym1NVx4LeNxxQ79DgxDsPFlm/UED8ykWQPSDs7mqt4pB4lxw==

>> 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