Installing development version with cabal

[mikeshulman]

I think would be useful if the installation documentation mentioned that it is also possible to install the development version of Agda with cabal install instead of make install, and what the differences are between those approaches. In particular, using Cabal permits the use of program-suffix to have multiple development versions installed at once. (Yes, I really do want to do that -- in one project I need to be on the bleeding edge with fixes like a18ed8a, but the project my students are currently working on only works in between 02cd13a and a569b16, and I want to be able to make incremental fixes to their library without redesigning it and forcing them to compile a new Agda.)

[andreasabel]

I typically do make v1-install which isn't much more than a cabal v1-install. In fact, it expands to cabal v1-install --disable-documentation -j1 --disable-library-profiling -fenable-cluster-counting --ghc-options="+RTS -A128M -M10G -RTS" --enable-tests --builddir=./dist-2.6.3-ghc-9.4.1 --program-suffix=-2.6.3. Keeping the essential, you could

cabal v1-install -fenable-cluster-counting --program-suffix=-2.6.3

but even plain cabal v1-install should produce something reasonable (without ICU). In the same way, cabal install should work fine (I never use it though).

The docs could mention cabal install with options -fenable-cluster-counting, --ghc-options="+RTS -A128M -M10G -RTS" (or similar, for compilation speedup) and --program-suffix=....

[mikeshulman]

Plain cabal install --program-suffix=... worked fine for me, although one difference I noticed relative to make install is that agda-program-suffix --version no longer includes the commit hash.

[gallais]

In particular, using Cabal permits the use of program-suffix to have multiple development versions installed at once.

Looking at the Makefile (the default target is install-bin), there is already the automatic addition of --program-suffix if you're compiling with cabal and what looks like an ad-hoc solution if you're using stack (that's the call to $(MAKE) copy-bins-with-suffix$(AGDA_BIN_SUFFIX). Does stack not support program suffixes?).

https://github.com/agda/agda/blob/b52180812845647b57ca3cfbd5d03f68d6f8e802/Makefile#L164-L176

It'd be interesting to track down why that did not work in your case.

[andreasabel]

one difference I noticed relative to make install is that agda-program-suffix --version no longer includes the commit hash.

Maybe because this part of the Makefile is then not run:

ensure-hash-is-correct:
	touch src/full/Agda/VersionCommit.hs

[mikeshulman]

It'd be interesting to track down why that did not work in your case.

make install does automatically add a program-suffix of -2.6.3. But two different commits on the development branch both add this same suffix, so this automatic suffix doesn't suffice to distinguish them. I guess I could edit the Makefile directly to set AGDA_BIN_SUFFIX to something else...

[nad]

Perhaps the problem can be fixed by moving the touch src/full/Agda/VersionCommit.hs hack to Setup.hs. In that case care should be taken to ensure that the hack works on all supported platforms.

[nad]

The touch hack does not seem to work very well when GHC 9.4.2 is used. My guess is that GHC is now better at avoiding recompilation.

An alternative is perhaps to generate Agda.VersionCommit using Setup.hs.

[nad]

A discussion about this kind of thing.