Include clearer installation instructions about cubical HOT 8 CLOSED

For those not familiar with agda we could certainly have more detailed instructions.

If you don't mind, could you tell us if the following helps?

Once you have agda master installed by following these instructions, given in the readme:

git clone https://github.com/agda/agda
cd agda
cabal sandbox init
cabal install

Then you want to "install" the emacs mode by running

agda-mode setup

Then you can just open the files from the cubical repo in emacs and work with them. The emacs mode is briefly described here
https://agda.readthedocs.io/en/latest/getting-started/quick-guide.html#quick-guide-introduction

If you want to use cubical as a library in your own development you have to "register" its .agda-lib file as described here:
https://agda.readthedocs.io/en/latest/tools/package-system.html?highlight=library

There's no compilation involved in installing an agda library, you just have the source files and agda will generate .agdai interface files on demand.

from cubical.

After running cabal install I cannot run agda-mode setup. There is no command, nor has agda been installed.

Edit

I think this is an issue with cabal install. I managed to find agda-mode in the dest folder and run it from there. Although I am not convinced it has actually done anything.

If agda-mode adds the following to my .emacs file:

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

Then if agda-mode isn't working properly, what use is it?

For whatever reason cabal install isn't installing agda-mode. I think this is due to the sandbox, but I don't know enough about cabal to get around this.

from cubical.

cabal install by default installs things in a local directory, on linux it's ~/.cabal/bin, maybe you do not have that in your $PATH.

from cubical.

I've checked inside ~/.cabal/bin there is no agda or agda-mode. I'm fairly sure this is because cabal install kept everything inside the sandbox, but that isn't really the way to install agda is it? I understand why the sandbox is being used, in order to build the developer version, however I don't think I can install it correctly.

from cubical.

I see, I don't use cabal sandbox myself, it seems you indeed have to copy the files from the sandbox to somewhere in your $PATH

https://stackoverflow.com/questions/27274475/cabal-install-an-executable-from-hackage-via-a-sandbox

@mortberg what do you do?

from cubical.

I just update my PATH in ~/.bashrc:

PATH=/home/mortberg/dev/agda/.cabal-sandbox/bin:$PATH

Writing some detailed install instructions in an INSTALL file sounds like a good idea. Maybe @Alizter can write a first draft once you get it to work?

We should not forget to include some instructions for how to set it up as a library.

from cubical.

I have managed to get it to work now. I installed agda-2.6.0 without using the sandbox.

A big potential confusion is definitely the $PATH variable. We will just have to tell users to make sure they have $HOME/.cabal/bin added to their path in .basrc. (And maybe restart the terminal so it reloads .bashrc).

Now I understand why the sandbox is used. If you don't have agda then there is no problem, do what I did. But if you already do then the library doesn't simply add on (yet). The current agda version is agda-2.5 yet this library only works for agda-2.6 and upwards.

A possible solution to this is having an install script? It would need to make sure there is the correct version of agda-2.6, if not install it in a sandbox somewhere, compile it and move the executable to the users bin (along with agda-mode). Then the sandbox can be rid of. (However I am not sure how this will interact with existing versions of agda).

from cubical.

I’m happy with the new instructions.

from cubical.