[feature request] support spec files about intellij-move HOT 4 CLOSED

Do you know if there are any scoping rules specific to this naming? Like, MODULE_NAME.spec.move having exclusive access to all items in the MODULE_NAME.move file, something like that? Maybe there are some docs?

from intellij-move.

I've added support for those files in 1.18.0, I'm going to release a new version at the beginning of the next week.

Spec modules scoping is really weird, basically, this code is valid

module 0x1::basket {
    fun main() {
        let _a = string::utf8(b"hello");
    }
}
spec 0x1::basket {
    use std::string;
}

and those spec modules can be anywhere in the package.

from intellij-move.

I've added support for those files in 1.18.0, I'm going to release a new version at the beginning of the next week.

Spec modules scoping is really weird, basically, this code is valid

module 0x1::basket {
    fun main() {
        let _a = string::utf8(b"hello");
    }
}
spec 0x1::basket {
    use std::string;
}

and those spec modules can be anywhere in the package.

The scoping was designed like so that if something is only used in the specification, it wouldn't be included in the final dependencies of the module bytecode.

Thanks for making this happen! I guess you are using the Move compilers expansion phase to also deal with spec name resolution? After expansion, the Move compiler and the Spec compiler go very different ways.

from intellij-move.

@wrwg

The scoping was designed like so that if something is only used in the specification, it wouldn't be included in the final dependencies of the module bytecode.

Yes, this is what I assumed, I expected the "spec" scope to be nested to the "main" scope, like

module 0x1::main {
   spec 0x1::main {
       use 0x1::string;  // isn't visible outside the scope
   }
}

but implicitly. And schema, spec fun imports will be special cased to be importable from the module itself, to be able to use

use 0x1::main::MySchema;

I just don't understand why imports inside the spec code leak into the main code. From the point of the compiler implementation, you can't just use local information to resolve names in the module anymore (for the non-spec code), you need to go through the whole package to try to find spec MODULE_NAME {} blocks and check for the imports there. Maybe it's a bug?

Thanks for making this happen! I guess you are using the Move compilers expansion phase to also deal with spec name resolution? After expansion, the Move compiler and the Spec compiler go very different ways.

If you mean the Move compiler itself:
no, I don't use it, Intellij-Move basically reimplements the compiler in Kotlin. I have a scoping rule, which splits spec items and non-spec items into separate groups.

from intellij-move.