An exception when loading a file from a different directory

informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

Apache License 2.0

608 stars 30 forks source link

An exception when loading a file from a different directory #1449

Open konnov opened 1 month ago

konnov commented 1 month ago

Consider the following two commands in the Quint home directory:

$ cd examples/cosmos/tendermint
$ quint -r TendermintModels.qnt::TendermintModels
Quint REPL 0.19.4
...
$ cd ..
$ # now we are in examples/cosmos and this fails:
$ quint -r tendermint/TendermintModels.qnt::TendermintModels
... produces a long stack trace