Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://agda.readthedocs.io/en/latest/getting-started/installation.html below:

Website Navigation

• Agda

Installation — Agda 2.9.0 documentation

To get started with Agda, follow these three steps:

• Step 1: Install Agda

• Step 2: Install the Agda Standard Library (agda-stdlib)

• Step 3: Install and Configure a Text Editor for Agda

In case of installation problems, check the section on troubleshooting.

Hint

If you want a sneak peek of Agda without installing it, try the Agda Pad.

There are at least four options for installing Agda:

Pre-built binaries are available for the following platforms:

• Windows (x86-64)

• Linux (x86-64, statically linked)

• macOS (x86-64)

• macOS (arm64, i.e. Apple M-series)

They can be downloaded from the Agda GitHub releases page (under “Assets”).

To install, download the appropriate archive, extract the binary, and place it in a directory listed in your PATH environment variable.

Important

This option does not require GHC. However, Agda programs cannot be compiled into executables without it. If you need to compile Agda programs, follow the GHCup installation instructions to install GHC.

Attention

On macOS, these binaries are not notarised, and will not run unless the quarantine attribute is removed:

Agda is intimately connected to the Haskell programming language: it is written in Haskell and its GHC Backend translates Agda programs into Haskell programs. So the most common way to install Agda and keep it up to date is through Haskell’s package manager, Cabal.

Non-Windows users need to ensure that the development files for the C libraries zlib and ncurses are installed (see https://zlib.net and https://www.gnu.org/software/ncurses/). Your package manager may be able to install these files for you. For instance, on Debian or Ubuntu it should suffice to run

apt-get install zlib1g-dev libncurses5-dev

as root to get the correct files installed.

Follow the GHCup installation instructions to install GHC and Cabal (see Tested GHC Versions for a list of supported GHC versions). You should now have the ghc and cabal commands available.

Now that you have cabal installed, use it to install Agda as a Haskell package:

cabal update
cabal install Agda

You should now have the agda command available.

Hint

If these commands aren’t available, check that programs installed by cabal are on your shell’s search path. This should have been done during the installation of cabal, but if not, the installation location is described by field installdir in the cabal configuration (check ~/.cabal/config; it defaults to ~/.cabal/bin). So e.g. under Ubuntu or MacOS you may need to add export PATH=~/.cabal/bin:$PATH to your .profile or .bash_profile.

Note

Some installation options are available through Installation Flags, although in most cases the defaults should be fine.

If you want to work on the Agda compiler itself, or you want to work with the very latest version of Agda, then you can compile it from source from the Github repository.

You should have GHC and Cabal installed (if not see the instructions in Option 1: Install Agda as a Haskell Package (recommended)).

Agda depends on the alex and happy tools, but depending on your system and version of Cabal these might not be installed automatically. You can use Cabal to install them manually:

cabal update
cabal install alex happy

In the top-level directory of the Agda source tree, run:

cabal update
make install

To install via stack instead of cabal, copy one of the stack-x.y.z.yaml files of your choice to a stack.yaml file before running make. For example:

cp stack-8.10.7.yaml stack.yaml
make install

Packaged Agda binaries and the Agda standard library are provided by various package managers. Installing Agda binaries can be faster than installing Agda from source, but installation problems might be harder to work around.

An OS-independent binary installation of Agda is provided by the python installer.

Warning

Depending on the system, prebuilt packages may not contain the latest release of Agda. See repology for a list of Agda versions available on various package managers.

See Prebuilt Packages and System-Specific Instructions for a list of known systems and their system-specific instructions.

Most users will want to install the standard library. You can install this as any other Agda library (see Library Management). See the agda-stdlib project’s installation instructions for the steps to take to install the latest version.

Your choice of text editor matters more in Agda than it does in most other programming languages. This is because Agda code typically uses a lot of unicode symbols, and because you will typically interact with Agda through the text editor while writing your program.

The most common choice is Emacs. Other editors with interactive support for Agda include

• Visual Studio Code (agda-mode on VS Code)

• Neovim (Cornelis), and

• Vim (agda-vim)

Emacs has good support for unicode input, and the agda-mode for emacs is maintained by the Agda developers in the main Agda repository and offers many advanced features.

After installing the agda program using cabal or stack run the following command:

The above command will first write the Agda data files to the Agda data directory (see --print-agda-data-dir) if this directory does not exist yet. (To force writing the data files there use the --setup option of agda.)

It then tries to set up Emacs for use with Agda via the Emacs mode. As an alternative you can copy the following text to your .emacs file:

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

It is also possible (but not necessary) to compile the Emacs mode’s files:

agda --emacs-mode compile

This can, in some cases, give a noticeable speedup.

Warning

If you reinstall the Agda mode without recompiling the Emacs Lisp files, then Emacs may continue using the old, compiled files.

If you are installing Agda using Cabal on Windows, depending on your system locale setting, cabal install Agda may fail with an error message:

hGetContents: invalid argument (invalid byte sequence)

If this happens, you can try changing the console code page to UTF-8 using the command:

You may get the following error when compiling with the GHC backend:

Compilation error:

MAlonzo/RTE/Float.hs:6:1: error:
    Failed to load interface for ‘Numeric.IEEE’
    Use -v to see a list of the files searched for.

This is because packages are sandboxed in the Cabal store (e.g. $HOME/.cabal/store) and you have to explicitly register required packages in a GHC environment. This can be done by running the following command:

cabal install --lib Agda ieee754

This will register ieee754 in the GHC default environment.

If you have setting executable-dynamic: True in your cabal configuration then installation will likely fail on Windows.

Cure: change to default executable-dynamic: False.

Further information:

Agda has been tested with GHC 9.2.8, 9.4.8, 9.6.7, 9.8.4, 9.10.2, and 9.12.2.

When installing Agda the following flags can be used:

debug

Enable debug printing. This makes Agda slightly slower, and building Agda slower as well. The --verbose={N} option only has an effect when Agda was installed with this flag. Default: off.

debug-serialisation

Enable debug mode in serialisation. This makes serialisation slower. Default: off.

debug-parsing

Enable debug mode in the parser. This makes parsing slower. Default: off.

dump-core

Save GHC Core output during compilation of Agda. Default: off.

enable-cluster-counting

Enable cluster counting. This will require the text-icu Haskell library, which in turn requires that ICU be installed. Note that if enable-cluster-counting is False, then option --count-clusters triggers an error message when given to Agda. Default: off, but on for development version.

optimise-heavily

Optimise Agda heavily. If this flag is on, compiling Agda uses more memory but Agda runs faster. Default: on.

use-xdg-data-home

Added in version 2.8.0.

Install data files under $XDG_DATA_HOME/agda/$AGDA_VERSION by default instead of the installation location defined by Cabal; see --print-agda-data-dir. This should not be enabled in declarative build environments like Nix or Guix. Default: off.

Hint

During cabal install you can add build flags using the -f argument: cabal install -fenable-cluster-counting. Whereas stack uses --flag and an Agda: prefix, like this: stack install --flag Agda:enable-cluster-counting.

If cluster counting is enabled (see the enable-cluster-counting flag above, enabled by default), then you will need the ICU library to be installed. See the text-icu Prerequisites documentation for how to install ICU on your system.

You may want to keep the default environment clean, e.g. to avoid conflicts with other installed packages. In this case you can a create separate Agda environment by running:

cabal install --package-env agda --lib Agda ieee754

You then have to set the GHC_ENVIRONMENT when you invoke Agda:

GHC_ENVIRONMENT=agda agda -c hello-world.agda

Note

Actually it is not necessary to register the Agda library, but doing so forces Cabal to install the same version of ieee754 as used by Agda.

Multiple versions of Agda can be installed concurrently by using the --program-suffix flag. For example:

cabal install Agda-2.6.4.3 --program-suffix=-2.6.4.3

will install version 2.6.4.3 under the name agda-2.6.4.3. You can then switch to this version of Agda in Emacs via

C-c C-x C-s 2.6.4.3 RETURN

Switching back to the standard version of Agda is then done by:

The recommended way to install Agda is through cabal, but in some cases you may want to use your system’s package manager instead:

The following prebuilt packages are available:

• Agda

• Agda standard library

In case of installation problems, please consult the issue tracker <https://gitlab.archlinux.org/archlinux/packaging/packages/agda/-/issues>_.

Prebuilt packages are available for Debian and Ubuntu from Karmic onwards. To install:

This should install Agda and the Emacs mode.

The standard library is available in Debian and Ubuntu from Lucid onwards. To install:

apt-get install agda-stdlib

More information:

• Agda (Debian)

• Agda standard library (Debian)

• Agda (Ubuntu)

• Agda standard library (Ubuntu)

Reporting bugs:

Please report any bugs to Debian, using:

reportbug -B debian agda
reportbug -B debian agda-stdlib

Agda is packaged for Fedora Linux and EPEL. Agda-stdlib is available for Fedora.

dnf install Agda Agda-stdlib

will install Agda with the emacs mode and also agda-stdlib.

Packages are available from FreshPorts for Agda and Agda standard library.

GNU Guix provides packages for both agda and agda-stdlib. You can install the latest versions by running:

guix install agda agda-stdlib

You can also install a specific version by running:

guix install agda@ver agda-stdlib@ver

where ver is a specific version number.

Packages Sources:

• Agda

• Agda-Stdlib

Agda is part of the Nixpkgs collection that is used by https://nixos.org/nixos. Install Agda (and the standard library) via:

nix-env -f "<nixpkgs>" -iE "nixpkgs: (nixpkgs {}).agda.withPackages (p: [ p.standard-library ])"
agda --emacs-mode setup
echo "standard-library" > ~/.agda/defaults

The second command tries to set up the Agda emacs mode. Skip this if you don’t want to set up the emacs mode. See Installation from source above for more details about agda --emacs-mode setup. The third command sets the standard-library as a default library so it is always available to Agda. If you don’t want to do this you can omit this step and control library imports on a per project basis using an .agda-lib file in each project root.

If you don’t want to install the standard library via nix then you can just run:

nix-env -f "<nixpkgs>" -iA agda
agda --emacs-mode setup

For more information on the Agda infrastructure in nix, and how to manage and develop Agda libraries with nix, see https://nixos.org/manual/nixpkgs/unstable/#agda. In particular, the agda.withPackages function can install more libraries than just the standard library. Alternatively, see Library Management for how to manage libraries manually.

Nix is extremely flexible and we have only described how to install Agda globally using nix-env. One can also declare which packages to install globally in a configuration file or pull in Agda and some relevant libraries for a particular project using nix-shell.

The Agda git repository is a Nix flake to allow using a development version with Nix. The flake has the following outputs:

• overlay: A nixpkgs overlay which makes haskellPackages.Agda (which the top-level agda package depends on) be the build of the relevant checkout.

• haskellOverlay: An overlay for haskellPackages which overrides the Agda attribute to point to the build of the relevant checkout. This can be used to make the development version available at a different attribute name, or to override Agda for an alternative haskell package set.

Homebrew is a free and open-source software package management system that provides prebuilt packages for OS X. Once it is installed in your system, you are ready to install agda. Open the Terminal app and run the following commands:

brew install agda
agda --emacs-mode setup

This process should take less than a minute, and it installs Agda together with its Emacs mode and its standard library. For more information about the brew command, please refer to the Homebrew documentation and Homebrew FAQ.

By default, the standard library is installed in the folder /usr/local/lib/agda/. To use the standard library, it is convenient to add the location of the agda-lib file /usr/local/lib/agda/standard-library.agda-lib to the ~/.agda/libraries file, and write the line standard-library in the ~/.agda/defaults file. To do this, run the following commands:

mkdir -p ~/.agda
echo $(brew --prefix)/lib/agda/standard-library.agda-lib >> ~/.agda/libraries
echo standard-library >> ~/.agda/defaults

Please note that this configuration is not performed automatically. You can learn more about using the standard library or using a library in general.

It is also possible to install with the command-line option keyword --HEAD. This requires building Agda from source.

To configure the way of editing agda files, follow the section Emacs mode.

Note

If Emacs cannot find the agda executable, it might help to install the exec-path-from-shell package by doing M-x package-install RET exec-path-from-shell RET and adding the line (exec-path-from-shell-initialize) to your .emacs file.

An OS-independent binary install of Agda is provided via the Python Installer:

Further information: https://pypi.org/project/agda/

Some precompiled version of Agda bundled with Emacs and the necessary mathematical fonts, is available at http://www.cs.uiowa.edu/~astump/agda.

• Agda 2.6.0.1 bundled with Emacs 26.1

• Agda 2.6.2.2 …

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4