Merge remote-tracking branch 'origin/main' into igor/ics23-fix

CHANGELOG.md

@@ -7,6 +7,82 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## UNRELEASED
 
+### Added
+### Changed
+### Deprecated
+### Removed
+### Fixed
+### Security
+
+## v0.22.4 -- 2024-11-19
+
+### Added
+### Changed
+### Deprecated
+### Removed
+### Fixed
+
+- Fixed a problem where traces other than the first one when `--n-traces` > 1
+  and `--mbt` is true had the incorrect `action_taken` and `nondet_picks` values
+  (#1553).
+
+### Security
+
+## v0.22.3 -- 2024-10-28
+
+### Added
+
+- Added a new operator called `getOnlyElement()` to extract elements out of singleton sets (#1525)
+
+### Changed
+
+- Updated grammar rule to allow an optional trailing comma in parameter lists (#1510):
+  - Operator calls
+  - Constant initialization
+  - Operator definitions
+
+### Deprecated
+### Removed
+### Fixed
+
+- The seed was not being properly printed when the simulator found some runtime errors (#1524).
+- Fixed a problem where using `--mbt` resulted in missing data on `nondet_picks`
+  due to internal caching (#1531)
+- Hashbang lines are now properly highlighted as comments in vscode and in highlight.js.
+
+### Security
+
+## v0.22.2 -- 2024-10-08
+
+### Added
+
+- `quint verify` has the option `--apalache-version` to pull a custom version (#1521)
+- Grammar updated with support for an optional leading hashbang (`#!`) line (#1522)
+
+### Changed
+### Deprecated
+### Removed
+### Fixed
+
+### Security
+
+## v0.22.1 -- 2024-09-25
+
+### Added
+### Changed
+### Deprecated
+### Removed
+### Fixed
+
+- Some error scenarios when importing files on Windows were fixed (#1498)
+- `quint verify` on Windows should now properly start an Apalache server on the
+  background (#1499)
+- `quint verify` on Linux properly terminates the spawned instance (#1520)
+
+### Security
+
+## v0.22.0 -- 2024-09-09
+
 ### Added
 
 - Calling `q::test`, `q::testOnce` and `q::lastTrace` on the REPL now works properly (#1495)
@@ -51,6 +127,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Bumped GRPC message sizes to 1G (#1480)
 - Fix format of ITF trace emitted by `verify` command (#1448)
 - Relax uppercase check for types qualified with a namespace (#1494)
+- Fixed file loading from imports on Windows (#1498)
 
 ### Security
 

docs/README.md

@@ -4,7 +4,7 @@
 
 - [Language tutorials](../tutorials/README.md)
 - [Syntax specification](./lang.md)
-- [Cheatsheet](./quint-cheatsheet.pdf)
+- [Cheatsheet](./public/quint-cheatsheet.pdf)
 - [API documentation for built-in operators](./builtin.md)
 
 ## Tooling

docs/components/faq/FAQBox.tsx

@@ -0,0 +1,49 @@
+import { useState, useEffect } from "react";
+
+export function FAQBox({ title, children }) {
+  const id = title.toLowerCase().replace(/[/?]/g, "").replace(/\s+/g, "-");
+  useEffect(() => {
+    const handleHashChange = () => {
+      const element = document.getElementById(id);
+      if (element && window.location.hash === `#${id}` && "open" in element) {
+        element.open = true;
+        element.scrollIntoView();
+      }
+    };
+
+    const handleAnchorClick = (event) => {
+      const anchor = event.target.closest("a");
+      if (anchor && anchor.hash === `#${id}`) {
+        const element = document.getElementById(id);
+        if (element && "open" in element) {
+          element.open = true;
+          element.scrollIntoView();
+        }
+      }
+    };
+
+    window.addEventListener("hashchange", handleHashChange);
+    document.addEventListener("click", handleAnchorClick);
+    handleHashChange();
+
+    return () => {
+      window.removeEventListener("hashchange", handleHashChange);
+      document.removeEventListener("click", handleAnchorClick);
+    };
+  }, [id]);
+
+  return (
+    <details
+      className="last-of-type:mb-0 rounded-lg bg-neutral-50 dark:bg-neutral-800 p-2 mt-4"
+      id={id}
+      onClick={() => {
+        window.history.pushState({}, "", `#${id}`);
+      }}
+    >
+      <summary>
+        <strong className="text-lg">{title}</strong>
+      </summary>
+      <div className="nx-p-2">{children}</div>
+    </details>
+  );
+}

docs/pages/docs/builtin.md

@@ -306,6 +306,19 @@ assert(Set(1, 2).allListsUpTo(1) == Set([], [1], [2]))
 assert(Set(1).allListsUpTo(2) == Set([], [1], [1, 1]))
 ```
 
+## getOnlyElement
+
+Signature: `pure def getOnlyElement: (Set[a]) => a`
+
+`s.getOnlyElement()` is, deterministically, the only element of `s`.
+If the size of `s` is not 1, this operator has undefined behavior.
+
+### Examples
+
+```quint
+assert(Set(5).getOnlyElement() == 5)
+```
+
 ## chooseSome
 
 Signature: `pure def chooseSome: (Set[a]) => a`