coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Software foundation for older versions of coq

From: Michael Soegtrop <MSoegtrop AT yahoo.de>
To: coq-club AT inria.fr, "Fernandez, Matthew" <matthew.fernandez AT intel.com>
Subject: Re: [Coq-Club] Software foundation for older versions of coq
Date: Wed, 23 Dec 2020 10:23:11 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=MSoegtrop AT yahoo.de; spf=Pass smtp.mailfrom=msoegtrop AT yahoo.de; spf=None smtp.helo=postmaster AT sonic311-23.consmr.mail.ne1.yahoo.com
Ironport-phdr: 9a23:+65NhxcK2d4CRxwZc2CNhe/zlGMj4u6mDksu8pMizoh2WeGdxcW4Yh7h7PlgxGXEQZ/co6odzbaP7Oa6ATNLuc/JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRe7oR/PusUKg4ZuJbo9xgbUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU063/chNBug61HoRKhvx1/zJDSYIGJL/p1Y6fRccoHSWZdQspdUipMCZ6+YYQSFeoMJftWoZfzp1UOrhWwCwejC+ztxTBUiXH42rY30/gjHAzcwAAtBdwDvXbSod7oNKkSS+e1zKzQwDvEbvNZxTf955LWfRAlvPqCQLVwftTeyUkzDQPFiU2QopHiMj2Sy+oNtHaU7+V8VeK1jG4nsxp8ozi1yccsjYnJgZgZxU3a+ihgxos+ONK3RlJhb9G+DJtQqz+VN5FwQs46X2xlpDo3x7IbtJC0YSQH1JsqyhHQZfCbboWE/hzuWeSPLDl3mX5pZLOyiRm2/EWuxODxSNS53VVFoyRLkNTBtnYA3AHQ5MifUvZw/0as1SyS2w3S5OxIO104mKnYJpI73LI8ipUevELeFSHsgkr2lrWZdkA89+io9evnZrLmq4eHN49zjAH+M7ghl8KiDeglKwQCQWaW9f6g273k+035W7BKjucsnqncqp/aJMAbqrS/AwBLz4ov8Ra+AC2m0NQfmnkLNk5KeBWCj4TxOlHOJu73DeunjlmtkTpn3e3KM7zvD5nXM3TOk7Tscaxj50JAxwc/1dVf6IhVCrEFLvLzQEjxtNnAAx88KAy0xPjoCNph1oMEXmKPGrSUMaPIvl+I4eIvJPOAa5ILtzrlMfgq++bujWMlmV8aZaSmwZwXaGmhEvt6J0WZfGHjj8waEWYKuwo+VPblhEeDUT5VfXayXrgz6is1CIK8Xs//QdWmh6XE1yOmFLVXYHpHAxaCCzOgPauJQfEFbi6fMIsptzUYSbisVMVpgRSnqBP6xqUhIOfO/CQeuZ/x/Nlz++DX0xo18GonId6a1jSoTmp0l24MDwQx0a9ju0tlggOm6q91jOBCEsR79vpJVQB8OZOKnL8yMMz7Rg+UJoTBc12hWNjzRGhpFotske9LWF50HpCZtj6G3yeuBORExaeMAp0/qfuFmiKqYc16zW3Dzu8khlgiBM1CbCu3j6548E7YAIubyxzFxZbvTrwV2Wv2zEnG1XCH5RkKQQdwVqKDUX1NPhKH/+S83VvLSvqVMZpiNwJAzcCYLa4TMo/4hFVBQ7HvNYaHbg==

Hi Matthew,

I have access to some Linux boxes where I do not have root and the local file
system is read-only.

Opam by default installs its database in ~/.opam, which should be writable. Is it so that your home directory is too small? A complete build of the Coq platform can take 5GB of disk. I could add an option to trade speed vs. size (e.g. install packages sequentially and run opam clean after each package) but it would still be largish.

It is not hard to put the opam root somewhere else and I also think that it is possible to change the install prefix of a specific switch. Currently the Coq platforms scripts don't support this directly - one would have to first init opam manually and then run the script, but I can for sure add this, since several users seem to have such issues. I will ping you when I have something to test.

Best regards,

Michael

Re: [Coq-Club] Software foundation for older versions of coq, (continued)
- Re: [Coq-Club] Software foundation for older versions of coq, Clément Pit-Claudel, 12/21/2020
  - Re: [Coq-Club] Software foundation for older versions of coq, Pierre Courtieu, 12/21/2020
    - Re: [Coq-Club] Software foundation for older versions of coq, Benjamin Pierce, 12/21/2020
      - Re: [Coq-Club] Software foundation for older versions of coq, Pierre Courtieu, 12/21/2020
        
        Re: [Coq-Club] Software foundation for older versions of coq, Benjamin Pierce, 12/21/2020
    - Re: [Coq-Club] Software foundation for older versions of coq, Michael Soegtrop, 12/21/2020
      - RE: [Coq-Club] Software foundation for older versions of coq, Fernandez, Matthew, 12/22/2020
        
        Re: [Coq-Club] Software foundation for older versions of coq, Michael Soegtrop, 12/23/2020
        
        RE: [Coq-Club] Software foundation for older versions of coq, Fernandez, Matthew, 12/23/2020
    - Re: [Coq-Club] Software foundation for older versions of coq, Michael Soegtrop, 12/21/2020