* Closes#2571
* It is reasonable to finish this PR before tackling #2562, because the
field element type is the primary data type in Cairo.
* Depends on #2653
Checklist
---------
- [x] Add field type and operations to intermediate representations
(JuvixCore, JuvixTree, JuvixAsm, JuvixReg).
- [x] Add CLI option to choose field size.
- [x] Add frontend field builtins.
- [x] Automatic conversion of integer literals to field elements.
- [x] Juvix standard library support for fields.
- [x] Check if field size matches when loading a stored module.
- [x] Update the Cairo Assembly (CASM) interpreter to use the field type
instead of integer type.
- [x] Add field type to VampIR backend.
- [x] Tests
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
This PR creates a new package that's bundled with the compiler in a
similar way to the stdlib and the package description package.
## The `package-base` Package
This package is called
[package-base](ab4376cf9e/include/package-base)
and contains the minimal set of definitions required to load a Package
file.
The
[`Juvix.Builtin`](ab4376cf9e/include/package-base/Juvix/Builtin/V1.juvix)
module contains:
```
module Juvix.Builtin.V1;
import Juvix.Builtin.V1.Nat open public;
import Juvix.Builtin.V1.Trait.Natural open public;
import Juvix.Builtin.V1.String open public;
import Juvix.Builtin.V1.Bool open public;
import Juvix.Builtin.V1.Maybe open public;
import Juvix.Builtin.V1.List open public;
import Juvix.Builtin.V1.Fixity open public;
```
`Juvix.Builtin.V1.Bool` is required to support backend primitive
integers `Juvix.Builtin.V1.Trait.Natural` is required to support numeric
literals.
## The `PackageDescription.V2` module
This PR also adds a new
[`PackageDescription.V2`](ab4376cf9e/include/package/PackageDescription/V2.juvix)
type that uses the `package-base`. This is to avoid breaking existing
Package files. The Packages files in the repo (except those that test
`PackageDescription.V1`) have also been updated.
## Updating the stdlib
The standard library will be updated to use `Juvix.Builtin.*` modules in
a subsequent PR.
* Part of https://github.com/anoma/juvix/issues/2511
This PR adds a Package.juvix file to the global 'package' package (that
is the package containing the `PackageDescription.{Basic, V1}` modules.
This means that users can now go-to-definition on Package.juvix types
and identifiers and navigate to fully highlighted
`PackageDescription.{Basic, V1}` modules.
* Closes https://github.com/anoma/juvix/issues/2525
This PR adds the `PackageDescription.Basic` module, available to
Package.juvix files.
```
module Package;
import PackageDescription.Basic open;
package : Package := basicPackage;
```
The `PackageDescription.Basic` module provides a Package type that is
translated to a Juvix Package with all default arguments. It is not
possible to customize a basic package.
A basic package does not depend on the standard library, so loads much
more quickly.
Additionally this PR:
* Adds `juvix init --basic/-b` option to generate a basic Package.juvix.
* Migrates Package.juvix files that only use default arguments, or only
customise the name field, to basic Package files.
* Closes https://github.com/anoma/juvix/issues/2508
This PR adds a version number to the module name of the
`PackageDescription` module. This allows us to change the Package file
format in a backwards compatible way in the future.
Now the simplest Package.juvix file looks like:
```
module Package;
import PackageDescription.V1 open;
package : Package := defaultPackage;
```
## Adding new versions
The idea is that new versions of the PackageDescription format will be
added as files of the form:
include/package/PackageDescription/Vx.juvix
The correspondence between a version of the PackageDescription file and
the package type name is recorded in
[`packageDescriptionTypes`](9ba869d836/src/Juvix/Compiler/Pipeline/Package/Loader.hs (L15)).
The `package` identifier type must come from **one** of the versions
of the PackageDescription module.
* Closes https://github.com/anoma/juvix/issues/2452
Depends on:
* ~~https://github.com/anoma/juvix/pull/2459~~
* https://github.com/anoma/juvix/pull/2462
This PR is part of a series implementing:
* https://github.com/anoma/juvix/issues/2336
This PR adds the package file loading function, including a file
evaluation effect. It integrates this with the existing `readPackage`
function and adds tests / smoke tests.
## Package.juvix format
Instead of `juvix.yaml` (which is still supported currently) users can
now place a `Package.juvix` file in the root of their project. The
simplest `Package.juvix` file you can write is:
```
module Package;
import PackageDescription open;
package : Package := defaultPackage;
```
The
[PackageDescription](35b2f618f0/include/package/PackageDescription.juvix)
module defines the `Package` type. Users can use "go-to definition" in
their IDE from the Package file to see the documentation and
definitions.
Users may also import `Stdlib.Prelude` in their Package file. This is
loaded from the global project. No other module imports are supported.
Notes:
* If a directory contains both `Package.juvix` and `juvix.yaml` then
`Package.juvix` is used in preference.
## Default stdlib dependency
The `Dependency` type has a constructor called `defaultStdlib`. This
means that any project can use the compiler builtin standard library
dependency. With `juvix.yaml` this dependency is only available when the
`dependencies` field is unspecified.
```
module Package;
import PackageDescription open;
package : Package := defaultPackage { dependencies := [defaultStdlib] };
```
## Validation
As well as the standard type checking validation that the Juvix compiler
provides additional validation is made on the file.
* The Package module must contain the identifier `package` and it must
have type `Package` that's obtained from the global `PackageDescription`
module.
* Every dependency specified in the Package.juvix must be unique.
* Closes https://github.com/anoma/juvix/issues/2336
## Examples
### Package with name and version
```
module Package;
import PackageDescription open;
package : Package :=
defaultPackage {name := "a-package";
version := mkVersion 0 1 0};
```
### Package with GitHub dependency
```
module Package;
import PackageDescription open;
package : Package :=
defaultPackage {name := "a-package";
version := mkVersion 0 1 0;
dependencies := [defaultStdlib;
github (org := "anoma";
repo := "juvix-containers";
ref := "v0.7.1")]};
```
## Package with main and buildDir fields
```
module Package;
import Stdlib.Prelude open;
import PackageDescription open;
package : Package :=
defaultPackage {name := "a-package";
version := mkVersion 0 1 0;
dependencies := [defaultStdlib;
github (org := "anoma";
repo := "juvix-containers";
ref := "v0.7.1")];
buildDir := just "/tmp/build";
main := just "HelloWorld.juvix"
};
```
The special PathResolver puts files from the global package stdlib and
files from the global package description files in scope of the
$root/Package.juvix module.
Currently this means that PackageDescription module is in scope for the
module so that the user can write:
```
module Package;
import Stdlib.Prelude open;
import PackageDescription open;
package : Package :=
mkPackageDefault
(name := "foo")
{ version := mkVersion 0 1 0
; dependencies :=
[ github "anoma" "juvix-stdlib" "adf58a7180b361a022fb53c22ad9e5274ebf6f66"
; github "anoma" "juvix-containers" "v0.7.1"]};
```
