coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "Fernandez, Matthew" <matthew.fernandez AT intel.com>
To: Michael Soegtrop <MSoegtrop AT yahoo.de>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Software foundation for older versions of coq
Date: Wed, 23 Dec 2020 17:43:03 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=intel.com; dmarc=pass action=none header.from=intel.com; dkim=pass header.d=intel.com; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=NJeE31ZahqNaDec9tMz/WSSAk1M6BOohqiXsCLTVqtk=; b=D7QFU9P3EhN8ilHevna/T3/c+7JMUn9zBU3OzbQV/TlgFXprOWg0p3EiiCp70Ey1YvfcPDPz7WKkyteZAx/CwtTYY03rfQaaaOUYKm8Far14nQA8A3Wh+fCCJoNx4dv+HnGfIoatMzm8Z7DGDL0IgXq0cAPGoCNHk+tY3Bq7q6ziBhOCvwH9upq8bhL1IjDVxuILKhrCbQ9Kly5ISJvqs/UB4yZcLk0zsF+bYKLXN2jS7HAO8+o4UT33XRF9/E6YuH/MdcEOOTBTcDJCblpgLpFxA3ZmMsnFI0Ny7qpqE07bCSwa81QGboZZ7mmHE7wlO1PLyKdJGPc/wWXYY9oBGA==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=PTC3bYXJzMFQB1ZN0Fi6wQ6uBErhlvbMvNeOUsPz0l3DWGi+zCLo19Irc2m6yirMKzJRfw7/OxfqYoj7av1h3jhpDQD7YU5q1i2z11ptulRfAAMCUVWh1XADuMCOLEEUE8Zorwg1E1rE76P87TuBmFi4lrLUh71uSQHCF6sR40s7b4LltcbwNBSKiTwoXtcUYku9uO5dSQzgEhBQX4l5D0Z6uFYB5lKHH2pnXIpmtyaUF9JEz2gO1SOwU+doT0pBDJmj1Nlj53Vt9DToOa5zp2ASpoU1/oJkZUKKBjca/aYiCMtVaw3CAq6DhuP0ENP5vrpaEGEQ+2bP1iqDd/4Y3A==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=matthew.fernandez AT intel.com; spf=Pass smtp.mailfrom=matthew.fernandez AT intel.com; spf=None smtp.helo=postmaster AT mga09.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.5.1.3
Ironport-phdr: 9a23:JqtpQxbtleQwj9N6TzpKN+H/LSx+4OfEezUN459isYplN5qZpsy7bR7h7PlgxGXEQZ/co6odzbaP7Oa6ATNLuM7b+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi0oAnLqMUanYlvJqksxhfVvHdDZvhby35vKV+PhRj3+92+/IRk8yReuvIh89BPXKDndKkmTrJWESorPXkt6MLkqRfMQw2P5mABUmoNiRpHHxLF7BDhUZjvtCbxq/dw1zObPc3ySrA0RCii4qJ2QxLmlCsLKzg0+3zMh8dukKxUvg6upx1nw47Vfo6VMuZ+frjAdt8eXGZNQ9pdWzBEDo66coABDfcOPfxAoof9uVUAsAe+CwevCuPhyDBIh2P506I13Ok6DQHJxxAsE84SvHjIrtj4MroZX+CvzKnPyDXOd/1a1zfj54jSdBAuu/eMUq9ufsvQ0UUkCgTLgU+MqYz5PzOayOoMv2aG5OdnUOKgkXInqx1xojexyMYgkIfJiZwPylDC7yp5xps6KsO5SUNgYN6kFodQuD+eN4dsXswiRGRotT88x7YbtpG1YDIEx447xx7DdfOHaY6I7wr+WOuVIDp1hHxodb29ihuv7EWty/DwW9S73ltEsyZInNbBu20N2hLT6cWLV/Rz8lu81TuSyw3e9+JJLF41mKfGLZMq370+loILvEjeECL7l1/6gLKYe0gr4OSk9urqb7T8qpOCOIJ4kgPzP6U0lsCiHOg1MhICU3aG9eim0LDu/lX1TKtLg/EqnKTUtY3WKdgAqaO4BgJY3Jov5hi6Ajqmy9sVmHwKIE9HdR+BkoPnIUvBIOriAve6m1mskClkx/TBPrD5B5XNIWLMnKvlcLpn6k5czhYzws5b555OFr4BJ/fzVlfwtNzeEBA5LxS5z/vpBdhyzI8SRGyCD6CDPK/Pv1KF5/gjL/eDaYMNvTbyMfkl5/rgjX8jnl8deLGk3Z4NZ3CkAvRmI1uWYHT2jtcPD2gKpAw+Q/bsiFKfTzFSZm2/X6M65jEnFo2mCZ3PSZyqgLyExCu7BIFZZnhaClCQFnflb5mLW/AVaC6LPsBhliEEWqO6Ro861RCusRf6xKB9IurV/C0Yr5Pj28Jv6+3djxFhvQBzWuGc2GGEQmU8pWQFSCMs27g39WlGzVqMzbJ/m9RJHNxU4LVFX1F+fdTXyPU/ANTvUCrAeM2IQRCoWJ/uVTo2V5c6x8IES0d7AdSryB7ZiXmEGbgQwvalCYYy+6TQ0mq1b+N012rG2bZrxw0jS9dTNWC5wKBy7Q7aAYLEgW2YkbqnceIX2yubpzTL9naHoEwNCF04aq7CR31KIxKO9Y2otHOHdKenDPEcCiUEzMeDLqVQbdiw1AdHQuvuPJLVZGfjwj7tVybN/auFac/RQ0tY3CjZDxFbwQUc9C7Xcwk4Giql5WnZCW42TA69UwbX6eB77UiDYAos1QjTNh9g0aa4/lgegvnOE/4=
Ironport-sdr: IjNm/USmqXDyEm3n+G3bsvzX7QCL+iE0f0PVotu9/JjTX6gqRLEcXQlQZxOAtAsuVwLsZSL1sj F+Ea2OK/W7Og==
Ironport-sdr: DZO/5+H6yu2b6CaE9u61se23e/k/cOXkcQSWKSXiPirYgBRrMZWWlmTRo6m7yPSgPZM09ukQ+z +zbx5k3mK6lw==

Hi Michael,

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

Sorry, I was just noting some other reasons these issues are relevant, not
that I have specific problems With Coq or OCaml. My home directory is indeed
too small, but I worked around this by either symlinking ~/.opam or
overriding $HOME. Currently I don't have any show stoppers to running Coq.

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