-
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.
Use this to turn off Adding an implicit 'assume new' warnings while compiling F*'s compiler.
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.
- Change the file extension check to allow
fsandfsi - Teach fstar-mode how to pass the right
--includes to F* (fstar-subp-prover-args-for-compiler-hacking) - Change the build process:
- Leave the .fs files in place instead of copying them
- Teach F* to use them
- Update the Makefile and fstar-mode to include these .fs folders instead of
u_boot_fstsandboot_fstis
- Make sure things work
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*.
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.