Rename unstable throughout codebase to trunk

Closes #1012

The trunk of our development has been called `unstable` for a long time.
This is a holdover from before we adopted a trunk-based development
model, and from before we had CI/CD running for the trunk. Now, the
trunk is really not very unstable, and stability is given by versioned
releases, rather than by maintaining long-lived branches in parallel.

After this change, we should be able to reconfigure the default branch.

.github/pull_request_template.md

@@ -5,4 +5,4 @@
 - [ ] Documentation added for any new functionality
 - [ ] Entries added to [./unreleased/][unreleased] for any new functionality
 
-[unreleased]: https://github.com/informalsystems/apalache/tree/unstable/.unreleased
+[unreleased]: https://github.com/informalsystems/apalache/tree/trunk/.unreleased

.github/workflows/README.md

@@ -2,12 +2,12 @@
 
 ## [./main.yml](./main.yml)
 
-- Triggered on pull requests into `unstable`.
+- Triggered on pull requests into `trunk`.
 - Our primary build and test workflow.
 
 ## [./deploy.yml](./deploy.yml)
 
-- Triggered by pull requests into `unstable`.
+- Triggered by pull requests into `trunk`.
 - Used for any artifacts that we deploy into production environments. Currently,
   this only consists of our website at https://apalache.informal.systems.
 
@@ -35,6 +35,6 @@
 
 ## [./container.yml](./container.yml)
 
-- Triggered by publishing releases or merging into the `unstable` branch
+- Triggered by publishing releases or merging into the `trunk` branch
 - The workflow builds the docker container defined in the
   [`/Dockerfile`](../../Dockerfile) and publishes it to GitHub Packages.

.github/workflows/auto-update.yml

@@ -6,7 +6,7 @@ name: Auto-update
 on:
   push:
     branches:
-      - unstable
+      - trunk
 
 jobs:
   Auto:

.github/workflows/container.yml

@@ -1,5 +1,5 @@
 # This workflow builds and publishes a docker container to the GitHub registry.
-# It is only triggered on merges into the unstable branch, and we assume that
+# It is only triggered on merges into the trunk branch, and we assume that
 # any commit merged into the trunk has passed CI is safe to release.
 
 # Adapted from https://docs.github.com/en/actions/publishing-packages/publishing-docker-images#publishing-images-to-github-packages
@@ -12,7 +12,7 @@ on:
       - published
   push:
     branches:
-      - unstable
+      - trunk
 
 env:
   REGISTRY: ghcr.io
@@ -38,7 +38,7 @@ jobs:
 
       # See https://github.com/docker/metadata-action#tags-input for the default
       # tags that are extracted this way. It includes tags for semver releases
-      # and any branches into unstable
+      # and any branches into trunk
       - name: Extract metadata (tags, labels) for Docker
         id: meta
         uses: docker/metadata-action@98669ae865ea3cffbcbaa878cf57c20bbf1c6c38

.github/workflows/deploy.yml

@@ -3,9 +3,7 @@ name: deploy
 on:
   push:
     branches:
-      - master
-      # TODO Remove once deploying unstable versions separately
-      - unstable
+      - trunk
 
 jobs:
   deploy:

.github/workflows/main.yml

@@ -7,7 +7,7 @@ on:
   #  See https://git.luolix.topmunity/t/actions-cache-cache-not-being-hit-despite-of-being-present/17956/3
   push:
     branches:
-      - unstable
+      - trunk
 
 name: build
 

.github/workflows/release.yml

@@ -2,7 +2,7 @@ name: release
 
 on:
   pull_request:
-    branches: [unstable]
+    branches: [trunk]
     types: [closed]
 
 jobs:

CHANGES.md

@@ -932,13 +932,13 @@
 
  * speed up by using constants instead of uninterpreted functions
 
- * options for fine tuning with `--fine-tuning`, see [tuning](https://github.com/informalsystems/apalache/blob/unstable/docs/src/apalache/tuning.md)
+ * options for fine tuning with `--fine-tuning`, see [tuning](https://github.com/informalsystems/apalache/blob/trunk/docs/src/apalache/tuning.md)
 
  * bugfix in logback configuration
 
 ## 0.4.0-pre1
 
- * type annotations and very simple type inference, see the [notes](https://github.com/informalsystems/apalache/blob/unstable/docs/src/apalache/types-and-annotations.md)
+ * type annotations and very simple type inference, see the [notes](https://github.com/informalsystems/apalache/blob/trunk/docs/src/apalache/types-and-annotations.md)
 
  * a dramatic speed up of many operators by using a `QF_NIA` theory and cherry pick
 

CONTRIBUTING.md

@@ -91,7 +91,7 @@ to [.github/CODEOWNERS](.github/CODEOWNERS).
 
 Sometimes a contributor wants to ensure that they have a chance to review a
 [pull request](#making-a-pull-request) before the changes are landed in
-`unstable`. Contributors can lock the PR to prevent it from being merged before
+`trunk`. Contributors can lock the PR to prevent it from being merged before
 they can complete a review by leaving an empty review on the PR, requesting
 changes, along with a note like:
 
@@ -125,11 +125,11 @@ of landing changes:
 
 ## Making a pull request
 
-We develop on the `unstable` branch and practice [trunk-based
+We develop on the `trunk` branch and practice [trunk-based
 development](https://trunkbaseddevelopment.com/).
 
 Nontrivial changes should start with a [draft pull request][] against
-`unstable`. The draft signals that work is underway. When the work is ready for
+`trunk`. The draft signals that work is underway. When the work is ready for
 feedback, hitting "Ready for Review" will signal to the maintainers that you are
 ready for them to take a look.
 
@@ -142,7 +142,7 @@ Each stage of the process is aimed at creating feedback cycles which align
 contributors and maintainers to make sure:
 
 - Contributors don’t waste their time implementing/proposing features which
-  won’t land in `unstable`.
+  won’t land in `trunk`.
 - Maintainers have the necessary context in order to support and review
   contributions.
 
@@ -471,14 +471,14 @@ The process proceeds in two steps:
 Assuming the current version recorded in the project's `VERSION` file is
 `l.m.n-SNAPSHOT`, the manual release process is as follows:
 
-- [ ] `git checkout unstable && git pull`
+- [ ] `git checkout trunk && git pull`
 - [ ] Run `./script/release-prepare.sh` to
   - create and checkout a branch `release/l.m.n`.
   - prepare and add a release commit `[release] l.m.n`
   - update the changelog
   - bump the version number
   - commit the changes
-  - opens a pr into `unstable` with the title `[release] l.m.n`.
+  - opens a pr into `trunk` with the title `[release] l.m.n`.
 - [ ] Get the PR reviewed and merged and **DO NOT SQUASH THE CHANGES** on merge.
 
 If you need to set a specific version (e.g., to increment to a major version),
@@ -490,9 +490,9 @@ RELEASE_VERSION=l.m.n ./script/release-prepare.sh
 
 #### Cut the release
 
-When the PR is merged into `unstable`:
+When the PR is merged into `trunk`:
 
-- [ ] Checkout the `[release] l.m.n` commit from the latest `unstable`
+- [ ] Checkout the `[release] l.m.n` commit from the latest `trunk`
 - [ ] Run `./script/release-publish.sh` to
   - tag the release commit
   - package the

COORDINATION.md

@@ -37,7 +37,7 @@ shared understanding of how to use and interpret the main features:
 (For more on projects vs. milestones, see
 https://stackoverflow.com/a/47542346/1187277)
 
-[adr and rfc]: https://github.com/informalsystems/apalache/tree/unstable/docs/src/adr
+[adr and rfc]: https://github.com/informalsystems/apalache/tree/trunk/docs/src/adr
 [discussion]: https://github.com/informalsystems/apalache/discussions
 [issues]: https://github.com/informalsystems/apalache/issues
 [labels]: https://github.com/informalsystems/apalache/issues/labels
@@ -109,7 +109,7 @@ nothing is a priority".
 
 We use a modified action-priority matrix. Our prioritization process is
 recorded in
-[RFC-21](https://github.com/informalsystems/apalache/blob/unstable/docs/src/adr/021rfc-prioritization.md)
+[RFC-21](https://github.com/informalsystems/apalache/blob/trunk/docs/src/adr/021rfc-prioritization.md)
 
 ### Milestones
 

README.md

@@ -9,10 +9,10 @@ alt="Apalache Logo">
 
 </div>
 
-[![unstable badge][]][unstable-ci]
+[![trunk badge][]][trunk-ci]
 
-[unstable badge]: https://github.com/informalsystems/apalache/workflows/build/badge.svg?branch=unstable
-[unstable-ci]: https://github.com/informalsystems/apalache/actions?query=branch%3Aunstable+workflow%3Abuild
+[trunk badge]: https://github.com/informalsystems/apalache/workflows/build/badge.svg?branch=trunk
+[trunk-ci]: https://github.com/informalsystems/apalache/actions?query=branch%3Atrunk+workflow%3Abuild
 
 Apalache translates [TLA+] into the logic supported by SMT solvers such as
 [Microsoft Z3]. Apalache can check inductive invariants (for fixed or bounded
@@ -28,11 +28,11 @@ course].
 Check the [releases page][] for our latest release.
 
 For a stable release, we recommend that you pull the latest docker image with
-`docker pull ghcr.io/informalsystems/apalache:unstable`, use the jar from the
+`docker pull ghcr.io/informalsystems/apalache:trunk`, use the jar from the
 most recent release, or checkout the source code from the most recent release
 tag.
 
-To try the latest cool features, check out the head of the [unstable branch][].
+To try the latest cool features, check out the head of the [trunk branch][].
 
 For more information on installation options, see [the
 manual][user-manual-installation].
@@ -144,7 +144,7 @@ Past funding from [Der Wiener Wissenschafts-, Forschungs- und Technologiefonds](
 [video course]: http://lamport.azurewebsites.net/video/videos.html
 [releases page]: https://github.com/informalsystems/apalache/releases
 [master]: https://github.com/informalsystems/apalache/tree/master
-[unstable branch]: https://github.com/informalsystems/apalache/tree/unstable
+[trunk branch]: https://github.com/informalsystems/apalache/tree/trunk
 [apalache zulip stream]: https://informal-systems.zulipchat.com/#narrow/stream/265309-apalache
 [tendermint specs]: https://github.com/tendermint/tendermint/tree/master/spec/light-client/accountability
 [tendermint blockchain]: https://github.com/tendermint

build.sbt

@@ -76,7 +76,7 @@ ThisBuild / scalacOptions ++= {
 // scalafmt
 // TODO: Remove if we decide we are happy with allways reformatting all
 // Only check/fix against (tracked) files that have changed relative to the trunk
-// ThisBuild / scalafmtFilter := "diff-ref=origin/unstable"
+// ThisBuild / scalafmtFilter := "diff-ref=origin/trunk"
 ThisBuild / scalafmtPrintDiff := true
 
 // scalafix

docs/highlightjs-tlaplus/package.json

@@ -14,7 +14,7 @@
   "bugs": {
     "url": "https://github.com/informalsystems/apalache/issues"
   },
-  "homepage": "https://github.com/informalsystems/apalache/tree/unstable/docs/highlightjs-tlaplus",
+  "homepage": "https://github.com/informalsystems/apalache/tree/trunk/docs/highlightjs-tlaplus",
   "devDependencies": {
     "highlight.js": "^11.5.1"
   }

docs/src/HOWTOs/howto-write-type-annotations.md

@@ -504,7 +504,7 @@ This may change later, when the tlaplus [Issue 578][] is resolved.
 
 
 [old type annotations]: ../apalache/types-and-annotations.md
-[Apalache.tla]: https://github.com/informalsystems/apalache/blob/unstable/src/tla/Apalache.tla
+[Apalache.tla]: https://github.com/informalsystems/apalache/blob/trunk/src/tla/Apalache.tla
 [Snowcat]: ../apalache/typechecker-snowcat.md
 [ADR002]: ../adr/002adr-types.md
 [HourClock.tla]: https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/RealTime/HourClock.tla
@@ -518,7 +518,7 @@ This may change later, when the tlaplus [Issue 578][] is resolved.
 [Issue 578]: https://github.com/tlaplus/tlaplus/issues/578
 [Issue 718]: https://github.com/informalsystems/apalache/issues/718
 [MissionariesAndCannibals.tla]: https://github.com/tlaplus/Examples/blob/master/specifications/MissionariesAndCannibals/MissionariesAndCannibals.tla
-[Variants module]: https://github.com/informalsystems/apalache/blob/unstable/src/tla/Variants.tla
+[Variants module]: https://github.com/informalsystems/apalache/blob/trunk/src/tla/Variants.tla
 [Chapter on variants]: ../lang/variants.md
 [Idiom 3]: ../idiomatic/003record-sets.md
 [LamportMutex.tla]: https://github.com/tlaplus/Examples/blob/master/specifications/lamport_mutex/LamportMutex.tla

docs/src/adr/002adr-types.md

@@ -549,8 +549,8 @@ AtMostOne ==
 
 [Snowcat tutorial]: https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html
 [Snowcat HOWTO]: https://apalache.informal.systems/docs/HOWTOs/howto-write-type-annotations.html
-[ADR014]: https://github.com/informalsystems/apalache/blob/unstable/docs/src/adr/014adr-precise-records.md
+[ADR014]: https://github.com/informalsystems/apalache/blob/trunk/docs/src/adr/014adr-precise-records.md
 [Issue 401]: https://github.com/informalsystems/apalache/issues/401
 [Row polymorphism]: https://en.wikipedia.org/wiki/Row_polymorphism
-[Variants.tla]: https://github.com/informalsystems/apalache/blob/unstable/src/tla/Variants.tla
+[Variants.tla]: https://github.com/informalsystems/apalache/blob/trunk/src/tla/Variants.tla
 [variant types]: https://en.wikipedia.org/wiki/Tagged_union

docs/src/adr/004adr-annotations.md

@@ -163,5 +163,5 @@ so it would be otherwise impossible to find the end of an annotation.
 
 [Java identifier]: https://docs.oracle.com/javase/specs/jls/se7/html/jls-3.html#jls-3.8
 
-[AnnotationParser]: https://github.com/informalsystems/apalache/blob/unstable/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/AnnotationParser.scala
+[AnnotationParser]: https://github.com/informalsystems/apalache/blob/trunk/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/AnnotationParser.scala
 

docs/src/adr/005adr-json.md

@@ -205,7 +205,7 @@ The implementation of the serialization can be found in the class
 
 [ADR-004]: https://apalache.informal.systems/docs/adr/004adr-annotations.html
 
-[TlaToJson]: https://github.com/informalsystems/apalache/blob/unstable/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala#L54
-[TlaEx]: https://github.com/informalsystems/apalache/blob/unstable/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaEx.scala#L10
-[TlaDecl]: https://github.com/informalsystems/apalache/blob/unstable/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDecl.scala#L9
-[TlaModule]: https://github.com/informalsystems/apalache/blob/unstable/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDecl.scala#L19
+[TlaToJson]: https://github.com/informalsystems/apalache/blob/trunk/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala#L54
+[TlaEx]: https://github.com/informalsystems/apalache/blob/trunk/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaEx.scala#L10
+[TlaDecl]: https://github.com/informalsystems/apalache/blob/trunk/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDecl.scala#L9
+[TlaModule]: https://github.com/informalsystems/apalache/blob/trunk/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDecl.scala#L19

docs/src/adr/006rfc-unit-testing.md

@@ -634,7 +634,7 @@ Let us know:
 [Property-based testing]: https://en.wikipedia.org/wiki/QuickCheck
 [TLA+ examples]: https://github.com/tlaplus/Examples/
 [LCR]: https://github.com/tlaplus/Examples/tree/master/specifications/chang_roberts
-[ChangRobertsTyped_Test.tla]: https://github.com/informalsystems/apalache/blob/unstable/test/tla/ChangRobertsTyped_Test.tla
+[ChangRobertsTyped_Test.tla]: https://github.com/informalsystems/apalache/blob/trunk/test/tla/ChangRobertsTyped_Test.tla
 [Distributed Algorithms]: https://dl.acm.org/doi/book/10.5555/2821576
 [Raft]: https://github.com/tlaplus/Examples/tree/master/specifications/raft
 [Apalache.tla]: https://github.com/informalsystems/apalache/blob/80cf914fe7272b14832a47b21193f5dfe8119348/src/tla/Apalache.tla

docs/src/adr/010rfc-transition-explorer.md

@@ -153,7 +153,7 @@ I propose the following high-level architecture:
 *NOTE*: The high-level sketch above assumes the new code organization proposed
 in [ADR 7][].
 
-[ADR 7]: https://github.com/informalsystems/apalache/tree/unstable/docs/src/adr/007adr-restructuring.md
+[ADR 7]: https://github.com/informalsystems/apalache/tree/trunk/docs/src/adr/007adr-restructuring.md
 
 #### API
 
@@ -170,7 +170,7 @@ with `Example`.
 
 In essence, this proposed API is only a thin wrapper around the
 [TransitionExecutor
-class](https://github.com/informalsystems/apalache/tree/unstable/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutor.scala).
+class](https://github.com/informalsystems/apalache/tree/trunk/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutor.scala).
 During previous iterations of the proposed API we discussed exposing a
 higher-level API, targeted at meeting the requirements more directly.  However,
 discussion revealed that the expensive computational costs of SAT solving in

docs/src/adr/015adr-trace.md

@@ -446,6 +446,6 @@ Reserved for the future.
 
 
 [ADR005]: https://apalache.informal.systems/docs/adr/005adr-json.html
-[MissionariesAndCannibalsTyped]: https://github.com/informalsystems/apalache/blob/unstable/test/tla/MissionariesAndCannibalsTyped.tla
+[MissionariesAndCannibalsTyped]: https://github.com/informalsystems/apalache/blob/trunk/test/tla/MissionariesAndCannibalsTyped.tla
 [JSON]: https://en.wikipedia.org/wiki/JSON
 [RFC7159]: https://datatracker.ietf.org/doc/html/rfc7159.html

docs/src/apalache/assignments-in-depth.md

@@ -75,7 +75,7 @@ that has one of the following forms:
 - `x' = e`,
 - `x' \in S`,
 - `UNCHANGED x`, or
-- `x' := e` (note that `:=` is the operator defined in [Apalache.tla](https://github.com/informalsystems/apalache/blob/unstable/src/tla/Apalache.tla))
+- `x' := e` (note that `:=` is the operator defined in [Apalache.tla](https://github.com/informalsystems/apalache/blob/trunk/src/tla/Apalache.tla))
 
 So to reformulate the second requirement: the transition operator must contain
 at least one assignment candidate for each variable declared in the

docs/src/apalache/example.md

@@ -2,7 +2,7 @@
 
 We introduce a TLA+ specification that we use to discuss features of Apalache in
 the following sections. Its source code can be found in
-[`test/tla/y2k.tla`](https://github.com/informalsystems/apalache/blob/unstable/test/tla/y2k.tla):
+[`test/tla/y2k.tla`](https://github.com/informalsystems/apalache/blob/trunk/test/tla/y2k.tla):
 
 ```tla
 {{#include ../../../test/tla/y2k.tla::55}}