Move agda2hs.agda-lib into lib directory and rename to base.agda-lib

[HeinrichApfelmus]

This pull request

• moves the agda2hs.agda-lib library and the associated source code into the lib/agda2hs directory, and
• renames the agda2hs.agda-lib library to base.agda-lib in order to mirror the Haskell base package.

The idea is that additional libraries, such as containers can be added to the lib/ directory in this repository. Such an arrangement makes sense as long as there is significant backflow of code from containers.agda-lib to base.agda-lib, and makes it easier to split out containers at a later point.

(EDIT: Accepted.
We may want to consider renaming the agda2hs.agda-lib to base.agda-lib, in order to match up with the Haskell base package.)

[jespercockx]

This looks like a sensible change to me. It's a bit of a pain that users have to update their libraries file, but there's not much we can do about that.

[jespercockx]

We may want to consider renaming the agda2hs.agda-lib to base.agda-lib, in order to match up with the Haskell base package.

Perhaps this is worth doing in one go so at least users only have to do a single update.

[HeinrichApfelmus]

We may want to consider renaming the agda2hs.agda-lib to base.agda-lib, in order to match up with the Haskell base package.

Perhaps this is worth doing in one go so at least users only have to do a single update.

Sure, I can change this pull request to also rename the library — I just wasn't quite sure whether people consider this a good idea.

For renaming, I see the following options:

1. agda2hs.agda-lib — current state of affairs.
2. base.agda-lib — matches the base package.
3. agda2hs-base.agda-lib — adds agda2hs as prefix in order to make the library stand out when accidentally mixed with other Agda libraries.

I think I prefer 2. 🤔

[omelkonian]

@HeinrichApfelmus I don't quite understand the monolithic approach of having containers in the same repo. Why not simply move this in the agda/agda2hs-containers repo?

That way, we retain the current configuration and name the library files like so:

• the main agda2hs codebase, containing base: agda2hs.agda-lib
• the containers package for agda2hs: agda2hs-containers.agda-lib
  A user who wants both base and containers, has to install both agda2hs and agda2hs-containers, which is slightly inconvenient but also consistent with what you would do in Haskell-land (i.e. add base and containers as Cabal dependencies).

[HeinrichApfelmus]

I don't quite understand the monolithic approach of having containers in the same repo. Why not simply move this in the agda/agda2hs-containers repo?

There are two slightly different questions here:

• Do we keep the base library separate from the containers library?
• If so, do we keep the base library in a separate repository from the containers library?

My impression was that we all agree that the answer to the first question is "yes" — the design principle being that we mirror the exact separation of libraries on the Haskell side.

The separation of libraries raises a small naming issue: Should we call the base library agda2hs.agda-lib, agda2hs-base.agda-lib or base.agda-lib? Should we call the containers library agda2hs-containers.agda-lib or containers.agda-lib? As we want the naming choice to scale to a large number of Haskell packages, I tend towards dropping the agda2hs- prefix and using the same name as the Haskell package, i.e. base.agda-lib and containers.agda-lib.

For the second question, I would argue that "no, for the time being". I see two arguments in favor of a monorepo for these two libraries:

• There is still significant backflow of code from containers to base. For example proving things about Data.Map.spanAntitone will require additions to Data.Ord. Developing them in separate repositories is painful.
• Having at least one library that is different from base in the repository informs the development of agda2hs. Any change to agda2hs will have to deal with the fact containers is there, that it's separate and that it's of considerable code size.

Note that these arguments do not address the question "what is the desired end state?", but the question "how do we get there?". Once base.agda-lib is reasonably complete, we can split out containers into a separate repository, as the backflow of code will slow to a trickle.

[omelkonian]

These are some excellent points for keeping containers in the base repo for the time being; let's revisit once we have a more stable ecosystem, in which case we should follow what Haskell does (i.e. put containers in a separate repo as in https://github.com/haskell/containers).

Onto library file naming. I am fine with dropping the agda2hs- prefix, since there is very little chance there will be a name collision with another (non-agda2hs-compliant) Agda library.

So, please go ahead with the renaming you initially suggested.

[omelkonian]

Reminder to check that these links still work and the documentation generating scripts do their job.

[HeinrichApfelmus]

I have now run make libHtml locally and found that my previous change did not yield the desired result. I have updated the change, it should now work — the result is still in the html directory without prefix.

[omelkonian]

Thanks Heinrich!