Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Setting Coq options for all files in a project

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Setting Coq options for all files in a project


Chronological Thread 
  • From: Ralf Jung <jung AT mpi-sws.org>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Setting Coq options for all files in a project
  • Date: Fri, 3 Feb 2017 15:44:23 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
  • Ironport-phdr: 9a23:bz+J2hPR+Tvk721n+sEl6mtUPXoX/o7sNwtQ0KIMzox0Lfz5rarrMEGX3/hxlliBBdydsKMYzbWP+P67EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT6ybL9oLhi6sArdu8gYjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRjnhjsHOTMn6W3bk9F9g7hGrxy9uxN/3ZPbbY6IP/Z6fq7RYdYWSGxcVchTSiNBGJuxYZYRAeoPPehWrIfzqFUBohS8GQaiC/jiyiNKi3LswaE2z+osHAHA0Qc9H9wOqnPUrNDtOakOS++1yKfIxijHYfNL3zf955XDfxcjofGRW7JwftHcyUw3FwPEl1mQsoLkPyiP2uQKqWib4PNtWOSygGAkswF8uiWjy8koh4XTm44YzkrI+ThjzIs6IdC1TlNwb8S+H5tKrS6aMpN7QsM8TGFsvyY30r0GtoChfCcQ0pgnwgbfa/2ef4iL5hLjT/2eLS19hHJ9d7KznQu9/la4xu39UMm7zkpKozJYntTCsn0BzQHf58ydRvdg5Eus1jKC2xjW6u5eIEA0kaTbK4Qmwr41jpcTs1nDHin5mEjtia+WbkQk9vGz6+XpebXqvJicN5V7ig3mKKQhhtS/AfgkMggJR2WU5eO81KT68ULlRLVKk+Y5n7LCsJHaIMQbvrS2DxVU0oYl8Ra/Di2p3M4WnXkdfxp5f0eMiJGsMFXTKtj5C+2+ihKiimRF3ffDa4foBpuFDGXFn/+1f6t75GZZ0At21s9EoZVOBedSc7rIRkbtuYmAXVcCOAuuzrO6UNg=

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
>



Archive powered by MHonArc 2.6.18.

Top of Page