search

FStarLang / fstar-interactive

An F* interactive mode for the atom editor
MIT License
7 stars 4 forks source link

Very unfriendly error messages turn off new users #12

Open catalin-hritcu opened 9 years ago

catalin-hritcu commented 9 years ago

John Kennerley reports this:

I downloaded Atom, git cloned atom-fstar and git cloned atom-interactive. I ran apm intsall and apm link for both. It looks like I got Atom syntax highlighting but fstar interactive in atom is giving me a exception in Atom. Ctrl-Shift-i in Atom with a jk.fst file open yields an exception in Atom. I tried clicking the create an issue on Atom from inside Atom but got a unicorn picture from github. It looks like the Atom with fstar development could be a good thing, although was semi expecting a VS support for fstar.

image

This page is taking way too long to load.

The Atom exception Error: ENOENT: no such file or directory, lstat 'C:\Users\John\AppData\Local\atom\app-1.0.7\atom:' at Error (native) at fs.lstatSync (fs.js:836:18) at Object.fs.lstatSync (ATOM_SHELL_ASAR.js:170:16) at Object.realpathSync (fs.js:1439:21) at Object.fs.realpathSync (ATOM_SHELL_ASAR.js:243:29) at C:\fstar-interactive\lib\main.js:180:27 at Function.find (C:\fstar-interactive\node_modules\lodash\dist\lodash.js:3217:15) at FStarMain.module.exports.FStarMain.fstarArgs (C:\fstar-interactive\lib\main.js:179:33) at FStarMain.module.exports.FStarMain.buildCommand (C:\fstar-interactive\lib\main.js:221:21) at FStarMain.module.exports.FStarMain.startChildProcess (C:\fstar-interactive\lib\main.js:276:20)

I agree that the error messages should be better, but the fstar-interactive is really just a way to run F. If you didn't manage to compile F and get an executable for it that you can use from the command line then there is no way you can use fstar-interactive. The cryptic error might be about not finding fstar.exe in your PATH ...

markulf commented 9 years ago

Love the unicorn.

Could we make apm install check that fstar is in the path? I really know too little about atom, maybe having some pointers and a rough development guide in the GitHub README.md of the two projects would attract more developer time for these mundane issues.

fournet commented 9 years ago

I also struggled with raw atom error reports; catching the error and reporting e.g. "F* not found" would be better than checking at install time.