coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq Ocaml version

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: Théo Zimmermann <theo.zimmi AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Coq Ocaml version
Date: Fri, 15 Mar 2019 18:31:36 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:VhSTgxFwrRgFSCLPHkzsr51GYnF86YWxBRYc798ds5kLTJ78osiwAkXT6L1XgUPTWs2DsrQY0rKQ6/mocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmSaxbaluIBmrsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95RWSJfH428aIUPAeQDMuhboYbyqEcBoxSlCAmwHePi0CNEimPs0KA41ekqDAHI3BYnH9ILqHnao9D1NKYWUeC0y6nH1THNYO1N2S/n84jHahEvruuIXbJ0b8XRxk4vGBvZg1WKqIzqJSiV3fkKvmeF9OdhWuGih3I9pwF2uDivyd4hh4/UjYwW0lDJ7Th1zYU2KNGiVkJ3f9+pHIFNuyyYKod6WN4uTm92tCoi17ELt5y2cDIXxJkjyBPTcf6KfoaS7h79SuqcITF1j29/dr2lnRa9602gx/X8Vsaq1FZKqTJIk9bPu3wRzRDT7dKHSvRl8keg3zaAyRzT5/lZLU03lqfXMYAtzqAxm5YJrEjOHDL6lF/rgKKYaEko4u2o5P7mYrXiqJ+cLYh0igTmP6swgcG+Duc1PhQUU2ic4+S826Xv/VflT7VSkv02jq7ZvYjGKsQcv661GhNa0oI+6xmkFDqmy9QZnXwfLF1fYh6Hjo7pO0vPIP/iF/u/jU6sw39XwKX6PjzmSqfMK33OirLoe7A1v1JcxQ1139Fa4pN8BbQIIfa1UUj04o/2FBg8ZiGxwuLmD+Jf25iMQlWgC6udPazVhnaS5+s0a72BTJ9F4HD6MfdztK2mtmMwhVJIJfrh5pAQcn3tW60+exzIM0qpuc8IFCIxhiR7SeXrjFOYVjsCNWbiB+Q7/D5pUdv6X7eGfZikhfm65An+BodfNzJWWgjKFm3nJd3dBqU8LRmKK8okqQQqELisT4hwhwH+7En90bU1d+c=
Organization: X80 Heavy Industries

Théo Zimmermann
<theo.zimmi AT gmail.com>
writes:

> "This configuration" includes the use of the OCaml flambda compiler.
> My point was that, in case the flambda compiler is not used, the
> options are (probably, but this needs to be confirmed) harmless.

They are indeed a noop when the compiler doesn't have flambda.

> In this case, there is no problem in changing the default value of
> these options, as it only affects the users of the flambda compiler.

There is a problem with OCaml < 4.07 + native compute enabled.

E.

Re: [Coq-Club] Implementation of Coq's automation tactics, (continued)
- [Coq-Club] Coq Ocaml version, Laurent Thery, 03/14/2019
  - Re: [Coq-Club] Coq Ocaml version, CYRIL SIX, 03/14/2019
  - Re: [Coq-Club] Coq Ocaml version, Emilio Jesús Gallego Arias, 03/14/2019
    - Re: [Coq-Club] Coq Ocaml version, Xuanrui Qi, 03/14/2019
      - Re: [Coq-Club] Coq Ocaml version, Laurent Thery, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Théo Zimmermann, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Gaëtan Gilbert, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Ian, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Théo Zimmermann, 03/15/2019
        Re: [Coq-Club] Coq Ocaml version, Emilio Jesús Gallego Arias, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Emilio Jesús Gallego Arias, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Emilio Jesús Gallego Arias, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Laurent Thery, 03/16/2019
      - Re: [Coq-Club] Coq Ocaml version, Emilio Jesús Gallego Arias, 03/15/2019