`import... from...` in REPL does not work

[konnov]

It looks like we have dismantled support for imports from files in REPL, when we made it incremental.

Consider a simple spec:

module foo {                                                                                       
  pure def x = 3
}

Suppose that the following command works for foo.qnt:

$ quint -r foo.qnt::foo
>>> x
3

The following command, which should be equivalent, does not work:

$ quint
>>> import foo.* from "./foo"
syntax error: error: [QNT405] Module 'foo' not found
import foo.* from "./foo"
^^^^^^^^^^^^^^^^^^^^^^^^^

[konnov]

The deeper I got into this issue, the more I understood how hard it would be to support import... from in REPL. I have a semi-working solution in https://github.com/informalsystems/quint/tree/igor/import1180

But it seems that it would take me 2-3 more days to fully implement it, which I do not have atm. This issue would require a very careful refactoring of incremental compilation.

@bugarela, do you think it would make sense to add an error message in REPL that import... from... is not supported? That should be relatively easy to do.

[konnov]

We have quint -r foo.qnt::qnt and .load in REPL. So supporting import... from... is not critical, though it would definitely make REPL more delightful :)

[bugarela]

Alternatively, we could disable incremental compilation for import ... from ..., that is, whenever that sort of declaration is evaluated by the REPL, we re-evaluate the whole thing (non-incrementally). I'm not sure, but that should be relatively easy to do.