Submodules vs. copying specs into the repo

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities

Other

1.29k stars 200 forks source link

Submodules vs. copying specs into the repo #100

Closed ahelwer closed 10 months ago

ahelwer commented 10 months ago

Was briefly discussed earlier in the year but IMO it would be better to just copy the specs into the repo. Reasons:

Avoids link rot; on a long enough timescale this is basically guaranteed, especially as awareness grows that centralizing all FOSS development on github is not ideal and people switch to alternative software forge services. Even if we can backup from local copies, why deal with the hassle of having to detect that then rectify it?
Specs are small. It is a trivial amount of duplicated data. They are also not often updated after being published, so tracking a remote repo is not likely to bring much benefit.
Copying the files into this repo ensures they can be made amenable to validation by the CI workflow.

Thoughts? I will say that adding the specs as submodules is preferable to them only existing as a hyperlink though. One of the submodules added exposed a bug in tree-sitter-tlaplus pluscal parsing!

lemmy commented 10 months ago

I agree that copying specs should be the default. The reasons for introducing submodules for CCF, BlockingQueue, and AzureCosmosDB are:

CCF:

Under heavy development

BlockingQueue:

git repository (commit history) is part of the example

Azure Cosmos DB

Under development
git repository has supplementary material
git repository is in the tlaplus/ github org
git repository is linked from docs.microsoft.com

For posterity, we should consider setting up github mirroring to, e.g., Gitlab, our Inria machine, or to the Linux Foundation. IMO this should also include wiki pages and Github issues (I once looked into distributed issue trackers to avoid Github vendor lock-in, but they were too inconvenient to use).

AFAIK, the Github action/checkout can clone submodules. Would that help with the CI workflow validation?

ahelwer commented 10 months ago

You're right action/checkout can clone submodules. Involving submodules might complicate things if we can't massage the submodule module/model names & locations such that the manifest generation script will be able to recreate everything nicely. Or if people try to run manifest generation without having checked out submodules, although a step can be added to the instructions for that.