commit 267b34a3f5a728769fa567421eda1ede5107428c
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed Nov 20 14:18:11 2024 +0100
give proper name of builtins
commit d0dc4155db5fa81945df343faeaf023e7850f094
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed Nov 20 14:09:37 2024 +0100
better error message
commit ccd90448c514ff1a8e9f00b8dd714b660afc0183
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed Nov 20 11:27:05 2024 +0100
allow implicit args
commit 768f45d5d04505307534ed0e54d109e27ea34e48
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue Nov 19 18:44:50 2024 +0100
stdlib
commit e778aaf9a427e8af1cec89f5d164cdec9d0984aa
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue Nov 19 18:29:00 2024 +0100
clean
commit 17939c76ea4f034c2840463f24dfd8c7a5325645
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue Nov 19 18:27:22 2024 +0100
update stdlib
commit 46d73889ae26f8c0d0b34c666ef1b35ad2af859e
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue Nov 19 18:18:22 2024 +0100
pragmas
commit 58d1063b4e4d683f6b6bd314e444d65f30534fd3
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue Nov 19 18:09:23 2024 +0100
do not group deriving statements
commit 057fdbbeef54683d4c16116bb00e097c00496203
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue Nov 19 15:14:31 2024 +0100
default case
commit d280fe741c34eaf60543d6cc4c311470d12ead0b
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue Nov 19 14:55:36 2024 +0100
fix
commit e3a7a764872d2c95ebcfbc1a0c5f3b4848c0b0da
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue Nov 19 09:57:22 2024 +0100
from concrete
commit f8fd9f484737749d26d63e41fa6759a82d50fb23
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon Nov 18 18:45:20 2024 +0100
refactor Fail
commit a889cb65ffa7c62572aa286ac7b669f28d57d5d8
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon Nov 18 18:00:27 2024 +0100
wip
commit 734f7c192d84e1e637175826b520d994e2f38ec6
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon Nov 18 13:00:14 2024 +0100
wip
commit 6a2d7d2c994c315e9af86071c94a0f4be33cbeef
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri Nov 15 13:29:44 2024 +0100
parsing and printing deriving kw
commit 412a6545ba3b00a9226103f2a828d7b96e6fe164
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri Nov 15 12:52:11 2024 +0100
add deriving kw
commit 110146284952ab8d985ca86875c4594eef9375ca
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri Nov 15 12:51:18 2024 +0100
style
commit 3aeec441865484fef18e9956b3579215cddc7c60
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu Nov 14 17:39:09 2024 +0100
remove section titles from parser
commit 15ec17dd6d8c1f4f421df51d520a1e26f48cc05c
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu Nov 14 15:29:57 2024 +0100
update stdlib
commit 546b5b2f7a6f2a2d4579406f7f672a5a02a19a42
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu Nov 14 11:27:04 2024 +0100
make Eq builtin
commit 865842046d
Author: Paul Cadman <git@paulcadman.dev>
Date: Wed Nov 20 07:53:21 2024 +0000
Support running nockma code with a running Anoma client (#3180)
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
```
commit 455249db4d
Author: Łukasz Czajka <62751+lukaszcz@users.noreply.github.com>
Date: Tue Nov 19 20:34:52 2024 +0100
HTML generation: make the light theme lighter (#3168)
* 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.
commit eab02a77da
Author: Paul Cadman <git@paulcadman.dev>
Date: Tue Nov 19 17:34:13 2024 +0000
Remove `GetAnomaProcess` from the Anoma effect (#3179)
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.
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}
```
