The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  Can't you do this by passing a specific coqrc file to the -init-file option of coqc or the -require flag? (untested) Just when working on the library I mean.

-- Matthieu

On Fri, Feb 3, 2017 at 4:26 PM Anton Trunov <anton.a.trunov AT gmail.com> wrote:

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