search

lostbearlabs / tiny-tlaplus-examples

Very small examples of TLA+ features.
The Unlicense
43 stars 1 forks source link

Rename repo "tlaplus" to "pluscal" #1

Open lemmy opened 5 years ago

lemmy commented 5 years ago

The more examples the better but for the sake of consistency, I'd suggest to rename the repo and generally change the wording from "tlaplus" to "pluscal".

lostbearlabs commented 5 years ago

@lemmy, what would you think of clarifying this in the README instead? I think the typical consumer of these examples (for example, me 6 months ago) would be searching google or github for "tlaplus" rather than "pluscal". I'm sure it drives the experts crazy, but for many more casual users this is going to be a distinction without a difference.

Also, there is one example that is not pluscal and there could be more later: https://github.com/lostbearlabs/tiny-tlaplus-examples/blob/master/simple-logic/SimpleLogic.tla

Perhaps some verbiage at the top and an additional tag or pair of tags like "#pluscal" and "#tlaplus" to categorize the examples?

lemmy commented 5 years ago

May I ask why you didn't choose to contribute your examples to the "official" Example project?

lostbearlabs commented 5 years ago

@lemmy, as I mentioned in my post to the google group, I would be willing to consider that. The official examples are all more complex and I don't know the community yet, so I was concerned that (1) these might be too simplistic for that repo, (2) a new learner might benefit more from having a bunch of tiny things in one place where they won't suddenly stumble across Paxos, and (3) somebody getting on their feet might benefit from the github-friendly documentation-in-markdown structure I adopted here rather than the documentation-in-the-spec that is more usual. Considering that, would you recommend I submit these in a PR? If so, how should they best be organized?

lemmy commented 5 years ago

We have always wanted to have more beginner friendly examples in the repo!

I would suggest to contribute your examples into a single sub-directory under specifications/ with some descriptive name ("tiny"/"snippets"/...). Ideally you would "tag" each spec so we can eventually move forward with https://github.com/tlaplus/Examples/issues/8.

I'd also suggest to duplicate the markdown documentation to "documentation-in-the-spec" to make the examples consumable off-line.

lostbearlabs commented 5 years ago

Thanks for the suggestions. I'll put that pull request together as soon as I can find a little free time.