1
1
mirror of https://github.com/anoma/juvix.git synced 2025-01-06 06:53:33 +03:00
Commit Graph

1566 Commits

Author SHA1 Message Date
Paul Cadman
0714391900
Release 0.6.7 (#3153)
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
2024-11-07 09:50:18 +00:00
Paul Cadman
2a463a00a2
Fix StdlibRandomNextBytes call (#3150)
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.
2024-11-07 09:05:13 +01:00
Paul Cadman
4a1350a783
Use nockmaEq instead of Eq instance to detect nil terminator (#3149)
`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.
2024-11-06 19:28:38 +01:00
Paul Cadman
1a8b632463
Update juvix-stdlib ref to latest main (#3148)
This PR updates the juvix-stdlib submodule ref to the latest main
branch.

It incorporates changes from:

* https://github.com/anoma/juvix-stdlib/pull/134
2024-11-06 15:52:58 +00:00
Jan Mas Rovira
bf09ee2888
Add dev nockma encode command (#3135)
- 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
```
2024-11-06 10:01:33 +01:00
Jan Mas Rovira
0961d874d3
juvix dev nockma run --anoma-dir ./anoma --args are given as a nockma list (#3142)
When we run nockma code in the anoma node, the arguments should be given
as a nockma list. I.e. a nil terminated tuple.
2024-11-05 17:11:24 +01:00
Paul Cadman
663cd85bcc
Anoma client verbose request response (#3140)
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.
2024-11-05 14:50:19 +00:00
Jan Mas Rovira
4cdcb2f747
Add anoma nockma tests (#3134)
* 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>
2024-11-05 13:28:28 +00:00
Łukasz Czajka
3030196fdd Non-recursive definitions (#3138)
* 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}
```
2024-11-04 18:18:39 +01:00
Jan Mas Rovira
71161ffecd
Fix package-base interaction (#3139)
- Fixes #3009 
- Fixes #2877
- TODO think if this makes https://github.com/anoma/juvix/issues/2985
slightly easier to fix
2024-11-01 14:42:18 +00:00
Łukasz Czajka
a43f73ab2c
Stdlib: add functions to the Map module (#3136)
Co-authored-by: Paul Cadman <git@paulcadman.dev>
2024-11-01 11:04:22 +00:00
Łukasz Czajka
95275ca5c1
Detect constant side conditions in matches (#3133)
* Closes #3007 
* Depends on #3101 
* Detects side conditions which are `true` (removes the condition) or
`false` (removes the branch).
2024-11-01 09:50:19 +00:00
Łukasz Czajka
68a79bc8a8
Detect redundant patterns (#3101)
* Closes #3008
* Implements the algorithm from [Luc Maranget, Warnings for Pattern
Matching](https://www.cambridge.org/core/services/aop-cambridge-core/content/view/3165B75113781E2431E3856972940347/S0956796807006223a.pdf/warnings-for-pattern-matching.pdf)
to detect redundant patterns.
* Adds an option to the Core pretty printer to print match patterns in a
user-friendly format consistent with pattern syntax in Juvix frontend
language.
2024-10-30 11:38:22 +01:00
Paul Cadman
23837ed745
Fix linux static build by pinning ghc-musl container version (#3132)
The linux nightly build stopped working on 2024-10-22 after the
ghc-musl:9.8.2 image was rebuilt.

With the following error:

```
Preprocessing executable 'juvix' for juvix-0.6.6..
Building executable 'juvix' for juvix-0.6.6..
[  1 of 199] Compiling Commands.Extra.Package
[  2 of 199] Compiling CommonOptions

<no location info>: error:
    Error loading shared library -lncursesw: No such file or directory
```

I've fixed this by pinning the container image using the container hash
from before the failure. We must use the `docker.io` repository because
`quay.io` does not seem to store old manifest files.

The linux nightly build is now working after this change:


https://github.com/anoma/juvix-nightly-builds/actions/runs/11579013347/job/32234216197
2024-10-29 19:58:00 +00:00
Paul Cadman
3b34f6e4ff
Support random API from the Anoma stdlib (#3129)
This PR adds frontend support for the Anoma Random API:

The frontend builtin APIs are:

```
builtin anoma-random-generator
axiom RandomGenerator : Type;

builtin anoma-random-generator-init
axiom randomGeneratorInit : Nat -> RandomGenerator;

builtin anoma-random-generator-split
axiom randomGeneratorSplit : RandomGenerator
  -> Pair RandomGenerator RandomGenerator;

builtin anoma-random-next-bytes
axiom randomNextBytes : Nat
  -> RandomGenerator
  -> Pair ByteArray RandomGenerator;
```

### Nockma Evaluator

The Nockma evaluator intercepts the corresponding Anoma random stdlib
calls using the
[System.Random](https://hackage.haskell.org/package/random-1.2.1.2/docs/System-Random.html)
API. The implementation uses the
[splitmix](https://hackage.haskell.org/package/splitmix-0.1.0.5/docs/System-Random-SplitMix.html)
generator directly because it has an API to destructure the generator
into a pair of integers. We can use this to serialise the generator.



* Closes https://github.com/anoma/juvix/issues/2902
2024-10-29 18:23:37 +00:00
Łukasz Czajka
c143259aee
Allow trailing semicolons everywhere (#3123)
* Closes #3039
* Closes #3043
* Closes #2970
* Closes #3089
* Parser allows trailing semicolons for any kind of semicolon-separated
items:
  - let-block statements,
  - module statements,
  - record declaration statements,
  - record update fields,
  - record pattern fields,
  - named application arguments,
  - list literal items,
  - list pattern items,
  - open statement using/hiding items,
  - `syntax iterator` declaration parameters,
  - `syntax fixity` declaration parameters.
* Formatter prints trailing semicolons if the items are displayed on
separate lines, removes them if on a single line.
* The formatting of multiline lists is changed to make it consistent
with other semicolon-separated blocks:
```
[
  1;
  2;
  3;
]
```
instead of
```
[ 1
; 2
; 3
]
```
2024-10-29 18:25:06 +01:00
Jan Mas Rovira
021f183d33
Run Nockma in an Anoma node (#3128)
# Changes
1. Adds a new command `juvix dev anoma node`. This command runs the
anoma node.
2. Adds a flag `--anoma-dir` to `juvix dev nockma run`. When given, it
must point to the anoma clone. Then, it will run the nockma code in the
anoma node and report the result (with no traces).

# Prerequisites
1. An anoma clone at some specific commit. 
   ```
   git clone git@github.com:anoma/anoma.git
   cd anoma
   git checkout 98e3660b91cd55f1d9424dcff9420425ae98f5f8
   
   # build anoma
   mix deps.get
   mix escript.install hex protobuf
   mix compile

   # build the client
   mix do --app anoma_client escript.build
   ```
2. The `mix` command (elixir).
3. The [`grpcurl`](https://github.com/fullstorydev/grpcurl) command. To
install a single binary in `~/.local/bin` you can run:
   ```
curl -sSL
"https://github.com/fullstorydev/grpcurl/releases/download/v1.9.1/grpcurl_1.9.1_linux_x86_64.tar.gz"
| tar -xz -C ~/.local/bin --no-wildcards grpcurl
   ```

# Testing
I've not included any test. It can be tested locally like this:
```
cd juvix/tests/Anoma/Compilation/positive
juvix compile anoma test001.juvix
echo 20 > args.debug.nockma
juvix dev nockma run --anoma-dir ~/projects/anoma test001.nockma --args args.debug.nockma
2024-10-29 17:32:59 +01:00
Łukasz Czajka
e1058c87fc
Improve function argument names in the standard library (#3127) 2024-10-28 13:29:50 +01:00
Jan Mas Rovira
47696514dc
Set line width to 80 (#3124) 2024-10-25 15:11:19 +02:00
Łukasz Czajka
3cf79faafb
Formatter: add braces when the iterator body is not enclosed (#3122)
* Closes #3091
* Formatter adds braces when the body is not enclosed in braces or
parentheses. Braces-enclosed body is always printed as a block on a new
line:
```
for (acc := 0) (x in lst) {
  x + acc
}
```
* If the body is enclosed in ordinary parentheses, then they are
preserved and the iterator is printed on a single line, if possible:
```
for (acc := 0) (x in lst) (x + acc)
```
This is sometimes useful when you want iterator application as an
argument to something.
2024-10-25 11:42:01 +02:00
Łukasz Czajka
ddca867871
Remove VampIR from the CI (#3126) 2024-10-24 20:18:50 +02:00
Paul Cadman
6639e64b64
Update Anoma nock library (#3119)
This PR updates the Anoma nock library for Anoma node release 0.25.0.

The nock locations for anoma lib functions do not change because the
only changes to the Anoma lib are within the `og` layer (which we do not
currently use).

The nock term in anomalib.nockma was obtained from:


4897751366/hoon/anoma.hoon

4897751366/hoon/resource-machine.hoon
2024-10-24 14:30:43 +01:00
Łukasz Czajka
8f180ccfda
Improve Set and Map modules in the standard library (#3120)
* Updates the standard library to
https://github.com/anoma/juvix-stdlib/pull/130
* Also changes `null` to `isEmpty`, which required updating some tests

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
2024-10-24 12:29:33 +01:00
Jan Mas Rovira
e951df077d
Don't put a space after the lambda keyword (#3121)
- Closes #3095
2024-10-23 16:02:56 +02:00
Paul Cadman
ae89c4d480
Serialize Nockma output using nock jam (#3066)
The Anoma API accepts jammed nock terms as input. The benefit to this is
that jammed terms are greatly compressed compared to the original term.

* Closes https://github.com/anoma/juvix/issues/3017

Remaining tasks:

- [x] Deserialize input nockma file in `juvix dev nockma {run, eval}`
- [x] Support debug input nockma file in `juvix dev nockma {run, eval,
repl}` i.e there should be a way to pass the `*.debug.nockma` (output of
`juvix compile anoma --debug`) file to `juvix dev nockma {run, eval,
repl}`
- [x] Add proper JuvixErrors for deserialisation failures

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2024-10-23 09:02:32 +01:00
Jan Mas Rovira
d741fbc971
Refactor dangerous default branches in Core to Tree translation (#3116)
- Closes #3115 

Now we will get a proper warning when adding more builtins to Core.
2024-10-22 13:38:24 +01:00
Paul Cadman
18cca89296
Add frontend support for Anoma Resource Machine builtins (#3113)
This PR adds frontend builtin support for the Anoma Resource machine
functions provided in
[resource-machine.hoon](4897751366/hoon/resource-machine.hoon),
*except* for the `prove-logic` function which still needs some
discussion.

Users must now mark the Anoma `Resource` type with
`builtin-anoma-resource` and the Anoma `Action` type with
`builtin-anoma-action`. This is required because the resource machine
functions use these types.

The compiler does not check that the constructors of `Resource` and
`Action` match the RM spec. I made this decision because the Anoma types
are sill in flux and it's easier to change if correctness is delegated
to the RM library for now. We can add the constructor checks when the
Anoma RM interface is stable.

The test file
[test085.juvix](47ba3e2746/tests/Anoma/Compilation/positive/test085.juvix)
demonstrates how each builtin should be used.

### Core Evaluator

The Core evaluator does not support these builtin functions in normal
mode. When used for normalisation (e.g when used in the constant folding
pass) the Core evaluator leaves the builtin functions unchanged.

### Nock Evaluator

The Nock evaluator does not intercept the Anoma lib functions that the
builtins correspond to in the Nock backend. It executes the underlying
Nock code instead. This means that several of the functions cannot be
tested because they're either too slow (e.g commitment) or do not have
an implementation in the Nock code (e.g addDelta).

* Closes: https://github.com/anoma/juvix/issues/3084
2024-10-22 13:10:08 +02:00
Paul Cadman
8fb5ae77ba
Rename Nockma stdlib to anomalib and add RM references (#3111)
Most changes in this PR relate to renaming of the Anoma Nock
StandardLibrary to AnomaLibrary. This is because the Anoma library now
consists of a standard library from
[anoma.hoon](a20b5e7838/hoon/anoma.hoon)
and the resource machine library
[resource-machine.hoon](a20b5e7838/hoon/anoma.hoon).

The Anoma RM functions and value references are also added. Their
integration into the compiler pipeline will happen in a separate PR.

The Anoma Library RM functions and stdlib functions are enumerated
separately. There is a separate type for Anoma Library values because
these are compiled differently than functions.

Part of:

* https://github.com/anoma/juvix/issues/3084
2024-10-21 13:28:37 +02:00
Łukasz Czajka
5d32e8f0b5
Fix closure representation in the Nock backend (#3105)
* Closes #3083 
* Closes #3042 

The representation of closures is changed to make it more efficient and
compatible with the Nock calling convention.
2024-10-18 18:49:34 +01:00
Paul Cadman
c238429753
Update anoma nock stdlib to include resource machine client library (#3110)
> ⚠️ There's a big diff because `stdlib.nockma` is now exported from
Anoma with no line-breaks.

The nock stdlib code was obtained from anoma release v0.24.1. The nock
stdlib now contains the resource machine client library.


a20b5e7838

using the Elixir interactive prompt in the root of a clone of Anoma.

```
iex -S mix
iex(1)> File.write("./stdlib.nockma", Nock.rm_core |> Noun.Format.print)
```

I've added these instructions for updating the `stdlib.nockma` file in a
`README.md`.

The nock cells in StdlibFunction.hs were obtained in the urbit dojo
using:


a20b5e7838/hoon/anoma.hoon

a20b5e7838/hoon/resource-machine.hoon
2024-10-18 16:25:27 +01:00
Paul Cadman
0a9ec8fb37
Add frontend support for Anoma stdlib sha256 (#3109)
This PR adds frontend support for Anoma stdlib sha256 function (aka
`shax` in Nock).

* Closes https://github.com/anoma/juvix/issues/2901

The new builtin can be declared as follows:

```
builtin anoma-sha256
axiom anomaSha256 : Nat -> ByteArray;
```

The intention is that it wraps a call to anomaEncode as follows:

```
sha256 {A} (a : A) : ByteArray := anomaSha256 (anomaEncode a);
```

### Fix for atom to ByteString

This PR also includes a commit
6205dc9ff9
to fix an issue with functions like `integerToByteArray` when called
with negative integers (the solution is to change the argument types to
Natural, as this is all we need for Anoma).
2024-10-17 19:11:26 +02:00
Emmanuel Ferdman
093a34b848
Update license reference (#3108)
# Description

Commit 22ba8f15fd renamed the license
file. This PR adjusts source to changes.

Fixes # (issue)

## Type of change

Please delete options that are not relevant.

- [x] Bug fix (non-breaking change which fixes an issue)
- [ ] New feature (non-breaking change which adds functionality)
- [ ] Breaking change (fix or feature that would cause existing
functionality to not work as expected)
- [ ] This change requires a documentation update

# Checklist:

- [x] My code follows the style guidelines of this project
- [x] I have made corresponding changes to the documentation
- [x] My changes generate no new warnings
- [ ] I have added tests that prove my fix is effective or that my
feature works:
  - [ ] Negative tests
  - [ ] Positive tests
  - [ ] Shell tests

Signed-off-by: Emmanuel Ferdman <emmanuelferdman@gmail.com>
2024-10-17 14:00:17 +01:00
Paul Cadman
6a9f1c3d93
Update AnomaCallablePathId to match Anoma calling convention (#3107)
The `StandardLibrary` constructor of `AnomaCallablePathId` must be last.
This is because Anoma will replace the tail of the main function with
the resource machine standard library when it calls it.

See:
* https://github.com/anoma/juvix/issues/3106

for more details.
2024-10-17 10:26:53 +01:00
Łukasz Czajka
f1bb0e50d9
Remove VampIR compile command and tests (#3104)
* Closes #2841 
* Moves the `vampir` compilation target under `dev`.
* Removes VampIR tests that require the external `vamp-ir` executable.
2024-10-16 15:03:14 +02:00
Łukasz Czajka
c50ad06976
Compile-time configuration (#3102)
* Closes #3077 
* Closes #3100 
* Adds a compilation-time configuration script that creates a
`config/config.json` file which is then read by the
`Makefile`/`justfile` and embedded into the Juvix binary.
2024-10-16 11:47:23 +02:00
Paul Cadman
9fcc49f6e0
Update anoma nock stdlib (#3103)
The nock stdlib code was obtained from anoma release v0.24.1


a20b5e7838/apps/anoma_lib/lib/nock.ex (L556)

The nock cells in StdlibFunction.hs were obtained in the urbit dojo
using:


a20b5e7838/hoon/anoma.hoon
2024-10-15 20:45:27 +02:00
Łukasz Czajka
feb422d445
Allow @ in constructor declarations (#3099)
* Closes #3041 
* The old syntax without `@` is still accepted, but the formatter
changes it to the new syntax
2024-10-15 19:15:37 +02:00
Łukasz Czajka
83539148cb
Update standard library coding style according to the guidelines (#3092)
* Closes #3079
* Closes #3086
* Depends on #3088 
* Updates the coding style guidelines (CODING.md) to reflect issues not
foreseen originally
* Changes the unicode arrow printed in the REPL to `->`. This is to make
the output consistent with how function types are written in the
standard library.

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
2024-10-14 15:56:54 +02:00
Paul Cadman
c499d0d7e1
Support Anoma stdlib curry function (#3097)
This PR adds support for the Anoma node stdlib function to the nockma
backend.

https://developers.urbit.org/reference/hoon/stdlib/2n#cury

This PR also changes the arguments placeholder value when compiling
functions and closures to make it a tuple of length equal to the
function/closure arity.

To use curry, the function argument's placeholder argument tuple must
have length equal to the function airty.

For example if we are compiling a function with arity 2, the compiled
nock function should have the form:

```
[compiled-code [0 0] env]
```
2024-10-11 16:53:06 +02:00
Łukasz Czajka
ec169a45cd
Merge containers into standard library (#3088)
* Closes #3067 
* Depends on #3087
2024-10-10 17:23:39 +01:00
Łukasz Czajka
7760267bcd
Fix JuvixTree unification (#3087)
* Closes #3016 
* Fixes the `curryType` function
* Changes the behaviour of `unifyTypes` and `isSubtype` to always curry
first
2024-10-09 15:33:42 +02:00
Łukasz Czajka
a3bfaca7bb
Avoid duplication in Nockma code generation (#3070)
* Closes #3013 
* Removes all remaining problems with evaluation duplication that could
potentially lead to an exponential blow-up in the running time.
* Adds the capacity to generate saves of temporary values in the Nock
code generation backend.
* Removes the `TempHeight` transformation on JuvixTree. It is no longer
needed.
* Removes the `ComputeCaseANF` transformation on JuvixCore from the
Anoma pipeline. It is no longer necessary.
2024-10-08 10:05:20 +02:00
Łukasz Czajka
4014030305
Add coding style guidelines (#3059)
Juvix coding style guidelines for the standard library and Anoma apps.
Compiled from discussions with @janmasrovira @paulcadman @heueristik

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2024-10-07 16:49:02 +02:00
Łukasz Czajka
40b71b95de
Nockma backend: translate trace to %puts hints (#3053)
* Closes #3022 
* Requires https://github.com/anoma/anoma/pull/861
2024-10-07 14:01:01 +02:00
Jan Mas Rovira
358551995e
Fix named application bug (#3075)
- Fixes #3074

- Merge after #3076

---------

Co-authored-by: Łukasz Czajka <62751+lukaszcz@users.noreply.github.com>
2024-10-03 16:26:59 +01:00
Jan Mas Rovira
8c37d9b439
Merge typechecker negative tests (#3076) 2024-10-03 10:02:45 +02:00
Jan Mas Rovira
137b6d83eb
Fix termination crash due to empty permutation (#3081)
- Fixes #3064
2024-10-02 18:59:30 +02:00
Jan Mas Rovira
a1926547a2
Reimplement positivity checker (#3057)
- Fixes #3048
- Fixes #3058

Due to #3071 I had to change the order of two lines in
tests/Compilation/positive/test079.juvix.
2024-10-01 13:39:28 +02:00
Jan Mas Rovira
eaec932df1
Remove unused field from ScoperState (#3073) 2024-09-30 19:28:44 +02:00
Jan Mas Rovira
deca981fa3
Ignore files that start with a . (#3072)
- Closes #3068
2024-09-30 12:17:18 +02:00