-
Notifications
You must be signed in to change notification settings - Fork 232
Some day, maybe
A bunch of F* engineering projects:
F*'s extraction should produce [@warning "-8"]-style annotations to disable spurious warnings (instead of our current _tags file for the compiler)
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)
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.
Clément will chat with François and Frédéric about this.
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.
https://github.com/FStarLang/FStar/issues/1151
Change the parser to accept fs and fsi in --MLish mode. Don't copy the files to a separate u_boot_fsts/ folder when building.
https://github.com/FStarLang/FStar/issues/1146
We currently have multiple stacks used for backtracking, including one in the SMT solver, one in the typechecker, one in ToSyntax, and one in the interactive mode. Additionally, we have separate notions of pushing, marking (along with popping, committing marks, and resetting marks). It would be nice to simplify these, and have a single backtracking stack in F*.
This would also be a good occasion to start using pure maps (psmap, pimap) rather than imperative maps with copies.
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
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.
Use this to turn off Adding an implicit 'assume new' warnings while compiling F*'s compiler.
See also "add rich types for errors", which would subsume this.