Merge branch 'main' into th/flush-logs

.git-blame-ignore-revs

@@ -6,3 +6,6 @@
 
 # Scala Steward: Reformat with scalafmt 3.7.6
 1b2091c13571348b534076f2183ced2cd2ff67a9
+
+# Scala Steward: Reformat with scalafmt 3.8.3
+60dd752b3c25a2b578b9f0a967878904d6941982

.github/workflows/README.md

@@ -9,22 +9,22 @@
 
 - Triggered by pull requests into `main`.
 - Used for any artifacts that we deploy into production environments. Currently,
-  this only consists of our website at https://apalache.informal.systems.
+  this only consists of our website at https://apalache-mc.org.
 
 ## [./prepare-release.yml](./prepare-release.yml)
 
 - Triggered manually.
 - The workflow prepares a release and opens a `[release]` PR.
 - **Requirements**:
-  - A personal API token is required to authenticate the API call that opens the
-    PR.
-    - We use a token belonging to our machine user [@apalache-bot][]. apalache-bot
+  - A personal API token called `APALACHE_BOT_TOKEN` is required to authenticate the API
+    call that opens the PR.
+    - We use a token belonging to our machine user [@coffeeinprogress][]. coffeeinprogress
       creates the PR from their fork of the repo, and they have no permissions in
       this repo itself.
     - Secrets are configured [here][secret-config].
 
-[@apalache-bot]: https://github.com/apalache-bot
-[secret-config]: https://github.com/informalsystems/apalache/settings/secrets/actions
+[@@coffeeinprogress]: https://github.com/coffeeinprogress
+[secret-config]: https://github.com/apalache-mc/apalache/settings/secrets/actions
 
 ## [./release.yml](./release.yml)
 

.github/workflows/main.yml

@@ -101,12 +101,7 @@ jobs:
         # See https://docs.github.com/en/actions/using-workflows/workflow-commands-for-github-actions#setting-an-environment-variable
         run: echo "APALACHE_HOME=$GITHUB_WORKSPACE" >> $GITHUB_ENV
       - name: Build and Unit Test
-        run: make test-coverage
-      - name: Upload coverage to Codecov
-        uses: codecov/codecov-action@v2
-        with:
-          # See https://app.codecov.io/gh/informalsystems/apalache/
-          token: ${{ secrets.CODECOV_TOKEN }} # not required for public repos
+        run: make test
       - name: Cleanup before cache
         # See https://www.scala-sbt.org/1.x/docs/GitHub-Actions-with-sbt.html#Caching
         shell: bash

.github/workflows/prepare-release.yml

@@ -3,7 +3,7 @@ name: prepare-release
 on:
   workflow_dispatch:
     # Allows manually triggering release via
-    # https://github.com/informalsystems/apalache/actions?query=workflow%3A%22Prepare+Release%22
+    # https://github.com/apalache-mc/apalache/actions?query=workflow%3A%22Prepare+Release%22
     inputs:
       release_version:
         description: "Version (leave empty to increment patch version)"
@@ -12,7 +12,7 @@ on:
 
 jobs:
   prepare-release:
-    if: github.repository_owner == 'informalsystems'
+    if: github.repository_owner == 'apalache-mc'
     env:
       RELEASE_VERSION: ${{ github.event.inputs.release_version }}
       # NOTE: We must not use the default GITHUB_TOKEN for auth here,

.scalafmt.conf

@@ -1,4 +1,4 @@
-version = "3.8.0"
+version = "3.8.3"
 
 runner.dialect = scala213
 fileOverride {

CHANGES.md

@@ -1,6 +1,24 @@
 <!-- NOTE: This file is generated. Do not write release notes here.
  Notes for unreleased changes go in the .unreleased/ directory. -->
 
+## 0.45.3 - 2024-08-21
+
+### Features
+
+- Added scope-unsafe builder.
+
+## 0.45.2 - 2024-08-19
+
+## 0.45.1 - 2024-08-19
+
+## 0.45.0 - 2024-08-17
+
+### Features
+
+- Handle expressions such as  S \in SUBSET [ a : Int ]  by rewriting the expression into  \A r \in S: DOMAIN r = {"a"} /\ r.a \in Int
+- Translate Quint's generate into `Apalache!Gen` (#2916)
+- Add `--timeout-smt` to limit SMT queries (#2936)
+
 ## 0.44.11 - 2024-05-06
 
 ### Features

FUNDING.md

@@ -0,0 +1,19 @@
+## Apalache Funding
+
+We are grateful to the following organizations for financially supporting
+the project Apalache for significant duration of time in the past:
+
+- [Informal Systems][]: 2020-2024
+- [Vienna Business Agency][]: 2021-2023
+- [Interchain Foundation][]: 2019-2023
+- [WWTF][] (Austria): Vienna Science and Technology Fund 2016-2020
+- [Inria Nancy][] and [LORIA][] (France): 2018-2019
+- [TU Wien][] (Austria): 2016-2020
+
+[WWTF]: https://wwtf.at/index.php?lang=EN
+[TU Wien]: https://www.tuwien.at/
+[Inria Nancy]: https://www.inria.fr/en/inria-centre-universite-lorraine
+[LORIA]: https://loria.fr
+[Interchain Foundation]: https://interchain.io/
+[Informal Systems]: https://informal.systems/
+[Vienna Business Agency]: https://viennabusinessagency.at/

Makefile

@@ -31,7 +31,8 @@ compile-strict: export APALACHE_FATAL_WARNINGS=true
 compile-strict:
 	sbt Test/compile compile
 
-# Run tests with scoverage report
+# Run tests with scoverage report.
+# This target is not used in the CI anymore. It needs additional devops work to re-enable it.
 test-coverage:
 	sbt coverage test coverageAggregate
 

README.md

@@ -3,16 +3,16 @@
 src="https://raw.githubusercontent.com/informalsystems/apalache/99e58d6f5eebcc41f432a126a13a5f8d2ae7afe6/logo-apalache.svg"
 alt="Apalache Logo">
 
-<h1><a href="https://apalache.informal.systems/">APALACHE</a></h1>
+<h1><a href="https://apalache-mc.org/">APALACHE</a></h1>
 
 <p>A symbolic model checker for TLA+<p>
 
 </div>
 
 [![main badge][]][main-ci]
 
-[main badge]: https://github.com/informalsystems/apalache/workflows/build/badge.svg?branch=main
-[main-ci]: https://github.com/informalsystems/apalache/actions?query=branch%3Amain+workflow%3Abuild
+[main badge]: https://github.com/apalache-mc/apalache/workflows/build/badge.svg?branch=main
+[main-ci]: https://github.com/apalache-mc/apalache/actions?query=branch%3Amain+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,7 +28,7 @@ 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:main`, use the jar from the
+`docker pull ghcr.io/apalache-mc/apalache:main`, use the jar from the
 most recent release, or checkout the source code from the most recent release
 tag.
 
@@ -49,10 +49,10 @@ manual][user-manual-installation].
 
 ## Website
 
-Our current website is served at https://apalache.informal.systems .
+Our current website is served at https://apalache-mc.org .
 
 The site is hosted by github, and changes can be made through PRs into the
-[gh-pages](https://github.com/informalsystems/apalache/tree/gh-pages) branch of
+[gh-pages](https://github.com/apalache-mc/apalache/tree/gh-pages) branch of
 this repository. See the README.md on that branch for more information.
 
 The user documentation is automatically deployed to the website branch as per
@@ -72,11 +72,11 @@ knowing too much about the internals of Apalache. Solving these issues would
 improve usability! Please comment in the relevant issue, if you are going to
 solve it.
 
-- Writing annotations in the JSON format: [#804](https://github.com/informalsystems/apalache/issues/804)
-- Add support for VIEW in the TLC config: [#851](https://github.com/informalsystems/apalache/issues/851)
+- Writing annotations in the JSON format: [#804](https://github.com/apalache-mc/apalache/issues/804)
+- Add support for VIEW in the TLC config: [#851](https://github.com/apalache-mc/apalache/issues/851)
 - Translate `\E x \in STRING: P` and `\A x \in STRING: P`:
-    [#844](https://github.com/informalsystems/apalache/issues/844)
-- Interval analysis for `a..b`: [#446](https://github.com/informalsystems/apalache/issues/446)
+    [#844](https://github.com/apalache-mc/apalache/issues/844)
+- Interval analysis for `a..b`: [#446](https://github.com/apalache-mc/apalache/issues/446)
 
 ## Industrial examples
 
@@ -142,27 +142,27 @@ Past funding from [Der Wiener Wissenschafts-, Forschungs- und Technologiefonds](
 
 [tla+]: http://lamport.azurewebsites.net/tla/tla.html
 [microsoft z3]: https://github.com/Z3Prover/z3
-[supported features]: https://apalache.informal.systems/docs/apalache/features.html
+[supported features]: https://apalache-mc.org/docs/apalache/features.html
 [tlc]: http://lamport.azurewebsites.net/tla/tools.html
 [leslie lamport's page on tla+]: http://lamport.azurewebsites.net/tla/tla.html
 [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
-[main branch]: https://github.com/informalsystems/apalache/tree/main
+[releases page]: https://github.com/apalache-mc/apalache/releases
+[master]: https://github.com/apalache-mc/apalache/tree/master
+[main branch]: https://github.com/apalache-mc/apalache/tree/main
 [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
 [standard repository of tla+ examples]: https://github.com/tlaplus/Examples
-[apalache benchmarks]: https://github.com/informalsystems/apalache-tests
-[checking inductive invariants]: https://github.com/informalsystems/apalache-tests/blob/master/results/001indinv-report.md
-[bounded model checking]: https://github.com/informalsystems/apalache-tests/blob/master/results/002bmc-report.md
-[user-manual]: http://informalsystems.github.io/apalache/docs/index.html
-[user-manual-docker]: https://apalache.informal.systems/docs/apalache/installation/docker.html
-[user-manual-installation]: https://apalache.informal.systems/docs/apalache/installation/index.html
-[language-manual]: https://apalache.informal.systems/docs/lang/index.html
-[idioms]: https://apalache.informal.systems//docs/idiomatic/index.html
+[apalache benchmarks]: https://github.com/apalache-mc/apalache-tests
+[checking inductive invariants]: https://github.com/apalache-mc/apalache-tests/blob/master/results/001indinv-report.md
+[bounded model checking]: https://github.com/apalache-mc/apalache-tests/blob/master/results/002bmc-report.md
+[user-manual]: http://apalache-mc.org/docs/index.html
+[user-manual-docker]: https://apalache-mc.org/docs/apalache/installation/docker.html
+[user-manual-installation]: https://apalache-mc.org/docs/apalache/installation/index.html
+[language-manual]: https://apalache-mc.org/docs/lang/index.html
+[idioms]: https://apalache-mc.org/docs/idiomatic/index.html
 [light client specs]: https://github.com/tendermint/tendermint/tree/master/spec/light-client/verification
 [model-based testing]: https://github.com/informalsystems/tendermint-rs/tree/master/light-client/tests/support/model_based#light-client-model-based-testing-guide
-[apalache.informal.systems]: https://apalache.informal.systems
+[apalache-mc.org]: https://apalache-mc.org
 [TLA-Apalache workshop]: https://github.com/informalsystems/tla-apalache-workshop
-[Beginner's tutorial]: https://apalache.informal.systems/docs/tutorials/entry-tutorial.html
+[Beginner's tutorial]: https://apalache-mc.org/docs/tutorials/entry-tutorial.html

VERSION

@@ -1 +1 @@
-0.44.12-SNAPSHOT
+0.45.4-SNAPSHOT

build.sbt

@@ -8,19 +8,19 @@ import scala.sys.process._
 ///////////////////////////
 
 name := "apalache"
-maintainer := "apalache@informal.org"
+maintainer := "apalache@konnov.phd"
 
 // See https://www.scala-sbt.org/1.x/docs/Multi-Project.html#Build-wide+settings
-ThisBuild / organizationName := "Informal Systems Inc."
-ThisBuild / organizationHomepage := Some(url("https://informal.systems"))
+ThisBuild / organizationName := "Apalache Development Team"
+ThisBuild / organizationHomepage := Some(url("https://apalache-mc.org"))
 ThisBuild / licenses += "Apache 2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0")
 
 // We store the version in a bare file to make accessing and updating the version trivial
 ThisBuild / versionFile := (ThisBuild / baseDirectory).value / "VERSION"
 ThisBuild / version := scala.io.Source.fromFile(versionFile.value).mkString.trim
 
 ThisBuild / organization := "at.forsyte"
-ThisBuild / scalaVersion := "2.13.13"
+ThisBuild / scalaVersion := "2.13.14"
 
 // Add resolver for Sonatype OSS Snapshots and Releases Maven repository
 ThisBuild / resolvers ++= Resolver.sonatypeOssRepos("snapshots")
@@ -351,7 +351,7 @@ lazy val root = (project in file("."))
         log.info(s"Unpacking package ${pkg} to ${target_dir}")
         // send outputs directly to std{err,out} instead of logging here
         // to avoid misleading logging output from tar
-        // See https://github.com/informalsystems/apalache/pull/1382
+        // See https://github.com/apalache-mc/apalache/pull/1382
         (s"tar zxvf ${pkg} -C ${target_dir}" !)
         log.info(s"Symlinking ${current_pkg} -> ${unzipped}")
         if (current_pkg.exists) {
@@ -369,7 +369,7 @@ lazy val root = (project in file("."))
 docker / imageNames := {
   val img: String => ImageName = s =>
     ImageName(
-        namespace = Some("ghcr.io/informalsystems"),
+        namespace = Some("ghcr.io/apalache-mc"),
         repository = name.value,
         tag = Some(s),
     )
@@ -406,7 +406,7 @@ docker / dockerfile := {
 
     // We need sudo to run apalache using the user (created in the entrypoint script)
     run("apt", "update")
-    run("apt", "install", "sudo")
+    run("apt", "install", "-y", "sudo")
 
     entryPoint("/opt/apalache/bin/run-in-docker-container")
   }
@@ -425,7 +425,7 @@ lazy val versionFile = settingKey[File]("Location of the file tracking the proje
 // These tasks are used in our bespoke release pipeline
 // TODO(shon): Once we've changed our packaging to conform to more standard SBT structures and practices,
 // we should consider moving to a release pipeline based around sbt-release.
-// See https://github.com/informalsystems/apalache/issues/1248
+// See https://github.com/apalache-mc/apalache/issues/1248
 
 lazy val printVersion = taskKey[Unit]("Print the current version")
 printVersion := {

docs/src/apalache/installation/docker.md

@@ -14,15 +14,15 @@ suitable JVM, and the container supplies this. However, you must already have
 To get the latest Apalache image, issue the command:
 
 ```bash
-docker pull ghcr.io/informalsystems/apalache
+docker pull ghcr.io/apalache-mc/apalache
 ```
 
 ## Running the docker image
 
 To run an Apalache image, issue the command:
 
 ```bash
-$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/informalsystems/apalache <args>
+$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/apalache-mc/apalache <args>
 ```
 
 The following docker parameters are used:
@@ -38,8 +38,8 @@ The following docker parameters are used:
 
   When using SELinux, you might have to use the modified form of `-v` option:
     `-v <your-spec-directory>:/var/apalache:z`
-- `informalsystems/apalache` is the APALACHE docker image name. By default, the `latest` stable
-  version is used; you can also refer to a specific tool version, e.g., `informalsystems/apalache:0.6.0` or `informalsystems/apalache:main`
+- `apalache-mc/apalache` is the APALACHE docker image name. By default, the `latest` stable
+  version is used; you can also refer to a specific tool version, e.g., `apalache-mc/apalache:0.6.0` or `apalache-mc/apalache:main`
 - `<args>` are the tool arguments as described in [Running the Tool](../running.md).
 
 We provide a convenience wrapper for this docker command in
@@ -67,11 +67,11 @@ Apalache in docker while sharing the working directory:
 
 ###### using the latest stable
 
-$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache'
+$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/apalache-mc/apalache'
 
 ###### using the latest main
 
-$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache:main'
+$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/apalache-mc/apalache:main'
 ```
 
 ## Using the development branch of Apalache
@@ -82,25 +82,25 @@ branch for a report of the newest features. Since we cut releases weekly, you
 should have access to all the latest features in the last week by using the
 `latest` tag. However, if you wish to use the very latest developments as they
 are added throughout the week, you can run the image with the `main` tag: just
-type `ghcr.io/informalsystems/apalache:main` instead of
-`ghcr.io/informalsystems/apalache` everywhere.
+type `ghcr.io/apalache-mc/apalache:main` instead of
+`ghcr.io/apalache-mc/apalache` everywhere.
 
 Do not forget to pull the docker image from time to time:
 
 ```bash
-docker pull ghcr.io/informalsystems/apalache:main
+docker pull ghcr.io/apalache-mc/apalache:main
 ```
 
 Run it with the following command:
 
 ```bash
-$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/informalsystems/apalache:main <args>
+$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/apalache-mc/apalache:main <args>
 ```
 
 To create an alias pointing to the `main` version:
 
 ```bash
-$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache:main'
+$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/apalache-mc/apalache:main'
 ```
 
 [changelog]: https://github.com/informalsystems/apalache/blob/main/CHANGES.md

docs/src/apalache/tuning.md

@@ -22,14 +22,6 @@ The following options are supported:
 `smt.randomSeed=<int>` passes the random seed to `z3` (via `z3`'s parameters
 `sat.random_seed` and `smt.random_seed`).
 
-##  Timeouts
-
-`search.smt.timeout=<seconds>` defines the timeout to the SMT solver in seconds.
-The default value is `0`, which stands for the unbounded timeout.  For instance,
-the timeout is used in the following cases: checking if a transition is enabled,
-checking an invariant, checking for deadlocks. If the solver times out, it
-reports 'UNKNOWN', and the model checker reports a runtime error.
-
 ## Invariant mode
 
 `search.invariant.mode=(before|after)` defines the moment when the invariant is