The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

On 03.02.2017 16:32, Matthieu Sozeau wrote:
> 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.

That will just do the equivalent of "Require options_file.", won't it?
The trouble is, we can either set options so that they only affect the
options_file (useless), or we can set them "Global", but then we impose
our options on every user.  The only way to be affected by options from
another file without affecting everyone importing you seems to be "Load".

I was told once that just doing "Set ...." would set options in a way
that they would apply through one, but *not* two levels of "Import" (and
an arbitrary number of "Export"), but that doesn't actually seem to be
the case.

; Ralf

> -- Matthieu
> 
> On Fri, Feb 3, 2017 at 4:26 PM Anton Trunov 
> <anton.a.trunov AT gmail.com
> <mailto: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
>     
> <mailto: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
>     
> <mailto: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
>     >>
>