Installing multiple development version of Idris

[gallais]

It would be nice to be able to specify a suffix to attach to the Idris2 executable to be able to install multiple versions of the development version of Idris2.

At the moment installing a broken version means we are forced to recompile a stable one from scratch or use the slower bootstrap build which is really time consuming.

One tricky aspect: all of these versions may be using different TTC format which means we would need to have multiple versions of the libs in ~/.idris2.

[chrrasmussen]

It is possible to set up multiple versions of the Idris 2 executable by changing the makefile/config files. I am not sure if this is what you had in mind. If not, I think the following can be useful to others anyway.

On my computer I have set up two copies of Idris 2: I have a stable version of idris2 (the master branch with no changes) that I update maybe once a week. And I have a development version called idris2dev.

To set up the development version:

1. Make a clone of Idris 2 to a new directory.
2. Change PREFIX in config.mk to $(HOME)/.idris2dev.
3. Change the NAME in Makefile to idris2dev.
4. Change the executable in idris2.ipkg to idris2dev.
5. Optional step: Change IDRIS2_BOOT in Makefile to point to the Idris 2 executable that you want to build from. In the case of idris2dev I want to use idris2 (so no changes are necessary).
6. Add $(HOME)/.idris2dev/bin to your $PATH to make idris2dev easily accessible.

Show diff

```diff diff --git a/Makefile b/Makefile index 68891e4..e64a699 100644 --- a/Makefile +++ b/Makefile @@ -4,7 +4,7 @@ include config.mk export IDRIS2_BOOT ?= idris2 # Idris 2 executable we're building -NAME = idris2 +NAME = idris2dev TARGETDIR = build/exec TARGET = ${TARGETDIR}/${NAME} diff --git a/config.mk b/config.mk index 0d82ad4..5d2bc6a 100644 --- a/config.mk +++ b/config.mk @@ -1,6 +1,6 @@ ##### Options which a user might set before building go here ##### -PREFIX ?= $(HOME)/.idris2 +PREFIX ?= $(HOME)/.idris2dev # For Windows targets. Set to 1 to support Windows 7. OLD_WIN ?= 0 diff --git a/idris2.ipkg b/idris2.ipkg index 2211067..b45bc7d 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -5,4 +5,4 @@ depends = idris2, contrib, network sourcedir = "src" main = Idris.Main -executable = idris2 +executable = idris2dev ```

---

In the case of #638 I needed 3 copies of Idris 2 to be able to reproduce it:

1. idris2 — Builds from bootstrap
2. idris2dev — Builds using idris2
3. idris2dev-2 — Builds using idris2dev

In order to make it build I did the following:

1. I needed to add toVect from libs/base/Data/Vect.idr to the idris2 copy.

2. Both idris2dev and idris2dev-2 checked out #638 (git fetch origin pull/638/head:pr-638 && git checkout pr-638).

3. To make idris2dev and idris2dev-2 compile, I had make the following change to definedInBlock,defName in src/TTImp/TTImp.idr:

   defName : List String -> ImpDecl -> List Name

Now I could reproduce the error from #632 using the idris2dev-2 executable.

It is still a bit inconvenient as changes to idris2dev also needs to go into idris2dev-2, but it should be better than building from bootstrap every time.