Meta-F* wish list - Githubissues

FStarLang / FStar

A Proof-oriented Programming Language

https://fstar-lang.org

Apache License 2.0

2.67k stars 231 forks source link

Meta-F* wish list #1419

Open nikswamy opened 6 years ago

nikswamy commented 6 years ago

[ ] Better names in interactive mode displays
[ ] A tactic REPL
[x] From #1418: Allowing tactics to control type inference, in particular how implicits are instantiated? (@mtzguido: marked it done by meta args)
[ ] Specifying a tactic independently from the assertion that it operates on. Something like let f x = ... assert p by t .... where t = ...
[x] More compilation of tactics, including canonicalizers esp. applied to sep_auto
[ ] induction tactic
[x] Automate inspect/pack as coercions? (@mtzguido: some work done in a local branch)
[ ] Update tutorial
[ ] Do some profiling to see what we can improve, both interpreted and compiled
[x] Generating inductives at the top level? @lastland

catalin-hritcu commented 6 years ago

Regarding the compilation of the canonizer (branch c_canon-native) @victor-dumitrescu has the latest status, but last time we looked at it together when we were leaving Seattle compilation was working but we hit a nasty issue: the compiled version had very different reduction behavior compared to the interpreted one, which could at least in part be a consequence of different reduction strategies (lazy vs cbv).

We also realized that with the curent implementation functions like canon and Xdenote are not run natively. Some of them could be separately compiled as a plugin but AFAIK not all, plus some of the manual unfolding would need to be turned off ...

mtzguido commented 6 years ago

[ ] Make all metaprogramming primitives in ulib/ have a clear prefix (m_?) giving direct access to a function in the typechecker. Currently we have some like apply, which take an extra argument (a bool) in the typechecker and two versions of it are exposed in ulib/ (apply and apply_raw). It's the interpreter adding true or false to the calls. That's a mess, let's just have a single m_apply taking the bool and do whatever we want with it in ulib/.
[x] In particular, do not define a plain fail in tactics since it shadows Pervasives.fail. and that's very annoying.
[ ] Rename Tac (& friends) to Meta?