coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Fernandez, Matthew" <matthew.fernandez AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Software foundation for older versions of coq
- Date: Tue, 22 Dec 2020 16:17:54 +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=Gb5TaKwRri/LYshHBFXFS+l0Q1vsW4OnH3QZ0lY0JNQ=; b=P+luyMNITEVTZSi7cdzq2Zzf1ruC6xC2ctYdVU7u4wF5qkhFFlfluGH7SrbpZ6peWf1ILFHGgagWcTsMW1dOxIo93oYZ3MaW4R71NqHqykS6uMG57NBAFduR3hiPtcEGqrtRjtvDlKyyzmtsWlrNBwZCwxBMgA8XIVE3PlS7BeAQazSXnY2E11a/VHWsCUxAi/NBsavJyg6flIx51hgsKkspA9tpavB8IlBAzYCDVfTXjYMLPPHpIUq2mowKCVhKsroINJE15cWdSyhJJKuGv/c/JMkOCJU53Qj1xCUOJGeRupnq+F+3AhMpZvUACm7SEXUmQtLUPon0Qjzw7p7Klg==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=AUJAtr7HiSK5d/hORqiKvrUfuxfywwI4qiBM48+EUs99ETKuQN0JMFToVq5spQ7w1Hwwoc4wVnrUiBVNSAZPeTfCBslFWclynDYGrvjP//0GcDM964oNP8T9qMm1y87SvQBbKC1kLshFriZFEljA00ohurrRat6kyLK5m28p0lRyyJcEGgO6ENh4KJgGpPz5Dg+63ij+89JKz/gEFXU1hqigYTWdKZifTeD+SjyQVUuipYzG3lsAOh7E283N6jVZ+/JdGWFiyPjrTv41ysZZ8zzdKegChae4nWoUqfgZnxBPfNXBSNVqYksKlD8RBm7d9BMUeIJKN7sXTmgx6ms2BA==
- 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:gZ29hB3IT4u07BsusmDT+DRfVm0co7zxezQtwd8ZseMSKvad9pjvdHbS+e9qxAeQG9mCtLQe07ad7f2ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbalsIBmqogjducgbjIt/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF+jLxVrg+9pxJxwIDUboOaNPtica3SctwXXnZBUd1NWyBdHo+wc4kCAuwcNuhYtYn9oF4OoAOwCQesGuzv0DlIiWXw3aInzesgEBnK1xEnEd0UrHTUsNX1O7kcUOy70aLFyjDDYOlK2Tfh6IjHbB4greuCXb1ua8rRz1MgFwXYgVqOqI3oJDKV1uIRs2eF6+psT/6gi2kiqwxopDWk28gjhJXTiI0P1lDE6Tt2wJwzJdCgVUJ2Zd+pHZteuiyVNYZ7X94vTmB1tCsnxbMLt4O3cSYFxZk6xxPRa/+Kf5WH7B7/SeqcPCt1iW9mdb+hhhu/7E6twfD/WMmsyFtGsyRIn9bWunwQ2RHe5dKLRuZz80qgwzqDyQ/e5vlGLE01j6bXNoItz74qmpYOtUnOETX6lFv4gaKVbkko5Oml5/jpb7jju5OQK5R7hwD7P6kghsCyD+E1PwgVUGWe/Omwyb/u8EvkS7tQlPI2iLPWsJXCKMQbuKG5BwhV354m6xawFTiqzNAVkWMGLFJDZBKIkYzpN0vSL/D/CPezm1WskDF1yPDaJrDtH5vAI3fZnLv8c7tw5FRQxBc9wN1e/Z5YFL4MLOr2WkDrtdzYChE5Mxazw+biENh905kRWX6TAq+ZLqzTv0WE5uwxLOmWYo8aojD9JOU76P/vlnI5mFkdfbW30psTcny3AvNmI0CBbXr2ntgBCXsKvhY5TOHylFKCVidTa2+uUKI4+zE0E5mrDZzDR4ComLyOxj23HpxQZmBcC1CDC23kd4ueW6REVCXHaMRmi3kPUaWrY44nzxCn8gHggfIzJe3NvyYcqJjL1d5v5uSVmwtkphJuCMHImU+AVWd9mG8FVXt++aljvUxw1R3Lha1xn+BYGMMV6f5TVA48OZPO5+18F932HAnGe4HaGx6dXty6DGRpHZoKyNgUbhMlQojwvlX4xyOvRoQtufmLCZgzq/2O2nf4f5c7ynDa2a1nhF4jEJMWaT+Ww5Vn/g2WPLbn1l2Dnv/zJ6UawCPJsmyEyDjW5RAKYEtLSazAGEsnSA7TpNX96FnFSub3W7UhLgZFj8WFL/kTZw==
- Ironport-sdr: 74+ReL4JpHl61aLGRZ6ufXhjSDO7QlZuh4LoWgxmn47AE0Owhj04VSFIePPmlk3ksOhwx5z/v4 bys182B/8WZQ==
- Ironport-sdr: +06c17MtwYFxZ8tBiqJwPa6kyHYFqzrAzujB9sedGloxBZ8sxy6t2nqhbg5Rl1tiUu0JNZOpES pT5NZ0qt9YJg==
> -----Original Message-----
> From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> On Behalf Of
> Michael Soegtrop
> Sent: Monday, December 21, 2020 12:44
> To: coq-club AT inria.fr
> Subject: Re: [Coq-Club] Software foundation for older versions of coq
>
> Enrico recently made a change in Coq to make it relocatable in a more
> controlled / reliable way. So one way would be to build Coq with opam in the
> usual way and then installing it to system folders using this relocation
> mechanism. We also create Windows installers from an opam switch which also
> uses this relocation mechanism. One could derive a Linux system install
> script
> from that.
>
> It should also be possible to redirect the prefix of an opam switch to
> system
> folders, but this would likely mean that one has to disable opam sandboxing.
> Opam has a mechanism to ensure that make install of packages does not touch
> any files outside of .opam. It is not entirely free of danger to call make
> install for 100 open source packages with root rights. A rm -rf * in the
> wrong
> folder run as root is no fun.
This type of relocatability and sandboxing is also relevant for those of us
trying to run Coq in a corporate environment (yes, boring I know). I have
access to some Linux boxes where I do not have root and the local file system
is read-only. Being able to alter the install prefix to point at an NFS
directory is essential. Sandboxing is not vital for system integrity (as I
don't have permissions to destroy anything anyway), but it is necessary to
prevent wayward rms removing my personal files. For other installers that do
not provide such things, I've had to play FUSE/symlink and Seccomp tricks
which are rather unpleasant.
- Re: [Coq-Club] Software foundation for older versions of coq, (continued)
- Re: [Coq-Club] Software foundation for older versions of coq, Pierre Courtieu, 12/22/2020
- Re: [Coq-Club] Software foundation for older versions of coq, Benoît Viguier, 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, Stefan Monnier, 12/22/2020
- 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, Pierre Courtieu, 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/23/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/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
Archive powered by MHonArc 2.6.19+.