F* release for POPL 2017

[catalin-hritcu]

Since all deadlines just passed, we should now have enough time to tackle the following cleanup issues (roughly sorted in decreasing order of importance/significance):

Merging branches

• kyod_parser
  Ready to go whenever thje Fsyacc bug is patched

  • blog/wiki post

• c_record_aead (Nik trying)
  Passing regression test in low-level crypto
  Set this for nightly-build only in master
  Will merge at first opportunity

• taramana_local_open, projectors, name_resolution: pull request 'Modul(term)' -> 'Modul.(term)' ; 'Dcon.prm' -> 'Dcon?.prm', 'is_Dcon' -> 'Dcon?' ; improved name resolution #772
  In that order

  • local open: Module.(term) instead of Module (term)
  • Some?.x for projectors
  • Some? for discriminators
  • document non-backwards-compatible syntax changes in the wiki
    see Modules, namespaces and name resolution
  • name resolution with more intuitive scope management

• Improvements based on these syntax changes

  • include (Support include for libraries, to "merge" several libraries into one single namespace #691): branch taramana_include
  • dependency generation (cf. bug Dependency analysis confused by effect name #784 )

Bootstrap

• remove --stratified P1 timeline: end of the 2016
  • Supporting recursive type abbreviations
  • Pushing code through the new type-checker and extraction machinery
• Improving the bootstrap process: P2 by January 15, 2017
  • remove duplicate bootstrap libraries, etc. (nik will start today)
  • use autodeps

Concrete syntax

• pretty-printer (sishtiaq_pp #764) P1 (protz, kenji, tomer, samin)

• finishing the hybrid integration of pprint/F# and pprint/ml including pretty_string and pretty_out_channel (samin)

• Printing the front-end syntax (timeline Jan 15, 2017) We have fstar --indent

• have fstar-indent as a use-case for the new pretty printer -- need to preserve comments (possibly tricky); ideally, hook it up to the emacs mode via m-x indent-region

• manual universe instantiation P1 by end of 2016

• ascription syntax P3 (precedence of <: ) asap (kenji)
  We want (fun x -> e <: t) to mean (fun x -> (e <: t)).

Libraries

• improved libraries P1 Tahina
  • Seq and SeqProperties merged using include
  • List.Tot and ListProperties
  • documented libraries (Documentation of the standard library #273, Improve Documentation #635 ) (using fsdoc syntax, not necessarily producing pretty html):
    • Sequences
    • Lists
• fsdoc (Implement fsdoc #634) Post pretty printer (Samin)

dm4free

• dm4free (Meta Issue for DM4F #753) P1 Kenji
  • All examples in examples/dm4free
  • Fix monadic application in the normalizer
  • Complete relational proofs using dm4free in examples/relational/new/ifcWhile.fst

Z3

• Z3 non-time-based resource limits (Replace Z3 timeouts with machine independent resource limits #767) P1 timeline: two weeks
• Z3 process pool for OCaml P3 (Support for parallel SMT solving ... make --n_cores great again #146, Tomer working on this)
• Resurrect split_cases?

Misc

• positivity (Aseem, see strict positivity check #319) P1

• interactive mode with interfaces (add interface keyword) (Jonathan, seems almost done)

• default effect Tot P1 By Jan 15th (see Top-level effects and module pre- and post-conditions #143 and Behavior of inferred effect arguments without val #581 and Very strange behavior of default effects #623 and Change the default effect to be Tot and namespace insensitive #705 and
  https://github.com/FStarLang/FStar/wiki/Top-level-effects) (Nik)

//val f (x:nat) : nat //f : x:nat -> Tot nat
let f x : nat = mk_ref 0; 0 ~~> let f x : DefaultEffect nat = ...
let f x = (fact y <: Pure nat (requires (y >= 0)) wp)

(e <: t) or (e <: M t wp)
(e <:: t)

confused

Post-release

• Transforming syntax.term to ast.term (post release)

• documented official concrete syntax (post-release)

• switch to sedlex P3 (post-release)

• Integer overloading using FStar.Integers ongoing (post-release)

• Making the heap models uniform (Aseem) ongoing (post-release)

• indexed effects (https://github.com/FStarLang/FStar/wiki/Indexed-effects) (post-release, Nik)

• Polarities: subtyping for datatypes Polarities: subtyping for datatypes #65 ? (post-release)

• F# compatibility (Meta Issue: problems with the F# version of F* (currently lagging behind the OCaml version) #746) P3 nice to have (post-release)

• F* as a driver for the OCaml compiler P2 by February 15, 2017

• Libraries: naming conventions (Towards a naming convention for the standard library? #687), import lemmas from Coq/Lean

• Update Wiki: https://github.com/FStarLang/FStar/wiki/Editing-files-in-the-library

[catalin-hritcu]

Should clarify how this is related to #505 and the past but not completely achieved "Universes Release" milestone (https://github.com/FStarLang/FStar/milestone/3).

[nikswamy]

Can we close this issue now? Perhaps creating separate issues for some of the tasks that are still to be completed. WDYT @catalin-hritcu ?

[catalin-hritcu]

@nikswamy Creating separate issues for things here that are still open and useful then closing this sounds good to me.

[valera-rozuvan]

This issue should definitely be closed. Also, need to update A roadmap for F*. The language is up to v0.9.6.x, and the roadmap is behind (at v0.9.4). What's left to do from the original list of this issue?

@mtzguido , @nikswamy , @aseemr

[catalin-hritcu]

In general, our meta issues have been living forever, but it would be great if some of them could be closed with the remaining tasks turned into separate issues. In this case, I have no clue which ones of these tasks are still useful, but someone working closer on the implementation should know.

As for the roadmap, I've renamed it to A roadmap for F* (Jan Feb 2017) so that it's clearer that that's an old document.

[aseemr]

Closing this issue seems fine to me. There are github issues/wiki pages for most things.