How to run tests in deep modules?

[p-offtermatt]

My spec is this: https://github.com/cosmos/interchain-security/blob/e09968d94a4e5a84bf144e5f0737e1f529494772/tests/difference/core/quint_model/ccv.qnt#L212

When I run quint test ccv.qnt --main CCVDefaultStateMachine I would expect the tests in the CCV module to be run. They are not; I guess because they themselves are not imported in CCVDefaultStateMachine, because CCV is not exported by CCVStatemachineLogic.

Adding export CCV.* to CCVStatemachineLogic (e.g. after import CCV.* does not work), when running quint test I get this:

Error: Internal error while flattening [QNT404] Name 'PROVIDER_CHAIN' not found,[QNT404] Name 'PROVIDER_CHAIN' not found
    at resolveNamesOrThrow (/Users/offtermatt/projects/quint/quint/dist/src/flattening/fullFlattener.js:90:15)
    at flattenModules (/Users/offtermatt/projects/quint/quint/dist/src/flattening/fullFlattener.js:61:35)
    at runTests (/Users/offtermatt/projects/quint/quint/dist/src/cliCommands.js:248:104)
    at EitherConstructor.asyncChain (/Users/offtermatt/projects/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:125:16)
    at /Users/offtermatt/projects/quint/quint/dist/src/cli.js:33:39

If I add export CCV without .*, I get this error:

Error: Internal error while flattening [QNT404] Name 'UnbondingPeriodPositiveTest' not found,[QNT404] Name 'VscTimeoutPositiveTest' not found,[QNT404] Name 'CcvTimeoutPositiveTest' not found,[QNT404] Name 'CcvTimeoutLargerThanUnbondingPeriodTest' not found,[QNT404] Name 'ProviderIsNotAConsumerTest' not found,[QNT404] Name 'CcvTimeoutKeysTest' not found,[QNT404] Name 'UnbondingPeriodKeysTest' not found
    at resolveNamesOrThrow (/Users/offtermatt/projects/quint/quint/dist/src/flattening/fullFlattener.js:90:15)
    at flattenModules (/Users/offtermatt/projects/quint/quint/dist/src/flattening/fullFlattener.js:73:24)
    at runTests (/Users/offtermatt/projects/quint/quint/dist/src/cliCommands.js:248:104)
    at EitherConstructor.asyncChain (/Users/offtermatt/projects/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:125:16)
    at /Users/offtermatt/projects/quint/quint/dist/src/cli.js:33:39

Is there a way to do what I am trying to do, i.e. run the tests in CCV, but with the instantiation I have done through CCVStatemachineLogic from CCVDefaultStateMachine? I am not sure if any of the behaviour here is a bug. At least from a users perspective, the error messages seem weird, but I can't quite tell.

[bugarela]

I guess because they themselves are not imported in CCVDefaultStateMachine, because CCV is not exported by CCVStatemachineLogic.

Yes, that's right, you need the export exactly as you said.

The export should work, but it's breaking flattening for some reason. That's not even related to the tests - if I comment out all of the tests, it still crashes.

Seems like an export bug to me.

[p-offtermatt]

Thanks for looking into it. I worked around this for now by splitting my modules differently, so it's not blocking me.