diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 51e1c69e3..c9fc71ebd 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,6 +1,6 @@ # Contributing -Welcome to the Quint repository! We are excited that you want to contribute to +Welcome to the Quint repository! We are excited that you want to contribute to Quint, whether it is by reporting issues, suggesting features, or writing code. ## Table of Contents @@ -78,7 +78,7 @@ This repository hosts all Quint pieces: - [ADR002: Error codes](./docs/content/docs/development-docs/architecture-decision-records/adr002-errors.md) - [ADR003: Interface to visit Internal Representation - components](./docs/content/docs/development-docs/architecture-decision-records/adr003-visiting-ir-components.md) + components](./docs/content/docs/development-docs/architecture-decision-records/adr003-visiting-ir-components.md) - [ADR004: An Effect System for Quint](./docs/content/docs/development-docs/architecture-decision-records/adr004-effect-system.md) - [ADR005: A Type System for @@ -280,14 +280,14 @@ ln -s $PWD/vscode/quint-vscode/ $HOME/.vscode/extensions/informal.quint-vscode-X We use `yalc` to manage unpublished packages. To install it, run -``` sh +```sh npm i yalc -g ``` Then use the `local` make target to replace the published version of `quint` with the local one and build the extension: -``` sh +```sh make local ``` @@ -308,13 +308,13 @@ Write unit tests in [quint/test](./quint/test), add test data to [quint/testFixture](./quint/testFixture). To run the tests and check code coverage, run the following commands (in the [quint](./quint) folder): - 1. Run unit tests: +1. Run unit tests: ```sh npm run test ``` - 1. Check code coverage with tests: +1. Check code coverage with tests: ```sh npm run coverage @@ -326,7 +326,7 @@ When adding a new test fixture or updating an existing one, you might need to generate the `.json` and `.map.json` files used in test expectations. For that, run: -``` sh +```sh npm run update-fixtures ``` @@ -365,10 +365,10 @@ The files containing tests for `txm` are: Run integration tests: - ```sh - npm run compile && npm link && npm run integration - ``` - +```sh +npm run compile && npm link && npm run integration +``` + PS: this will not run the Apalache-related tests, as they usually won't break as consequences of changes in the Quint codebase. They are run in the CI, and you can run them locally by running `npm run apalache-integration` and `npm run @@ -388,7 +388,7 @@ To [add a new dependency for integration tests or other development purposes](https://docs.npmjs.com/specifying-dependencies-and-devdependencies-in-a-package-json-file) run: -``` sh +```sh npm install --save-dev ``` @@ -402,7 +402,7 @@ To [add a new dependency for integration tests or other development purposes](https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html) run: -``` sh +```sh cargo add --dev ``` @@ -436,7 +436,7 @@ lose the advantage of exhaustiveness checking. Here's an example: Assume we have a type `T` ```typescript -type T = 'a' | 'b' | 'c' +type T = 'a' | 'b' | 'c'; ``` We should structure our program such that @@ -445,7 +445,7 @@ We should structure our program such that - whenever a new alternative is added to this type, the type system will warn us about all the places we need to account for the new kind of data. -If we use `T` with a `switch` or `if`/`then` statement that *returns values*, +If we use `T` with a `switch` or `if`/`then` statement that _returns values_, this indispensable help is ensured. E.g., if we try to write the following: ```typescript @@ -535,15 +535,15 @@ false false ``` -For this reason, we are using `isEqual` provided by the [lodash.isequal][] +For this reason, we are using `isEqual` provided by the [node:util][] package: ```js > import { none, just } from '@sweet-monads/maybe' -> import isEqual from 'lodash.isequal' -> isEqual(just(true), just(true)) +> import { isDeepStrictEqual } from 'node:util' +> isDeepStrictEqual(just(true), just(true)) true -> isEqual(none(), none()) +> isDeepStrictEqual(none(), none()) true ``` @@ -606,7 +606,7 @@ the Rust evaluator and the VSCode extension + the language server. This will trigger the release and publication of the package to npm and GitHub. - + ### Evaluator The evaluator is the latest addition to the Quint repository, and it's release diff --git a/quint/package-lock.json b/quint/package-lock.json index fb4b9f0d3..a3b1a9e1a 100644 --- a/quint/package-lock.json +++ b/quint/package-lock.json @@ -28,7 +28,6 @@ "line-column": "^1.0.2", "lodash": "^4.17.21", "lodash.clonedeep": "4.5.0", - "lodash.isequal": "^4.5.0", "seedrandom": "^3.0.5", "tar": "^6.1.14", "yargs": "^17.7.2" @@ -6588,11 +6587,6 @@ "integrity": "sha512-uHaJFihxmJcEX3kT4I23ABqKKalJ/zDrDg0lsFtc1h+3uw49SIJ5beyhx5ExVRti3AvKoOJngIj7xz3oylPdWQ==", "dev": true }, - "node_modules/lodash.isequal": { - "version": "4.5.0", - "resolved": "https://registry.npmjs.org/lodash.isequal/-/lodash.isequal-4.5.0.tgz", - "integrity": "sha512-pDo3lu8Jhfjqls6GkMgpahsF9kCyayhgykjyLMNFTKWrpVdAQtYyB4muAMWozBB4ig/dtWAmsMxLEI8wuz+DYQ==" - }, "node_modules/lodash.merge": { "version": "4.6.2", "resolved": "https://registry.npmjs.org/lodash.merge/-/lodash.merge-4.6.2.tgz", diff --git a/quint/package.json b/quint/package.json index 0ced04675..eddcdf90e 100644 --- a/quint/package.json +++ b/quint/package.json @@ -67,7 +67,6 @@ "line-column": "^1.0.2", "lodash": "^4.17.21", "lodash.clonedeep": "4.5.0", - "lodash.isequal": "^4.5.0", "seedrandom": "^3.0.5", "tar": "^6.1.14", "yargs": "^17.7.2" diff --git a/quint/src/effects/base.ts b/quint/src/effects/base.ts index f2419c052..a646805ef 100644 --- a/quint/src/effects/base.ts +++ b/quint/src/effects/base.ts @@ -17,7 +17,7 @@ import { Either, left, mergeInMany, right } from '@sweet-monads/either' import { Substitutions, applySubstitution, applySubstitutionToEntity, compose } from './substitutions' import { Error, ErrorTree, buildErrorLeaf, buildErrorTree } from '../errorTree' import { flattenUnions, simplify } from './simplification' -import isEqual from 'lodash.isequal' +import { isDeepStrictEqual } from 'node:util' import { differenceWith, intersectionWith } from 'lodash' /* Kinds for concrete effect components */ @@ -332,7 +332,7 @@ export function unifyEntities(va: Entity, vb: Entity): Either v.name)), new Set(v2.stateVariables.map(v => v.name)))) { + if (isDeepStrictEqual(new Set(v1.stateVariables.map(v => v.name)), new Set(v2.stateVariables.map(v => v.name)))) { return right([]) } else { return left({ @@ -349,7 +349,7 @@ export function unifyEntities(va: Entity, vb: Entity): Either unifyEntities(v, v2))) @@ -358,10 +358,10 @@ export function unifyEntities(va: Entity, vb: Entity): Either 0) { - const s1 = { ...v1, entities: differenceWith(v1.entities, intersection, isEqual) } - const s2 = { ...v2, entities: differenceWith(v2.entities, intersection, isEqual) } + const s1 = { ...v1, entities: differenceWith(v1.entities, intersection, isDeepStrictEqual) } + const s2 = { ...v2, entities: differenceWith(v2.entities, intersection, isDeepStrictEqual) } // There was an intersection, try to unify the remaining entities return unifyEntities(s1, s2) diff --git a/quint/src/effects/modeChecker.ts b/quint/src/effects/modeChecker.ts index 8a657cc2b..8b29593f7 100644 --- a/quint/src/effects/modeChecker.ts +++ b/quint/src/effects/modeChecker.ts @@ -13,7 +13,7 @@ * @module */ -import isEqual from 'lodash.isequal' +import { isDeepStrictEqual } from 'node:util' import { qualifierToString } from '../ir/IRprinting' import { IRVisitor, walkDeclaration } from '../ir/IRVisitor' import { QuintError } from '../quintError' @@ -248,7 +248,7 @@ function addedEntities(paramEntities: Entity[], resultEntity: Entity): Entity[] case 'union': return resultEntity.entities.flatMap(entity => addedEntities(paramEntities, entity)) case 'concrete': { - const vars = resultEntity.stateVariables.filter(v => !paramEntities.some(p => isEqual(p, v))) + const vars = resultEntity.stateVariables.filter(v => !paramEntities.some(p => isDeepStrictEqual(p, v))) if (vars.length === 0) { return [] } @@ -256,7 +256,7 @@ function addedEntities(paramEntities: Entity[], resultEntity: Entity): Entity[] return [{ kind: 'concrete', stateVariables: vars }] } case 'variable': - return !paramEntities.some(p => isEqual(p, resultEntity)) ? [resultEntity] : [] + return !paramEntities.some(p => isDeepStrictEqual(p, resultEntity)) ? [resultEntity] : [] } } diff --git a/quint/src/effects/simplification.ts b/quint/src/effects/simplification.ts index ec4b65501..900364af7 100644 --- a/quint/src/effects/simplification.ts +++ b/quint/src/effects/simplification.ts @@ -12,9 +12,9 @@ * @module */ -import isEqual from 'lodash.isequal' import { unreachable } from '../util' import { ConcreteEffect, Effect, Entity, StateVariable } from './base' +import { isDeepStrictEqual } from 'node:util' /** * Simplifies a concrete effect by: @@ -100,7 +100,7 @@ function deduplicateEntity(entity: Entity): Entity { const nestedEntities = entity.entities.map(v => deduplicateEntity(v)) const unique: Entity[] = [] nestedEntities.forEach(entity => { - if (!unique.some(v => isEqual(v, entity))) { + if (!unique.some(v => isDeepStrictEqual(v, entity))) { unique.push(entity) } }) diff --git a/quint/src/effects/substitutions.ts b/quint/src/effects/substitutions.ts index 3bf884945..0f1e63959 100644 --- a/quint/src/effects/substitutions.ts +++ b/quint/src/effects/substitutions.ts @@ -17,7 +17,7 @@ import { ErrorTree, buildErrorTree } from '../errorTree' import { Effect, Entity } from './base' import { effectToString, substitutionsToString } from './printing' import { simplify } from './simplification' -import { isEqual } from 'lodash' +import { isDeepStrictEqual } from 'node:util' /* * Substitutions can be applied to both effects and entities, replacing @@ -88,7 +88,7 @@ export function applySubstitution(subs: Substitutions, e: Effect): Either { - if (!isEqual(r, e)) { + if (!isDeepStrictEqual(r, e)) { // Keep re-applying the substitutions until the effect is unchanged. // Useful when substitutions have a transitive pattern [ a |-> b, b |-> c ] return applySubstitution(subs, r) diff --git a/quint/src/runtime/impl/nondet.ts b/quint/src/runtime/impl/nondet.ts index 93d36e6bb..9195c6df7 100644 --- a/quint/src/runtime/impl/nondet.ts +++ b/quint/src/runtime/impl/nondet.ts @@ -15,7 +15,7 @@ import { Either, right } from '@sweet-monads/either' import { EvalFunction } from './builder' import { RuntimeValue, rv } from './runtimeValue' -import { isEqual } from 'lodash' +import { isDeepStrictEqual } from 'node:util' import { QuintError } from '../../quintError' import { CachedValue } from './Context' import { Maybe } from '@sweet-monads/maybe' @@ -92,7 +92,7 @@ export function evalNondet( } // Retry if condition is satisfied and we haven't exhausted all possible positions. - } while (shouldRetry && !isEqual(newPositions, originalPositions)) + } while (shouldRetry && !isDeepStrictEqual(newPositions, originalPositions)) // Reset the cache cache.value = undefined diff --git a/quint/src/types/substitutions.ts b/quint/src/types/substitutions.ts index 7d901fea2..0713a0ba2 100644 --- a/quint/src/types/substitutions.ts +++ b/quint/src/types/substitutions.ts @@ -19,7 +19,7 @@ import { ConcreteFixedRow, QuintType, Row } from '../ir/quintTypes' import { Constraint } from './base' import { unify, unifyRows } from './constraintSolver' import { substitutionsToString } from './printing' -import { isEqual } from 'lodash' +import { isDeepStrictEqual } from 'node:util' /* * Substitutions can be applied to Quint types, type variables with another type @@ -113,7 +113,7 @@ export function applySubstitution(table: LookupTable, subs: Substitutions, t: Qu } const result = singleApplication() - if (isEqual(result, t)) { + if (isDeepStrictEqual(result, t)) { return t } else { return applySubstitution(table, subs, result) diff --git a/quint/src/util.ts b/quint/src/util.ts index 2ce0caf95..153b7631a 100644 --- a/quint/src/util.ts +++ b/quint/src/util.ts @@ -56,7 +56,7 @@ export function zip(a: A[], b: B[]): [A, B][] { * * ``` * const result = findMap([1,2,3], (x) => x % 2 === 0 ? just(x) : none()) - * lodash.isEqual(result, just(2)) + * lodash.isDeepStrictEqual(result, just(2)) * ``` * */ export function findMap(xs: Iterable, f: (x: X) => Maybe): Maybe {