Skip to content
This repository was archived by the owner on Dec 14, 2025. It is now read-only.
This repository was archived by the owner on Dec 14, 2025. It is now read-only.

Very unfriendly error messages turn off new users #12

Description

@catalin-hritcu

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 ...

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions