Feature requests from 2014-04-17 discussion

[cpitclaudel]

• [x] Jump to definition in other window
• [x] Pick the reduction rules to apply in "compute"
• [x] Jump to dependencies of current file
• [ ] Simple form of "destruct" that just inserts a single match
• [x] Jump to the "alternate" location of an error
• [x] List of option values

[cpitclaudel]

Jump to the "alternate" location of an error

@fournet Do you have a small example where multiple locations being reported for an error, and it's useful to be able to visit all locations?

[s-zanella]

While you're at it, it would be really useful if describe-repl could print the current value of interactively-settable options (https://github.com/FStarLang/FStar/wiki/Pragmas-%28%23set-options%2C-%23reset-options%29)

[cpitclaudel]

@s-zanella Happy to add support for this on the Emacs side. Do you want to volunteer an F*-side patch (presumably on top of the currently-unmerged PR)?

[s-zanella]

Sure, I'll prepare a patch for https://github.com/FStarLang/FStar/pull/995

[cpitclaudel]

Wonderful, thanks! I'll update the UI side very soon (the patch looks great)

[cpitclaudel]

I extended your patch to include default values, too, and pushed the UI. Let me know if it works! The keybinding is C-c C-s h o, or M-x fstar-options.

[s-zanella]

Works and looks great. Thanks!

[cpitclaudel]

Great, thanks for the suggestion and the patch!

[cpitclaudel]

Feel free to comment on the rest of the PR, of course.

[s-zanella]

Nit: the buffer that shows the list of options is called *fstar: dependencies*

[cpitclaudel]

Thanks, fixed.