Roadmap for usable interfaces - FStarLang/FStar GitHub Wiki

  • The Emacs mode should send the complete path to F* so that it can perform the initial loading & dependency analysis properly (done via https://github.com/FStarLang/FStar/commit/2124ad68a7a41fed982ab4cf1a6a7d442389bdbb)
    • Why don't we rely on Aseem's dependencies-as-you-go feature? Because it's unsound so we might as well do a first (sound) analysis first thing.
    • This would solve the problem of one launching Emacs on a file that is not in the current directory (currently a broken scenario) Yes
    • We still may want a warning that if Emacs is in dir1 and launches F* on dir2/Foo.fst and dir2 is not in the include path, then this is sketchy (need to send the current working directory to F*, then) TODO
  • We need --interactive ==> --partial done via https://github.com/FStarLang/FStar/commit/5a6f70ae90f08abbb022f68277b96e3adc8b1d3e (partial is now the default unless --verify_all (or the upcoming --extract_all) is specified)
  • We need to fix the broken dependency arrow from fsti to fst (done)
  • We want a low-fidelity mode where editing an fst in interactive mode when an fsti exists
    • parses, lax-checks and brings into scope the fsti while disabling the warnings such as "no definition", etc.
    • then proceeds to read the chunks sent by Emacs TODO