This PR:
* Updates the anomalib nock stdlib to the latest head of
`artem/juvix-node-integration-v0.28` containing the latest testnet
fixes.
* Re-enables the Anoma resource machine builtins tests
* Closes#3201
* As a side effect, aliases can now only be used after they are declared
(but they can still forward-reference identifiers, except the
non-recursive definitions or other aliases).
Now it is allowed to use field puns in record updates. E.g.
```
type R :=
mkR@{
a : Nat;
b : Nat;
c : Nat;
};
example : R :=
let
z :=
mkR@{
a := 0;
b := 0;
c := 0;
};
a := 6;
in z@R{a} -- the field `a` is updated to 6
```
1. Closes#3192. The first pipe is ensured in a multi-clause lambda.
3. Bugfix: Pragmas are now properly printed for deriving statements.
Previously they were never printed.
4. Record types are always declared in a new line, even if they have a
single constructor and fit in a line. I think this change improves
readability.
```
-- before
type Eq A := mkEq@{builtin isEqual eq : A -> A -> Bool};
-- after
type Eq A :=
mkEq@{
builtin isEqual
eq : A -> A -> Bool;
};
```
5. I've formatted the stdlib
(https://github.com/anoma/juvix-stdlib/pull/150).
6. I've refactored some code related to adding the first pipe so that it
is reused for cases, lambdas and types.
7. Now `ConstructorDef` has a proper `PrettyCode` instance and does not
need to be passed a bool indicating whether it is the only constructor
in a definition.
This mode is for tests that must run on the Anoma Node / Client. These
tests contain calls that are crashes in AnomaLib nock file and must
therefore be jetted.
With this changed the contents of test085 (resource machine builtins)
can be uncommnented. However it currently fails, unexpectedly on the
node.
* Closes#3186
* Changes the generated code for derived Eq instances to define a local
recursive function with a let instead of a lambda. This is necessary,
because otherwise an indirection is generated on each recursive call --
instance resolution inserts the instance identifier, which then is
matched on and the function for the recursive call extracted instead of
being called directly. This cannot be (easily) optimized in Core
because, to avoid looping in the compiler, in general one cannot do
inlining of recursive functions.
* Minor improvements to the inlining optimization and the main
optimization phase: do inlining before specialization and more liberal
rules for heuristic case value inlining.
This PR makes changes to make our Anoma client CLI commands compatible
with the https://github.com/anoma/anoma/tree/testnet-01 branch.
We must now capture the Anoma client node_id on start because some
endpoints (e.g mempool submit) require this node id in the request.
I'm using
[Effectful.Environment](https://hackage.haskell.org/package/effectful-2.5.0.0/docs/Effectful-Environment.html)
to interact with environment variables as it avoids use of `IOE`.
In a separate PR we should replace all usages of `System.Environment`
with `Effectful.Environment` but I've left existing usages of
`System.Environment` in place for the time being.
Add `juvix dev anoma prove`
This is similar to `juvix dev nockma run`.
The difference is that the managed client is used and it outputs the
result as a jammed file.
## CLI docs
```
The prove command submits a Nockma program to the Anoma.Protobuf.NockService.Prove gRPC endpoint.
By default, the gRPC request is made to the client that is started by juvix dev anoma start.
Use the -c/--config option to use a different Anoma client.
The config file format is:
url: <ANOMA_CLIENT_URL>
port: <ANOMA_CLIENT_GRPC_PORT>
The gRPC response (a Nockma program) is saved to a file named <input>.proved.nockma, where <input> is the base name of the input file.
Use the -o/--output option to specify a custom output filename.
If the program generates traces, they will be written to standard output.
Usage: juvix dev anoma prove NOCKMA_FILE [--args ARGS_FILE]
[-c|--config CONFIG_FILE] [-o|--output OUTPUT_FILE]
Submit a Nockma program to Anoma.Protobuf.NockService.Prove
Available options:
NOCKMA_FILE Path to a .nockma file
--args ARGS_FILE Path to a file containing args. The args file should
contain a list (i.e. to pass 2 and [1 4] as args, the
contents should be [2 [1 4] 0]).
-c,--config CONFIG_FILE A path to an Anoma client configuration file
-o,--output OUTPUT_FILE Path to output file
-h,--help Show this help text
```
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* Closes#3118
* Allows patterns on the left-hand sides of definitions. To avoid
clashes with constructor names, the patterns need to be enclosed in
parentheses or have the form `n@...`. A standalone symbol `x` in a
definition `x := ...` is always interpreted as an identifier even if
there exists a constructor `x`.
* Left-hand side patterns are desugared in the translation from Concrete
to Internal. If the inductive type has more than one constructor,
non-exhaustive pattern matching error will later be given by the pattern
matching compiler.
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
This PR adds the `juvix dev anoma {start, stop, status}` commands to
manage a running Anoma client.
The motivation for this is that we can add additional commands (e.g
`indexer`, `prove`, `(mempool)-submit`) which interact with the
persistent Anoma client.
`juvix dev anoma start` now writes a configuration file in
`<juvix_config>/anoma-client/config.yaml` which contains the host URL
and
port of the started Anoma client and the pid of the Anoma client
process.
For example:
config.yaml
```
host:
port: 58922
url: localhost
pid: 75299
```
The `anoma stop` command kills the Anoma client and the `anoma status`
command shows the config of the currently running client.
There can be at most one Anoma client running when using this mechanism.
## Dependency
This PR adds a new dependency on the `unix` package. This is used for
APIs to send signals to processes.
## CLI docs
### `juvix dev anoma`
```
Usage: juvix dev anoma COMMAND
Subcommands related to the Anoma client
Available options:
-h,--help Show this help text
Available commands:
start Start an Anoma client
status Show the status of the Anoma client
stop Stop the Anoma client
```
### `juvix dev anoma start`
```
Usage: juvix dev anoma start --anoma-dir ANOMA_DIR [-g|--foreground]
[-f|--force]
Start an Anoma client
Available options:
--anoma-dir ANOMA_DIR Path to anoma repository
-g,--foreground Start the client in the foreground
-f,--force Forcefully start a client, terminating any currently
running client if necessary
-h,--help Show this help text
```
### `juvix dev anoma status`
```
Usage: juvix dev anoma status
Show the status of the Anoma client
Available options:
-h,--help Show this help text
```
### `juvix dev anoma stop`
```
Usage: juvix dev anoma stop
Stop the Anoma client
Available options:
-h,--help Show this help text
```
This pr adds automatic implementation of `Eq` instances for inductive
types. To create such an instance the user will use the same syntax as a
regular instance with two differences.
1. It is prefixed with the `deriving` keyword.
2. It has no body.
E.g.
```
deriving instance
eqProductI {A B} {{Eq A}} {{Eq B}} : Eq (Pair A B);
```
This desugars into an instance that returns true when the constructors
match and all arguments are equal according to their respective
instances. There is no special handling of type errors occurring in the
generated code. I.e. if the user forgets a necessary instance argument
in the type signature, a type error will occur in the generated code.
## Stdlib PR
- https://github.com/anoma/juvix-stdlib/pull/148
# Future work
* In the future we should look at
https://www.dreixel.net/research/pdf/gdmh_nocolor.pdf
* See also:
https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/generic-deriving
---------
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
This PR sets `std_in` to `NoStream` on the Anoma client process.
https://hackage.haskell.org/package/process-1.6.25.0/docs/System-Process.html#t:StdStream
We do not read from the Anoma client process stdin so we do not need to
open a handle to stdin.
This fixes an issue where the Anoma client stdin does not get cleaned up
correctly on exit which causes subsequent input to the terminal to be
corrupted.
* Closes#2990
* Allows type signatures for constructors, record fields and axioms to
have the same form as in function definitions, e.g.,
```
field {A} {{M A}} (arg1 arg2 : A) : List A
```
* For constructors, this introduces an ambiguity between record and GADT
syntax with names. For example,
```
ctr {
A : Type
}
```
can be confused by the parser with initial part of GADT type signature:
```
ctr {A : Type} : A -> C A
```
For now, this is resolved by preferring the record syntax. Hence, it's
currently not possible to use type signatures with implicit arguments
for constructors. Ultimately, the `@` in record syntax should be made
mandatory, which would resolve the ambiguity:
```
ctr@{
A : Type
}
```
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
This PR:
1. Adds a new interpretation for the Anoma effect, which makes gRPC
calls to an existing Anoma client instead of spawning a new one.
2. Adds a new `nockma run` mode, `with-client`, which can be used to run
an Anoma program against a running Anoma client, using its URL and gRPC
port.
3. separates the `nockma run` command into subcommands.
CLI docs:
## `nockma run`
```
Usage: juvix dev nockma run COMMAND
Subcommands used to run an Anoma program. Use with artefacts obtained from
compilation with the anoma target
Available options:
-h,--help Show this help text
Available commands:
builtin-evaluator Run with the builtin Nockma evaluator
ephemeral-client Run with an ephemeral Anoma client
with-client Run with a running Anoma client
```
### `with-client`
```
Usage: juvix dev nockma run with-client
NOCKMA_FILE [--args ARGS_FILE] (-p|--grpc-port PORT) [--url URL]
Run with a running Anoma client
Available options:
NOCKMA_FILE Path to a .nockma file
--args ARGS_FILE Path to file containing args. The args file should
contain a list (i.e. to pass 2 and [1 4] as args, the
contents should be [2 [1 4] 0]).
-p,--grpc-port PORT The GRPC port of a running Anoma client
--url URL The URL of a running Anoma client. default: localhost
-h,--help Show this help text
```
### `ephemeral-client`
```
Usage: juvix dev nockma run ephemeral-client
NOCKMA_FILE [--args ARGS_FILE] --anoma-dir ANOMA_DIR
Run with an ephemeral Anoma client
Available options:
NOCKMA_FILE Path to a .nockma file
--args ARGS_FILE Path to file containing args. The args file should
contain a list (i.e. to pass 2 and [1 4] as args, the
contents should be [2 [1 4] 0]).
--anoma-dir ANOMA_DIR Path to anoma repository
-h,--help Show this help text
```
### `builtin-evaluator`
```
Usage: juvix dev nockma run builtin-evaluator
NOCKMA_FILE [--args ARGS_FILE] [--profile]
Run with the builtin Nockma evaluator
Available options:
NOCKMA_FILE Path to a .nockma file
--args ARGS_FILE Path to file containing args. The args file should
contain a list (i.e. to pass 2 and [1 4] as args, the
contents should be [2 [1 4] 0]).
--profile Report evaluator profiling statistics
-h,--help Show this help text
```
* Closes#3141
* Adds the `latte-light` theme with lighter background and makes it the
default. This is a bit subjective, but in my opinion the light theme
should not have a background darker than the browser window pane. It
should be close to white.
This PR removes `GetAnomaProcess` from the Anoma effect.
Use the `launchAnoma` function to start a persistent Anoma client /
server (used by `juvix dev anoma node`).
Other changes:
* It's no longer necessary to pass the protobuf files to `grpcurl`
because the Anoma client now supports gRPC reflection.
* We pass the elixir start command to `mix` via `-e` argument instead of
using a temporary file.
The purpose for this change is that we I want to add an interpreter for
Anoma that makes gRPC calls to an exisitng Anoma client.
`GetAnomaProcess` has no meaning for this interpreter.
The `from` and `to` long options for `juvix dev nockma encode` were
mislabelled. `from` should be the source encoding and `to` should be the
target encoding.
* Closes#3147
When we call a function that is currently being defined (there may be
several such due to nested local definitions), we add a reflexive edge
in the call map instead of adding an edge from the most nested
definition. For example, for
```juvix
go {A B} (f : A -> B) : List A -> List B
| nil := nil
| (elem :: next) :=
let var1 := f elem;
var2 := go f next;
in var1 :: var2;
```
we add an edge from `go` to the recursive call `go f next`, instead of
adding an edge from `var2` to `go f next` as before.
This makes the above type-check.
The following still doesn't type-check, because `next'` is not a
subpattern of the clause pattern of `go`. But this is a less pressing
problem.
```juvix
go {A B} (f : A -> B) : List A -> List B
| nil := nil
| (elem :: next) :=
let var1 := f elem;
var2 (next' : List A) : List B := go f next';
in myCons var1 (var2 next);
```
This PR:
1. Fixes the compilation of the sha256 builtin anoma lib call
A sha256 hash is 32 bytes long, not 64 bytes. This number is used when
constructing the ByteArray representation (i.e `[length payload]` cell)
of the output of Anoma stdlib sha256 call. The Anoma stdlib sha256 call
just returns the atom payload.
2. Fixes the evaluation of the sha256 stdlib call
Previously we were converting the sha256 hash bytestring to Base16
format. This is convenient when displaying the ByteString hash. However
the Anoma nock interpreter outputs the raw bytes so we must change the
builtin evaluator to match this behaviour.
After these fixes we can re-enable the test084 anoma compilation test.
This PR changes how we launch the Anoma Client to avoid a bug with
linking cryptographic APIs.
libsodium cryptographic APIs like sign-detached cannot currently be
called from within the Anoma node or client binaries. Until this is
solved we must start both the node and client from the elixir REPL.
Previously we were starting the node using the REPL and the client using
the binary.
This commit changes the `start.exs` script we were using to start the
node to now start both a node and a client.
After this change we can enable Anoma compilation test `test077`.
The output of `juvix dev anoma node --anoma-dir ANOMA_DIR` is now:
```
Anoma node and client successfully started
Listening on port 51748
```
The issue with alpine ncurses packaging has been fixed upstream and the
ghc-musl containers have been rebuilt. Therefore we can resume using the
tagged releases of the ghc-musl container.
https://github.com/benz0li/ghc-musl/issues/10
Thanks @benz0li for help with diagnosing and fixing this issue.
Co-authored-by: Olivier Benz <olivier.benz@b-data.ch>
Support for emacs
[nockma-mode](https://github.com/anoma/juvix-mode/pull/25). The list of
features is given in the link.
It adds the following commands:
1. `juvix dev nockma ide check`. Parses a nockma file (used by flycheck
only).
2. `juvix dev nockma ide highlight`. Highlights a nockma file.
3. `juvix dev nockma ide rules`. Shows all evaluation rules properly
highlighted in emacs.
- Fixes#3030
The `ComputeTypeInfo` transformation was incorrectly assuming that the
type of the body couldn't refer to the let item. When inferring the type
of a let, we now inline the let item(s) into the type of the body.
```
NLet Let {..} ->
let bodyTy = Info.getNodeType _letBody
in subst (_letItem ^. letItemValue) bodyTy
```
The purpose of this release is to add support for the `--vscode` flag,
required by an update to the juvix vscode extension.
* https://github.com/anoma/juvix/pull/3162
* https://github.com/anoma/vscode-juvix/pull/153
This PR updates:
- [x] Package version
- [x] Smoke test
The CHANGELOG generator we use:
https://github.com/github-changelog-generator/github-changelog-generator
has stopped working with errors like the following:
```
Warning: PR 3148 merge commit was not found in the release branch or tagged git history and no rebased SHA comment was found
```
So we'll defer populating the CHANGELOG summary until after the release.
* Add a `--vscode` option which causes the error messages to be printed
without newlines, in a way compatible with the problem matcher of the
VSCode extension
* Related VSCode extension PR:
https://github.com/anoma/vscode-juvix/pull/153
This pr adds support for getting traces from the anoma node.
I've updated the test suite so that tests that were disabled because of
traces are now being run.
There are a few tests that require atention:
1. `test028`: Gives the wrong answer.
2. `test084`: Gives the wrong answer.
4. `test074`: Expected to fail because it uses scry.
5. `test086`: Expected to fail because Anoma representation of prngs is
different than the juvix representation.
> ⚠️ Based on https://github.com/anoma/juvix/pull/3142
When using AnomaTestModeFull the compilation tests are run in debug
mode, with stdlib interception and run using the raw nock (without
stdlib interception).
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
This PR updates:
- [x] Package version
- [x] Smoke test
The CHANGELOG generator we use:
https://github.com/github-changelog-generator/github-changelog-generator
has stopped working with errors like the following:
```
Warning: PR 3148 merge commit was not found in the release branch or tagged git history and no rebased SHA comment was found
```
So we'll defer populating the CHANGELOG summary until after the release
The hoon code that generates the stdlib call is:
1a8b632463/src/Juvix/Compiler/Nockma/AnomaLib.hs (L101)
i.e the random number generator is the first argument and the width is
the second argument. We have the arguments transposed in the
corresponding Juvix builtin API so the call was failing.
This PR transposes the argumetns in the stdlib call so the builtin API
and hoon generated nock code are compatible.
`unfoldList` should work with for lists like:
* `[5 0]`
* `[5 nil]`
* `[5 tag@myNilTag 0]`
* etc.
currently `unfoldList` will work only for list `nil` terminators that
are tagged with `unfoldList`. `nockmaEq` compares nock terms ignoring
debug annotations, so the above lists will work correctly.
- New command `juvix dev nockma encode --help`
```
Usage: juvix dev nockma encode --to ENCODING --from ENCODING
Encode and decode nockma terms
Available options:
--to ENCODING Choose the source encoding.
• base64: Jam and Base 64 encoding
• bytes: Jam encoding
• debug: Nockma code with annotations
• text: Nockma code without annotations
--from ENCODING Choose the target encoding.
• base64: Jam and Base 64 encoding
• bytes: Jam encoding
• debug: Nockma code with annotations
• text: Nockma code without annotations
```
Use:
```
juvix --log-level=verbose dev nockma run --anoma-dir ~/heliax/anoma Identity.nockma --args args.debug.nockma
```
To print out the JSON request and response payload used in the Anoma
Client RPC call.
* Fixes a bug in calling Anoma stdlib from Nock code
* Runs the anoma compilation test with the anoma node nockma evaluator.
I've classified the tests in 4 categories:
1. `Working`. The test works as expected.
2. `Trace`. We need more work on our end to get the traces from the
anoma node and check that they match the expected result.
3. `NodeError`. The anoma node returns `failed to prove the nock
program`.
4. `Wrong`. The anoma node returns some value that does not match the
expected value.
---------
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
Co-authored-by: Łukasz Czajka <62751+lukaszcz@users.noreply.github.com>
Co-authored-by: Paul Cadman <git@paulcadman.dev>
* Closes#2968
* Implements detection of function-like definitions, which either:
- have some arguments on the left of `:`, or
- have at least one clause.
* Only function-like definitions are recursive.
* Non-recursive definitions are not mutually recursive either, and can
be used only after their definition. This necessitates rearranging some
definitions in existing Juvix code.
* Changes the scoping of identifiers in record updates. Now field names
on the right side don't refer to the old values of the record fields but
to identifiers in scope defined outside the record update. To refer to
old values, one needs to explicitly use record projections, e.g.
```
r@Rec{x := Rec.x r}
```
