coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

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: Tue, 7 Feb 2017 19:04:46 +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:4aiOEhzCmugNahvXCy+O+j09IxM/srCxBDY+r6Qd1OkWIJqq85mqBkHD//Il1AaPBtSHraIcwLuP+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFHiTanYr5+MBq6oAHMusILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8qBkRgPohioZLjI16XzahdZtg6xHvB2huQFwzoHJa42RNPdyYqbRcNUHTmRDQ8lRTTRMDJ6mb4sBEeQPPeVWoYfzqFQBrxSxGQaiCfjzyjJKnHL6wbE23uojHAzAwQcuH8gOsHPRrNjtKKkdS+S1zKfVxjvHcvNW3zj945XPfxAjvPGMW71wfNHUyUk3FgPJl06QqIL+Pz+P0eQNqWeb4vNmWOmyiGAnsxl8riWhy8ookIXFm4YYxkrZ+Sljz4s4Idu1Q1Nhb9G+CptfrSSaOpN2Qsw8R2Fovz43yr0Ytp6hZicG0pEnxwbea/CecIiI5gnjW/2LLTd9nHJld6iziAus/kS4y+38UNe70EpSoyZYnNTBsmoB2wHX58SdV/dx5Eis1DKX2wDW8O5EIEQ0laTBK54mx749jpgTsVnFHi/5g0j2ibeWdkQ99uiz5eXnea/qppiGN497kg3+KLghmtSjAeQkNQgDR3SU+eOl1LH64UL5RKhKgeYtn6nCsJHaINwbqbSjDw9U1IYj8Re/AC283NQWh3lUZG5CLRmAls3iP0zECPH+F/a2xVq2ww1m3/TXArq0CZLUa3PHjb3JfLBn6kcaxhBg48pY4sduA7UPaNDuXEC54N7FCBARNhS1hv34E5N6zIxICjHHObOQLK6H6QzA3ekoOeTZOdcY

Hi again,

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

The good news is that we can hack the Makefile to install .v files, and
then "Load iris_options" will work.

Somehow I feel like I am not using this the way it is intended to be used...

; Ralf

[Coq-Club] Setting Coq options for all files in a project, Ralf Jung, 02/03/2017
- Re: [Coq-Club] Setting Coq options for all files in a project, Anton Trunov, 02/03/2017
  - Re: [Coq-Club] Setting Coq options for all files in a project, Ralf Jung, 02/03/2017
    - Re: [Coq-Club] Setting Coq options for all files in a project, Anton Trunov, 02/03/2017
      - Re: [Coq-Club] Setting Coq options for all files in a project, Matthieu Sozeau, 02/03/2017
        
        Re: [Coq-Club] Setting Coq options for all files in a project, Ralf Jung, 02/07/2017
        
        Re: [Coq-Club] Setting Coq options for all files in a project, Pierre-Marie Pédrot, 02/07/2017
        
        Re: [Coq-Club] Setting Coq options for all files in a project, Ralf Jung, 02/07/2017
      - Re: [Coq-Club] Setting Coq options for all files in a project, Ralf Jung, 02/07/2017
        
        Re: [Coq-Club] Setting Coq options for all files in a project, Ralf Jung, 02/07/2017