Should ghcup config add-release-channel build a set rather than a list?

[andreasabel]

Should ghcup config add-release-channel build a set rather than a list, or at least a nublist (if order matters)?

After hitting ghcup config add-release-channel ... twice, I am seeing:

$ ghcup config 
...
url-source:
  AddSource:
  - Right: https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-prereleases-0.0.7.yaml
  - Right: https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-prereleases-0.0.7.yaml
...

[hasufell]

Order matters.

What wold be the expected behavior for:

• add channel A
• add channel B
• add channel A

Will we remove the first or last A?

[andreasabel]

Will we remove the first or last A?

Either one, depending in which order ghcup tries these channels. Pruning one of the As need to be done so that the behavior is unaffected.

Does add-release-channel have effects other than adding the given URL to the channel list?

[hasufell]

They are tried in order. So which one gets removed?

[andreasabel]

Is this a quiz or what? I am the professor here!

[hasufell]

Is this a quiz or what? I am the professor here!

I'm saying I have no idea what the expected behavior is.

So this can't be done, unless we figure that out and have a precise specification how it's supposed to work.

Order matters

[hasufell]

Any new insights?

[andreasabel]

Well, I would have to understand the code how the release-channels are used once they are added. This should determine their semantics.

I am very puzzled about this interaction, it seems you just don't know the semantics of release channel collections. At the same time, I assumed you wrote ghcup mostly single-handedly. But as I said, I have no insight into the code. Maybe this release channel collection is just shipped off to some third party tool that does not give away the semantics either.

In any case, if order matters, I don't understand the current specs:

Usage: ghcup config add-release-channel URI

  Add a release channel from a URI

If order matters, "Add" is an unspecified operation. You would have to say where it is added: at the front, at the end, in alphabetical order, etc.

But this said, you might have more important things to look after. I just stumbled over it and thought I bring attention to it.

My curiosity came from haskell/actions/setup. Due to working on this, I might have to learn more things about ghcup in time. But the current issue is not pressing, so feel free to ignore it

[hasufell]

Well, I would have to understand the code how the release-channels are used once they are added.

ghcup-hs/lib/GHCup/Download.hs

Lines 133 to 141 in 31e83ca

	mergeGhcupInfo :: MonadFail m
	=> [GHCupInfo]
	-> m GHCupInfo
	mergeGhcupInfo [] = fail "mergeGhcupInfo: internal error: need at least one GHCupInfo"
	mergeGhcupInfo xs@(GHCupInfo{}: _) =
	let newDownloads = M.unionsWith (M.unionWith (\_ b2 -> b2)) (_ghcupDownloads <$> xs)
	newGlobalTools = M.unionsWith (\_ a2 -> a2 ) (_globalTools <$> xs)
	newToolReqs = M.unionsWith (M.unionWith (\_ b2 -> b2)) (_toolRequirements <$> xs)
	in pure $ GHCupInfo newToolReqs newDownloads newGlobalTools

I am very puzzled about this interaction, it seems you just don't know the semantics of release channel collections.

I'm puzzled how you came to this conclusion.

I asked you what you think the expected semantics are. You were unable to hash out what they are. Which I'm unable too.

I explained to you that currently order matters. See the code above.

At the same time, I assumed you wrote ghcup mostly single-handedly.

https://github.com/haskell/ghcup-hs/graphs/contributors

If order matters, "Add" is an unspecified operation. You would have to say where it is added: at the front, at the end, in alphabetical order, etc.

It is append.

[andreasabel]

I asked you what you think the expected semantics are.

Ok, if you ask me like this: I expect "later overwrites earlier". This is LIFO (stack). So adding A,B,A is the same as adding B,A.

[hasufell]

I asked you what you think the expected semantics are.

Ok, if you ask me like this: I expect "later overwrites earlier". This is LIFO (stack). So adding A,B,A is the same as adding B,A.

Overwrites what?

[andreasabel]

Mmh, no progress, so let me switch to mathematical language:

My model is that of the ghcup configuration being a state s and configuration commands being actions a applied to the state, with the action written s.a producing a new state. The actions form naturally a (non-commutative) monoid with concatenation also written a.b. Welldefinedness of the actions gives associativity (s.a).b = s.(a.b), so we can drop parenthesis.

We shall also consider ghcup commands c which act on a world w (state of your machine in terms of which ghc etc is installed and available). Such commands are also dependent on the ghcup configuration s, so their semantics is a function State -> World -> World.

We consider extensional equality of states, so two states are equal if they lead to equal results if involved in the same ghcup command in any kind of world. "Equal results" are not equal worlds but predicates Q on the world, e.g. "GHC 9.2.5 is installed and operational". We also need some preconditions P to hold on the world. So, more precisely, a command c would be denoting a function (s : State) -> {w : World | P_c(w)) -> {w : World | Q_c(w)}. Two states s and s' are equal it forall c, w. P_c(w) => Q_c(c(s,w)) iff Q_c(c(s',w)).

We are now interested in the question whether there is a non-trivial quotient on configuration action sequences xs. This quotient is defined by xs ~ xs' iff forall s. s.xs = s.xs'. In particular I wonder whether, given a is ghcup config add-release-channel foo, is it true that xs.a.ys.a ~ xs.ys.a for all xs and ys?

If this is the case, then the current representation of states s isn't canonical (meaning extensionally equal states may have different representation). Why I am not striving for full canonicity, I am asking whether the representation of states can be made more canoncial so that in particular s.a.b.a and s.b.a have the same representation.

[hasufell]

I don't care about the maths.

This is a simple question: what is overwritten?

There are multiple ways to do this with wide ranging consequences.

The ghcup metadata are nested maps:

ghcup-hs/lib/GHCup/Types.hs

Lines 103 to 109 in 31e83ca

	-- | Description of all binary and source downloads. This is a tree
	-- of nested maps.
	type GHCupDownloads = Map Tool ToolVersionSpec
	type ToolVersionSpec = Map Version VersionInfo
	type ArchitectureSpec = Map Architecture PlatformSpec
	type PlatformSpec = Map Platform PlatformVersionSpec
	type PlatformVersionSpec = Map (Maybe VersionRange) DownloadInfo

1. do we overwrite the tool?
2. or the version (that's the current behavior)
3. or the platform?
4. etc.

If we do e.g. 1, the pre-release channel would have to duplicate the base channel otherwise it would drop all non-prerelease versions.

Overwriting versions (2.) is somewhat similar to how e.g. gentoo overlays work.

[hasufell]

I'm inclined to error out on duplicates.

The user can supply --force then, which will a) remove the existing element from the list and b) append it again.

[hasufell]

done

[hasufell]

Released in https://github.com/haskell/ghcup-hs/releases/tag/v0.1.19.1

[andreasabel]

Great, thanks!

[hasufell]

Not sure we settled the maths though 😂

[andreasabel]

Another time...