stack install Agda-2.6.3 picks lts (latest) which lacks Agda-2.6.3

[andreasabel]

Agda-2.6.3 is only on nightly yet. If I command

$ stack install Agda-2.6.3

it fails with a missing dependency in lts-20.13:

Writing implicit global project config file to: /home/runner/.stack/global-project/stack.yaml
Note: You can change the snapshot via the resolver field there.
Using latest snapshot resolver: lts-20.13
..
Error: [S-4804]
       Stack failed to construct a build plan.
       
       While constructing the build plan, Stack encountered the following errors:
       
       In the dependencies for Agda-2.6.3:
           vector-hashtables must match >=0.1 && <0.2, but the Stack configuration has no specified
                             version (latest matching version is 0.1.1.2)
       needed since Agda is a build target.

This is odd:

• stack should not have picked lts-20.13 because it does not even have Agda-2.6.3
• it should have picked latest nightly instead which does have Agda-2.6.3 and all its dependencies
• if stack insists on not using nightly unless forced to, it should have reported that Agda-2.6.3 is not in a LTS rather than going with a plan that will not lead to the end goal (installing Agda-2.6.3) and has no chance of succeeding

stack's behavior is like when you place an order for a BMW Z4 and then you get the reply that the BMW X1 isn't in stock.

In the wild: https://github.com/andreasabel/ipl/actions/runs/4391563244/jobs/7690803077#step:6:468

[mpilgrem]

@andreasabel, I think Stack is behaving as you would expect.

stack install Agda-2.6.3 is the equivalent of stack build Agda-2.6.3 --copy-bins. I assume that Agda-2.6.3 is not a local package, extra dep or snapshot, and so Stack will be using the version of Agda-2.6.3 from the package index (Hackage). (https://docs.haskellstack.org/en/stable/build_command/) The Agda-2.6.3 package on Hackage does not supply a stack.yaml file (https://hackage.haskell.org/package/Agda-2.6.3/src/). (EDIT: Even it it did, it would not be in the project folder, so Stack would not see it. (https://docs.haskellstack.org/en/stable/yaml_configuration/#yaml-configuration))

In terms of a snapshot, as it looks like there is no project-level YAML configuration file named stack.yaml in the folder or its ancestor folders, Stack is falling back on the stack.yaml in the global-project directory.

The global-project directory does not seem to exist on your system already, so Stack is creating it, and populating it by default with the most recent Stackage Haskell LTS snapshot (being LTS 20.13).

If you want to build Agda-2.6.3 with a different snapshot, you need to specify one - for example, by creating a stack-yaml in the folder or an ancestor folder or specifying a file on the command line. EDIT: stack --resolver nightly-2023-03-10 build Agda-2.6.3 worked on my system.

[mpilgrem]

Or, to view it another way, when you command stack build, Stack needs to know what project-level YAML configuration file to use. If you do not specify one, Stack, as a last resort, will look to the global-project directory. The fact that Agda-2.6.3 can be found in nightly-2023-03-10 does not allow Stack to guess that you want to specify nightly-2023-03-10 as the snapshot.

[andreasabel]

@mpilgrem: Thanks for you swift reply!

My motivation is that I would like to use stack like a package manager when installing an executable.

$PACKAGEMANAGER install $PACKAGE-$VERSION

This is the conventional syntax, known from apt, brew, cabal etc.

Usually hackage publications do not have a stack.yaml file. Such would be problematic, because it would be fixed at the time of publication. E.g. for Agda, this would just contain something like resolver: nightly-YYYY-MM-DD because at publication time, LTS resolvers are usually not available. Agda (an all other packages) enter LTS later. So, the better assignment of a resolver is dynamic, picked at time of installation, not at time of publication.

I follow your explanation of how stack resolves to a snapshot. However, I think the default could be improved. So, if no stack.yaml is available, stack install $PACKAGE-$VERSION should pick

1. the latest LTS that has version $VERSION of $PACKAGE,
2. if there is no such LTS, pick nightly if it has $VERSION.

Currently, I can work around this by

stack install Agda-2.6.3 --resolver nightly

but this is not a forward-compatible installation instruction: nightly might not have 2.6.3 in the future, it might be in lts instead.

A future-proof instruction would be, I suppose,

stack install Agda-2.6.3 --resolver nightly || stack install Agda-2.6.3 --resolver lts

however, this isn't very pretty.

[mpilgrem]

Currently, you would do this (EDIT: a more comprehensive version):

rmdir Agda-* -Force -Recurse # Tidy up any existing versions of Agda (PowerShell version)
stack unpack Agda # Will get the most recent version from Hackage (currently Agda-2.6.3)
cd Agda-* # Change to the downloaded package's directory (currently Agda-2.6.3)
stack init # This will identify snapshot nightly-2023-03-18 for the stack.yaml
stack install
cd ..
rmdir Agda-* -Force -Recurse # Tidy up (PowerShell version)

[mpilgrem]

I have extended the examples at https://docs.haskellstack.org/en/stable/build_command/#examples.

At the moment, if you command stack build outside of a project directory (with no stack.yaml in the current directory or an ancestor directory) you are, by definition, specifying that you want to use the stack.yaml in the global-project directory of the Stack root. I think that causing Stack to substitute (for that specification) a snapshot from some Stackage snapshot (which could change, as Stackage publishes snapshots) for target packages in the package index would be problematic - not least, for 'reproducibility'.

[andreasabel]

In practice, how useful is this global-project thing?
It seems to be blocking a standard interface to stack as a packet manager, so maybe it could be reevaluated.
Personally, I get the impression that Haskell was moving into the direction that every package defines its dependencies self, so maybe global-project is an anachronism?
Anyway, my impression is that a robust stack install PACKAGE that servers many users that need not know anything about stack is more useful than some small convenience for stack experts (such as not having to write the one line echo 'resolver: lts-19.33' > stack.yaml or stack init --resolver lts).

[mpilgrem]

It is usually the global-project that provides the project-specific configuration (especially snapshot, extra-deps and flags) when Stack is run outside of a project directory. The poster child for that would be running stack ghci.

Package description files (eg Cabal files or package.yaml) do define dependencies, but usually not uniquely. That is where Stack/Stackage step in: to provide curated lists of specific package versions that are known to work well together.

I think the point of departure between what you are suggesting and what Stack does is that stack install is just a synonym for stack build --copy-bins (and --copy-bins relates only to built executables, not built libraries); Stack is not aiming to manage built executables or libraries, just build them from source code in an efficient and reproducible way.

[andreasabel]

The poster child for that would be running stack ghci.

Ok, this seems to be the motivation for the global-project. Thanks for the explanation!

To me, it still seems that there is room for improvement of stack install EXTERNALPACKAGE-VERSION, but it seems like this would need a larger effort (like refining stack install so that it is not just a synonym for stack build --copy-bins). So it is just something for the wish list.

Moved the issue to the wishlist.