-
Notifications
You must be signed in to change notification settings - Fork 232
Some day, maybe
A bunch of F* engineering projects:
Annotate each warning with an identifier. Include the identifier in messages, and make it possible do disable specific warnings from the command line. Add disabled-by-default warnings under -Wall.
Change the parser to accept fs and
Add a rich type for errors, and propagate that type into the interactive mode. For example, instead of Expected "int", got ""A" ^ "B"" of type "string", say UnificationError ("Expected '%s', got '%s' of type '%s'", Code "int", Code "\"A\" ^ \"B\""). This lets the IDE highlight the code snippets, for example.
An extension of this would be to associate lists of ranges to errors, instead of single errors. F*-mode can already jump to related errors, but we currently have at most one, and it's sometimes parsed from the error message text (Also see:). This would make it much nicer (we'd probably to highlight related ranges when the point is on an error)
In addition to hints, record a hash of unsat SMT queries in a cache, and admit queries that can be found in the cache. Useful for CI and potentially for interactive developments (with such a system, issuing one query per assert might be faster than producing one large VC, due to caching). https://github.com/FStarLang/FStar/issues/1140
Should be a relatively easy extension of FStar.Interactive.Ide.fs. Overwriting definitions might be tricky. Same for loading modules on the fly (dependencies are currently (2017-07) loaded all at once when the file is first parsed). See next item.
In interactive mode, defer dependency analysis and loading to when each dependency is first encountered. Instead of parsing the whole file and loading all dependencies, only load a dependency after receiving the first chunk mentioning it (through an open, and include, or a qualified reference to a symbol).
This would remove the requirement for interactive files to be syntactically valid when an editing session is started, and it would get rid of annoying errors about modules not being found (and it would save the time spent reprocessing everything after reloading a module, too).
Enrich the parser with error states, and use these to do contextual completion, type-at-point info with partial terms, eldoc-style argument type suggestion, for indentation driven by F*-mode.
This would let you run info queries (type at point etc) while a long-running proof is in progress.
Decide on a standard code layout format, and implement a tool to apply it consistently.