forked from omelkonian/agda-minimal-backend
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
1 changed file
with
19 additions
and
17 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,39 +1,41 @@ | ||
# Agda backend for Rust | ||
# Agda backend for Rust | ||
|
||
## Working with source code | ||
|
||
* Starting continuous compilation loop | ||
* Compile Agda code to Rust | ||
|
||
```sh | ||
ghcid | ||
cabal run -- agda2rust --help | ||
|
||
cabal run -- agda2rust test/Hello.agda | ||
cabal run -- agda2rust test/Test.agda | ||
``` | ||
|
||
* Build | ||
* Testing compiled Rust code | ||
|
||
```sh | ||
cabal build all | ||
rustc --crate-type=lib test/Hello.rs | ||
rustc --crate-type=lib test/Test.rs | ||
``` | ||
|
||
* Compile Rust code | ||
# Working with source code | ||
|
||
The `test/` directory contains an example compilation of `Test.agda` to `Test.rs` | ||
and `Hello.agda` to `Hello.rs`: | ||
* Starting continuous compilation loop | ||
|
||
```sh | ||
cabal run -- agda2rust --help | ||
cabal run -- agda2rust test/Hello.agda | ||
cabal run -- agda2rust test/Test.agda | ||
ghcid | ||
``` | ||
* Testing compiled Rust code | ||
|
||
* Build | ||
|
||
```sh | ||
cd test | ||
rustc --crate-type=lib test/Hello.rs | ||
rustc --crate-type=lib test/Test.rs | ||
cabal build all | ||
``` | ||
|
||
* Run tests | ||
|
||
```sh | ||
cabal test all | ||
``` | ||
|
||
* CI | ||
|
||
Unit tests and compiling sample Agda code to Rust are [run on CI](https://github.com/lemastero/agda2rust/blob/master/.github/workflows/haskell.yml). |