Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(readme): add links #657

Merged
merged 4 commits into from
May 13, 2024
Merged

feat(readme): add links #657

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
456f1d2
feat(readme): add a header with all relevant links
W95Psp May 13, 2024
60fc0cc
feat(readme): add a `Learn more` section, move examples there
W95Psp May 13, 2024
96baa4a
feat(readme): add `pro-verif`
W95Psp May 13, 2024
e0b0f91
feat(readme): hack on hax: "internal" docs link
W95Psp May 13, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 22 additions & 7 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,11 @@
<p align="center">
<a href="https://hacspec.org/">🌐 Website</a> |
<a href="https://hacspec.org/book">📖 Book</a> |
<a href="https://hacspec.org/blog">📝 Blog</a> |
<a href="https://hacspec.zulipchat.com/">💬 Zulip</a> |
<a href="https://hacspec.org/hax/">🛠️ Internal docs</a>
</p>

# Hax

hax is a tool for high assurance translations that translates a large subset of
Expand All @@ -12,15 +20,24 @@ standard library, to write succinct, executable, and verifiable specifications i
Rust.
These specifications can be translated into formal languages with hax.

## Learn more

Here are some resources for learning more about hax:
- [Book](https://hacspec.org/book) (work in progress)
+ [Quick start](https://hacspec.org/book/quick_start/intro.html)
+ [Tutorial](https://hacspec.org/book/tutorial/index.html)
- [Examples](examples/): the [examples directory](examples/) contains
a set of examples that show what hax can do for you.

## Usage
Hax is a cargo subcommand.
The command `cargo hax` accepts the following subcommands:
* **`into`** (`cargo hax into BACKEND`): translate a Rust crate to the backend `BACKEND` (e.g. `fstar`, `coq`).
* **`json`** (`cargo hax json`): extract the typed AST of your crate as a JSON file.

Note:
* `BACKEND` can be `fstar`, `coq` or `easycrypt`. `cargo hax into
--help` gives the full list of supported backends.
* `BACKEND` can be `fstar`, `coq`, `easycrypt` or `pro-verif`. `cargo hax into --help`
gives the full list of supported backends.
* The subcommands `cargo hax`, `cargo hax into` and `cargo hax into
<BACKEND>` takes options. For instance, you can `cargo hax into
fstar --z3rlimit 100`. Use `--help` on those subcommands to list
Expand Down Expand Up @@ -91,12 +108,10 @@ Quicklinks:
- [🔨 Rejected rust we want to support](https://github.com/hacspec/hax/issues?q=is%3Aissue+is%3Aopen+label%3Aunsupported-rust+-label%3Awontfix%2Cwontfix-v1);
- [💭 Rejected rust we don't plan to support in v1](https://github.com/hacspec/hax/issues?q=is%3Aissue+is%3Aopen+label%3Aunsupported-rust+label%3Awontfix%2Cwontfix-v1).

## Examples

There's a set of examples that show what hax can do for you.
Please check out the [examples directory](examples/).

## Hacking on Hax
The documentation of the internal crate of hax and its engine can be
W95Psp marked this conversation as resolved.
Show resolved Hide resolved
found [here](https://hacspec.org/hax/).

### Edit the sources (Nix)

Just clone & `cd` into the repo, then run `nix develop .`.
Expand Down
Loading