2022-03-28 15:03:21 +02:00
|
|
|
#+title: :lang fstar
|
|
|
|
|
#+subtitle: (Dependent) types and (monadic) effects and Z3
|
|
|
|
|
#+created: February 02, 2020
|
|
|
|
|
#+since: 21.12.0 (#2473)
|
2021-10-16 01:28:32 +02:00
|
|
|
|
|
|
|
|
* Description :unfold:
|
2020-02-02 10:40:25 -05:00
|
|
|
This module adds [[https://fstar-lang.org/][F*]] support, powered by [[https://github.com/FStarLang/fstar-mode.el][fstar-mode.el]].
|
2020-02-02 14:08:55 -05:00
|
|
|
|
2021-10-16 01:28:32 +02:00
|
|
|
- Syntax highlighting
|
|
|
|
|
- Interactively process F* files one definition at a time
|
|
|
|
|
- Query the running F* process to look up definitions, documentation, and
|
2020-02-02 14:08:55 -05:00
|
|
|
theorems
|
|
|
|
|
|
|
|
|
|
** Maintainers
|
2021-10-16 01:28:32 +02:00
|
|
|
- [[doom-user:][@tchajed]]
|
|
|
|
|
|
|
|
|
|
[[doom-contrib-maintainer:][Become a maintainer?]]
|
|
|
|
|
|
|
|
|
|
** Module flags
|
|
|
|
|
/This module has no flags./
|
|
|
|
|
|
|
|
|
|
** Packages
|
|
|
|
|
- [[doom-package:][fstar-mode]]
|
|
|
|
|
|
|
|
|
|
** Hacks
|
|
|
|
|
/No hacks documented for this module./
|
|
|
|
|
|
|
|
|
|
** TODO Changelog
|
|
|
|
|
# This section will be machine generated. Don't edit it by hand.
|
|
|
|
|
/This module does not have a changelog yet./
|
2020-02-02 14:08:55 -05:00
|
|
|
|
2021-10-16 01:28:32 +02:00
|
|
|
* Installation
|
|
|
|
|
[[id:01cffea4-3329-45e2-a892-95a384ab2338][Enable this module in your ~doom!~ block.]]
|
2020-02-02 14:08:55 -05:00
|
|
|
|
2021-10-16 01:28:32 +02:00
|
|
|
This module requires [[https://github.com/FStarLang/FStar/blob/master/INSTALL.md][F*]].
|
2020-02-02 14:08:55 -05:00
|
|
|
|
2021-10-16 01:28:32 +02:00
|
|
|
While ~fstar-mode~ supports the latest release of F*, you may have a better
|
|
|
|
|
experience installing a more recent version from source.
|
|
|
|
|
|
|
|
|
|
** macOS
|
|
|
|
|
#+begin_src sh
|
2020-02-02 14:08:55 -05:00
|
|
|
brew install fstar
|
2021-10-16 01:28:32 +02:00
|
|
|
#+end_src
|
|
|
|
|
|
|
|
|
|
** Arch Linux
|
|
|
|
|
~fstar~ is available in the AUR:
|
|
|
|
|
#+begin_src sh
|
2020-02-02 14:08:55 -05:00
|
|
|
yaourt -S fstar
|
2021-10-16 01:28:32 +02:00
|
|
|
#+end_src
|
2020-02-02 14:08:55 -05:00
|
|
|
|
2021-10-16 01:28:32 +02:00
|
|
|
* TODO Usage
|
|
|
|
|
#+begin_quote
|
|
|
|
|
🔨 This module has no usage documentation yet. [[doom-contrib-module:][Write some?]]
|
|
|
|
|
#+end_quote
|
2020-02-02 14:08:55 -05:00
|
|
|
|
2021-10-16 01:28:32 +02:00
|
|
|
* TODO Configuration
|
|
|
|
|
#+begin_quote
|
|
|
|
|
🔨 This module has no configuration documentation yet. [[doom-contrib-module:][Write some?]]
|
|
|
|
|
#+end_quote
|
2020-02-02 14:08:55 -05:00
|
|
|
|
|
|
|
|
* Troubleshooting
|
2021-10-16 01:28:32 +02:00
|
|
|
[[doom-report:][Report an issue?]]
|
|
|
|
|
|
|
|
|
|
- If you're having trouble getting F* to start correctly, you may need to
|
|
|
|
|
configure a few variables in ~fstar-mode~; see its [[https://github.com/FStarLang/fstar-mode.el][README]] for more details.
|
|
|
|
|
|
|
|
|
|
* Frequently asked questions
|
|
|
|
|
/This module has no FAQs yet./ [[doom-suggest-faq:][Ask one?]]
|
|
|
|
|
|
|
|
|
|
* TODO Appendix
|
|
|
|
|
#+begin_quote
|
|
|
|
|
🔨 This module has no appendix yet. [[doom-contrib-module:][Write one?]]
|
|
|
|
|
#+end_quote
|
