The Coq mailing list

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

Hi,

all the "Load"-based approaches have one problem in common: it seems
impossible to "Load" a file from an installed library.  So let's say
iris has a file "iris_options.v" ("Load" does not support giving paths
like "iris.options", so we have to do silly things like use globally
unique filenames).  All Iris files do "Load iris_options."
  Now we have something else using Iris, and it also wants to use the
same options.  However, doing "Load iris_options." now fails because
"make install" totally did not install the "iris_options.v" file; just
"iris_options.vo" was installed.

On 03.02.2017 16:26, Anton Trunov wrote:
> Another version I can think of is to create 2 files:
> `SetOptions.v` and `UnsetOptions.v`.
[...]
> 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`. 

Plus, we need to know the default setting and keep our file up-to-date
with that.  I don't think we'd want to go with this.

Kind regards,
Ralf

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