Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Install with cabal - Debian 11.3 #229

Open
CoghettoR opened this issue May 27, 2022 · 1 comment
Open

Install with cabal - Debian 11.3 #229

CoghettoR opened this issue May 27, 2022 · 1 comment

Comments

@CoghettoR
Copy link

CoghettoR commented May 27, 2022

Hi,

Please submit an issue or pull request if these commands don't work for you (in README.md):

cabal update
git clone git@github.com:agda/agda.git
cd agda
git checkout release-2.6.2
cabal install Agda-2.6.2 --program-suffix=-2.6.2  # (takes a very long time)
cd ~/.cabal/bin/
touch ~/.emacs
cp ~/.emacs ~/.emacs.backup
./agda-mode-2.6.2 setup
./agda-mode-2.6.2 compile
mkdir -p ~/bin
cp ~/.emacs ~/bin
cp ~/.emacs.backup ~/.emacs
cd ~/bin
echo '#!/bin/bash' > agdamacs
echo 'PATH=~/.cabal/bin:$PATH emacs --no-init-file --load ~/bin/.emacs $@' >> agdamacs
chmod +x agdamacs
echo 'export PATH=~/bin:~/.cabal/bin:$PATH' >> ~/.profile

I start with an empty "~/.cabal" directory (otherwise it is possible to have installation problems)

I followed the above procedure, with modifications:

I replaced git clone git@github.com:agda/agda.git by
git clone --recurse-submodules https://github.com/agda/agda.git to have access to
the file "standard-library.agda-lib"

I replaced ./agda-mode-2.6.2 setup and ./agda-mode-2.6.2 compile by
./agda-mode setup and ./agda-mode compile

I added the file ~/.agda/libraries containing :
~/agda/std-lib/standard-library.agda-lib (you have to adapt if necessary with your own path)

so I could use agda-algebras (but with another slight modification):
$ git clone https://github.com/ualib/agda-algebras.git

I replaced, in the file agda-algebras.agda-lib the line depend: standard-library-1.7 by the line depend: standard-library-1.7.1

$ cd agda-algebras
$ make test
[...]
$

or

$ cd src/Examples/Categories
$ agda Functors.lagda
$

Have a nice day,

@JacquesCarette
Copy link
Collaborator

Thanks a lot for the report - one of us will look in more detail soon.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants