-
Notifications
You must be signed in to change notification settings - Fork 232
Roadmap for usable interfaces
Jonathan Protzenko edited this page Jan 4, 2017
·
3 revisions
- The Emacs mode should send the complete path to F* so that it can perform the initial loading & dependency analysis properly
- Why don't we rely on Aseem's dependencies-as-you-go feature?
- This would solve the problem of one launching Emacs on a file that is not in the current directory (currently a broken scenario)
- We still may want a warning that if Emacs is in dir1 and launches F* on
dir2/Foo.fst
anddir2
is not in the include path, then this is sketchy (need to send the current working directory to F*, then)
- We need
--interactive ==> --partial
- We need to fix the broken dependency arrow from
fsti
to `fst`` - We want a low-fidelity mode where editing an
fst
in interactive mode when anfsti
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
- parses, lax-checks and brings into scope the