4
votes

I've read the .travis.yml in the agda-stdlib project, while it's very different and complex from a simple library that was written in Agda purely (without those Haskell codes and Shell scripts).

I'm confused with the stdlib's .tarvis.yml. I've installed agda via cabal install, but the stdlib is trying to clone and compile Agda on Travis CI, and there're a lot of commands that seems to be irrealavent to building it.

Also, agda-stdlib seems to be available on Ubuntu's source. This could be the 3rd approach to install it.

Also, the stdlib doesn't have dependencies, but I have. I don't know how to add a dependency either.

Conclusion of my question:

  • In the 3 choices of installing agda listed above, which one should I choose?
  • How to add an dependency that let the agda compiler knows I'm actually using it?
1

1 Answers

1
votes

The standard library is a bit of a special case: it evolves in lock-step with the development version of Agda. As such it is often the case that it cannot be compiled with a version of Agda readily available in your distribution of choice (e.g. because it uses syntax that was not available beforehand!) and it is forced to pull the latest version from github.

Installing Agda

If your library is compatible with a distributed version then it will be far simpler for you to simply pull it from the repositories via apt-get install agda.

Alternatively Scott Fleischman has a basic example on how to use a docker image to typecheck your development: https://github.com/scott-fleischman/agda-travis

Installing your dependencies

If your project relies on dependencies then you do need to install them. In practice it'll probably mean fetching a bunch of tarballs via wget, and having a ~/.agda/libraries pointing at their library files.

Cf. the manual on library management