mirror of
https://github.com/Kindelia/Kind.git
synced 2024-09-11 08:55:36 +03:00
chore: improved readme a little bit
This commit is contained in:
parent
668233184f
commit
3f434a1aff
71
README.md
71
README.md
@ -1,7 +1,24 @@
|
|||||||
Kind2
|
<div align="center">
|
||||||
=====
|
|
||||||
|
|
||||||
**Kind2** is a **functional programming language** and **proof assistant**.
|
![banner]
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
[![crates.io][crates.io-badge]][crates.io]
|
||||||
|
[![discord.invite][discord.badge]][discord.invite]
|
||||||
|
![build.badge]
|
||||||
|
|
||||||
|
**Kind** is a **pure functional programming language** and **proof assistant**.
|
||||||
|
|
||||||
|
[Getting started](#getting-started) •
|
||||||
|
[Examples](#examples) •
|
||||||
|
[Installation](#installation)
|
||||||
|
|
||||||
|
</div>
|
||||||
|
|
||||||
|
# Getting started
|
||||||
|
|
||||||
It is a complete rewrite of [Kind1](https://github.com/kindelia/kind-legacy), based on
|
It is a complete rewrite of [Kind1](https://github.com/kindelia/kind-legacy), based on
|
||||||
[HVM](https://github.com/kindelia/hvm), a **lazy**, **non-garbage-collected** and **massively parallel** virtual
|
[HVM](https://github.com/kindelia/hvm), a **lazy**, **non-garbage-collected** and **massively parallel** virtual
|
||||||
@ -11,10 +28,9 @@ unleashes the [inherent parallelism of the Lambda
|
|||||||
Calculus](https://github.com/VictorTaelin/Symmetric-Interaction-Calculus) to become the ultimate programming language of
|
Calculus](https://github.com/VictorTaelin/Symmetric-Interaction-Calculus) to become the ultimate programming language of
|
||||||
the next century.
|
the next century.
|
||||||
|
|
||||||
**Welcome to the inevitable parallel, functional future of computers!**
|
<div align="center"><b>Welcome to the inevitable parallel, functional future of computers! </b></div>
|
||||||
|
|
||||||
Examples
|
## Examples
|
||||||
--------
|
|
||||||
|
|
||||||
Pure functions are defined via equations, as in [Haskell](https://www.haskell.org/):
|
Pure functions are defined via equations, as in [Haskell](https://www.haskell.org/):
|
||||||
|
|
||||||
@ -25,19 +41,6 @@ map a b Nil f = Nil
|
|||||||
map a b (Cons head tail) f = Cons (f head) (map tail f)
|
map a b (Cons head tail) f = Cons (f head) (map tail f)
|
||||||
```
|
```
|
||||||
|
|
||||||
Side-effective programs are written via monads, resembling [Rust](https://www.rust-lang.org/) and [TypeScript](https://www.typescriptlang.org/):
|
|
||||||
|
|
||||||
```javascript
|
|
||||||
// Prints the double of every number up to a limit
|
|
||||||
Main : IO (Result () String) {
|
|
||||||
ask limit = IO.prompt "Enter limit:"
|
|
||||||
for x in (List.range limit) {
|
|
||||||
IO.print "{} * 2 = {}" x (Nat.double x)
|
|
||||||
}
|
|
||||||
return Ok ()
|
|
||||||
}
|
|
||||||
```
|
|
||||||
|
|
||||||
Theorems can be proved inductively, as in [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) and [Idris](https://www.idris-lang.org/):
|
Theorems can be proved inductively, as in [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) and [Idris](https://www.idris-lang.org/):
|
||||||
|
|
||||||
```javascript
|
```javascript
|
||||||
@ -49,8 +52,7 @@ black_friday_theorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (black_friday_
|
|||||||
|
|
||||||
For more examples, check the [Wikind](https://github.com/kindelia/wikind).
|
For more examples, check the [Wikind](https://github.com/kindelia/wikind).
|
||||||
|
|
||||||
Usage
|
# Installation
|
||||||
-----
|
|
||||||
|
|
||||||
First, install [Rust](https://www.rust-lang.org/tools/install) first, then enter:
|
First, install [Rust](https://www.rust-lang.org/tools/install) first, then enter:
|
||||||
|
|
||||||
@ -58,13 +60,6 @@ First, install [Rust](https://www.rust-lang.org/tools/install) first, then enter
|
|||||||
cargo install kind2
|
cargo install kind2
|
||||||
```
|
```
|
||||||
|
|
||||||
### Warning:
|
|
||||||
New versions probably are not in `cargo`, so you can install the current version of kind2 by following these instructions:
|
|
||||||
|
|
||||||
1. Install Rust Nightly Toolchain
|
|
||||||
2. Clone the repository
|
|
||||||
3. `cargo install --path crates/kind-cli --force`
|
|
||||||
|
|
||||||
Then, use any of the commands below:
|
Then, use any of the commands below:
|
||||||
|
|
||||||
Command | Usage | Note
|
Command | Usage | Note
|
||||||
@ -72,19 +67,16 @@ Command | Usage | Note
|
|||||||
Check | `kind2 check file.kind2` | Checks all definitions.
|
Check | `kind2 check file.kind2` | Checks all definitions.
|
||||||
Eval | `kind2 eval file.kind2` | Runs using the type-checker's evaluator.
|
Eval | `kind2 eval file.kind2` | Runs using the type-checker's evaluator.
|
||||||
Run | `kind2 run file.kind2` | Runs using HVM's evaluator, on Rust-mode.
|
Run | `kind2 run file.kind2` | Runs using HVM's evaluator, on Rust-mode.
|
||||||
To-HVM | `kind2 to-hvm file.kind2` | Generates a [.hvm](https://github.com/kindelia/hvm) file. Can then be compiled to C.
|
To-HVM | `kind2 to-hvm file.kind2` | Generates a [.hvm](https://github.com/kindelia/hvm) file. Can then be compiled to a rust crate using HVM.
|
||||||
To-KDL | `kind2 to-kdl file.kind2` | Generates a [.kdl](https://github.com/kindelia/kindelia) file. Can then be deployed to [Kindelia](https://github.com/kindelia/kindelia).
|
To-KDL | `kind2 to-kdl file.kind2` | Generates a [.kdl](https://github.com/kindelia/kindelia) file. Can then be deployed to [Kindelia](https://github.com/kindelia/kindelia).
|
||||||
|
|
||||||
Executables can be generated via HVM:
|
The rust crate can be generated via HVM:
|
||||||
|
|
||||||
```
|
```
|
||||||
kind2 to-hvm file.kind2
|
kind2 to-hvm file.kind2 > file.hvm
|
||||||
hvm compile file.hvm
|
hvm compile file.hvm
|
||||||
clang -O2 file.c -o file
|
|
||||||
./file
|
|
||||||
```
|
```
|
||||||
|
|
||||||
|
|
||||||
---
|
---
|
||||||
|
|
||||||
- If you need support related to Kind, email [support.kind@kindelia.org](mailto:support.kind@kindelia.org)
|
- If you need support related to Kind, email [support.kind@kindelia.org](mailto:support.kind@kindelia.org)
|
||||||
@ -92,3 +84,14 @@ clang -O2 file.c -o file
|
|||||||
- For Feedbacks, email [kind@kindelia.org](mailto:kind@kindelia.org)
|
- For Feedbacks, email [kind@kindelia.org](mailto:kind@kindelia.org)
|
||||||
|
|
||||||
- To ask questions and join our community, check our [Discord Server](https://discord.gg/kindelia).
|
- To ask questions and join our community, check our [Discord Server](https://discord.gg/kindelia).
|
||||||
|
|
||||||
|
|
||||||
|
[banner]: ./img/banner.png
|
||||||
|
|
||||||
|
[crates.io-badge]: https://img.shields.io/crates/v/kind2?style=flat-square
|
||||||
|
[crates.io]: https://crates.io/crates/zoxide
|
||||||
|
|
||||||
|
[discord.badge]: https://img.shields.io/discord/912426566838013994?style=flat-square
|
||||||
|
[discord.invite]: https://discord.gg/kindelia
|
||||||
|
|
||||||
|
[build.badge]: https://img.shields.io/github/actions/workflow/status/kindelia/kind/ci.yml?style=flat-square
|
BIN
img/banner.png
Normal file
BIN
img/banner.png
Normal file
Binary file not shown.
After Width: | Height: | Size: 655 KiB |
Loading…
Reference in New Issue
Block a user