The Coq mailing list

[Anton Trunov <anton.a.trunov AT gmail.com>]

Another version I can think of is to create 2 files:
`SetOptions.v` and `UnsetOptions.v`.

$ cat SetOptions.v
Global Set Implicit Arguments.

$ cat UnsetOptions.v
Global Unset Implicit Arguments.

$ cat lib.v
Require SetOptions.
Definition id (A : Type) (a : A) := a.
About id. (* A is implicit *)
Require UnsetOptions. (* restore default options *)

$ cat user.v
Require Import lib.
Definition id_user (A : Type) (a : A) := a.
About id_user. (* A is NOT implicit *)

There are at least two disadvantages to this approach:
 - we need to remember to unset the options;
 - the user needs to set their options _after_ `Require Import lib`. 

—
best regards,
Anton

> On 3 Feb 2017, at 17:44, Ralf Jung 
> <jung AT mpi-sws.org>
>  wrote:
> 
> Hi,
> 
>> FWIW, `Load options.` would work for this minimalistic example.
>> I'm not so sure if it's useful in your setting.
> 
> That's an interesting vernacular!
> However, it doesn't seem to be intended for libraries.  In particular, I
> cannot say "Load iris.options.", I can only say "Load options."  The
> documentation says this is loaded from "the loadpath"; it seems not to
> have been updated since -Q was added.  But tests shows that the logical
> path a physical directory is mapped to seems to be irrelevant for "Load".
> 
> The lack of qualification also means that even though we put everything
> into an "iris" module, we have to call this file "iris_options" or so,
> to make it globally unique...
> 
> Kind regards,
> Ralf
> 
>> 
>> -Anton
>> 
>>> On 3 Feb 2017, at 14:51, Ralf Jung 
>>> <jung AT mpi-sws.org>
>>>  wrote:
>>> 
>>> Hi all,
>>> 
>>> there are some Coq options ("Set ...") that we want to set in a
>>> particular way for all files in our library, but do not want to force on
>>> our users.  For example
>>> 
>>> Set Default Proof Using "Type".
>>> 
>>> Right now, we have that line at the top of every file, but that clearly
>>> doesn't scale.
>>> 
>>> We got the advice to instead create a file, e.g. "options.v", put the
>>> settings in there, and import that file everywhere.  However, that does
>>> not seem to work, as the following testcase shows:
>>> 
>>> $ cat options.v
>>> Set Implicit Arguments.
>>> $ cat test.v
>>> Require Import options.
>>> (* Set Implicit Arguments. *)
>>> Definition id (A : Type) (a : A) := a.
>>> 
>>> Even though the option is set in "options.v", it is not in effect in
>>> "test.v".  I can of course change options.v to use "Global Set", but
>>> then the option will leak to everything that even imports test.v, i.e.,
>>> to every user of our library -- which we specifically tried to avoid.
>>> Using "Require Import" or "Require" in test.v also does not seem to make
>>> any difference.
>>> 
>>> Is there any way in Coq to set options in every file of a library
>>> *without* imposing these options on the user, and without repeating the
>>> option in every single file?
>>> 
>>> Kind regards,
>>> Ralf
>>