Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
    < Chronological >      < Thread >
  • 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.

Archive powered by MHonArc 2.6.19+.

Top of Page