search

digama0 / mm0

Metamath Zero specification language
Creative Commons Zero v1.0 Universal
315 stars 40 forks source link

vscode-mm0 notation issues with lean.mm1 #16

Closed ammkrn closed 4 years ago

ammkrn commented 4 years ago

commit : master 7eacd8 OS : Ubuntu 18.04.4 LTS haskell stack : 2.1.3 (df6d1f)

I built mm0-hs using the stack install instructions.

This only seems to happen with examples/lean.mm1, but whether the plugin is installed from the marketplace or from the source, there's a cascade of errors and red underlines after line 32 notation l_pl (u v a b) = u ($+l$:0) a ($<=$:0) v ($+l$:0) b: 0 lassoc; that all are about either uses of the <= notation or +l notation.

The unique ones that start the chain are

unexpected ':'
expecting '(', ';', or identifier char
MM0 [32, 61]
unexpected '+'
expecting '$' or infix >= 0
MM0 [33, 35]
term 'l_le' not declared
MM0 [37, 20]

The rest of them are repetitions of unexpected notation errors.

Also just a heads up, the directions for installing the extension from source might benefit from an explicit mention that users might need to run npm install before npm run compile. Running the latter without the former gave me an error about not being able to find tsc.

digama0 commented 4 years ago

I will look into this later, but for now, you might want to try using mm0-rs as your MM0 server, which is at this point better supported than mm0-hs and will be made the default shortly. The issue in this case is that mm0-hs doesn't support composite infix notations yet (the : 0 lassoc is part of that, and mm0-hs doesn't know what to do with it).

ammkrn commented 4 years ago

Thanks, switching to mm0-rs cleared it up.