search

ualib / agda-algebras

The Agda Universal Algebra Library (html docs available at the url below)
https://ualib.github.io/agda-algebras/
Creative Commons Attribution Share Alike 4.0 International
29 stars 7 forks source link

reorganize repo to accommodate parallel setoid-based development #79

Closed williamdemeo closed 3 years ago

williamdemeo commented 3 years ago

I think it makes more sense to make the setoid stuff a truly parallel development and structure the repo as in this PR.

Whereas before we had

module1/submodule1.1.lagda
module1/submodule1.2.lagda
...

and then a big module1/Setoid.lagda module with the setoid versions of all the submodules combined into one file.

now we will have

module1/submodule1.1.lagda
module1/submodule1.2.lagda
...

for the non-setoid versions and

module1/Setoid/submodule1.1.lagda
module1/Setoid/submodule1.2.lagda
...

for the setoid-based versions.

Apart from this reorganization, the only other thing this PR does is remove some unnecessary imports from some modules.

williamdemeo commented 3 years ago

I want to merge these organization changes before my other work gets too far out of sync... sorry!

JacquesCarette commented 3 years ago

No problem!

BTW, do you know about git mv? That's the best way to do renames so that the history is preserved.

williamdemeo commented 3 years ago

Yes, thanks. I try to do git mv, but sometimes when I'm renaming lots of things, one or two might get lost.

Of course, the history is preserved somewhere, but you're absolutely right, it's better if the history is preserved and attached to the (newly renamed) file.

Thanks!

On Sun, Jul 18, 2021 at 8:03 PM Jacques Carette @.***> wrote:

No problem!

BTW, do you know about git mv? That's the best way to do renames so that the history is preserved.

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/ualib/agda-algebras/pull/79#issuecomment-882095915, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA25MJCP3IGLFBTIO6BCH73TYMJPLANCNFSM5ARMY3MQ .