coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq opam instructions

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq opam instructions
Date: Mon, 25 Apr 2016 15:37:01 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f53.google.com
Ironport-phdr: 9a23:uVj/VROvD3dsrYndVUIl6mtUPXoX/o7sNwtQ0KIMzox0KP/6rarrMEGX3/hxlliBBdydsKIUzbWJ+Pm8EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35TxiL/5osGbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSJDUgKWE8osPx5jfZSg7a2HIQU2BeoBNMAhbMpEXkTJ71szXznuF4xW+XMdCgHuN8Yiir86o+EEygsywALTNsqGw=

On Mon, Apr 25, 2016 at 3:26 AM, Jeehoon Kang <jeehoon.kang AT sf.snu.ac.kr> wrote:

Another way to install multiple instances of Coq with opam is using opam aliases:
https://github.com/ocaml/opam/wiki/Advanced_Usage#ability-to-make-a-copy-of-a-given-compiler-under-an-alias

```
opam switch install 4.02.3.coq.8.5.0 --alias-of 4.02.3
opam install coq.8.5.0
```

It sounds interesting, but it still re-compiles OCaml compiler:

$ opam switch

...

4.02.3 C 4.02.3 Official 4.02.3 release

...

$ opam switch install 4.02.3.coq.8.4 --alias-of 4.02.3

=-=- Installing compiler 4.02.3 -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

[default.comp] http://caml.inria.fr/pub/distrib/ocaml-4.02/ocaml-4.02.3.tar.gz downloaded

Now compiling OCaml. This may take a while, please bear with us...

Processing: [4.02.3: make world.opt]

CMU ECE PhD candidate

Mobile: +1(510)220-1060

[Coq-Club] Coq opam instructions, Beta Ziliani, 04/24/2016
- Re: [Coq-Club] Coq opam instructions, Tadeusz Litak, 04/25/2016
  - Re: [Coq-Club] Coq opam instructions, Théo Zimmermann, 04/25/2016
    - Re: [Coq-Club] Coq opam instructions, Jeehoon Kang, 04/25/2016
      - Re: [Coq-Club] Coq opam instructions, Vadim Zaliva, 04/26/2016