This PR implements:
* JuvixTree parser.
* JuvixTree pretty printer.
* `juvix dev tree read file.jvt` command which reads and pretty prints a
JuvixTree file.
* The `tree` target in the `compile` command.
* Removal of `StackRef` in JuvixAsm. This makes JuvixAsm more consistent
with JuvixTree and simplifies the data structures. `StackRef` is not
needed for compilation from Core.
Tests for the parser will appear in a separate PR, when I implement an
automatic translation of JuvixAsm to JuvixTree files.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
Adds annotations to cells to indicate that it is a call to the stdlib
and might be evaluated faster in the Haskell evaluator.
The syntax for stdlib calls is as follows:
```
[stdlib@add args@<args-term> <left-term> <right-term>]
```
where `add` is the name of the function being called, `<args-term>` is a
nockma term that points to the position of the arguments, and
`<left-term>` and `<right-term>` are the actual components of the cell.
This PR:
* introduces the JuvixTree language which is like JuvixAsm except that
instead of the value stack there is an applicative structure,
* refactors the JuvixCore -> JuvixAsm translation into JuvixCore ->
JuvixTree -> JuvixAsm.
JuvixAsm is a bit too low level for efficient compilation to Nock.
Translating the value stack explicitly is a bad idea and it's
unnecessary, because the value stack just represents an applicative
structure which can be represented directly in Nock. It's possible, but
cumbersome and unnecessary, to recover the applicative structure from
JuvixAsm code. It's better to have a bit more high-level JuvixTree
language which still retains the explicit applicative structure.
This PR is a snapshot of the current work on the JuvixAsm -> Nockma
translation. The compilation of Juvix programs to Nockma now works so we
decided to raise this PR now to avoid it getting too large.
## Juvix -> Nockma compilation
You can compile a frontend Juvix file to Nockma as follows:
example.juvix
```
module example;
import Stdlib.Prelude open;
fib : Nat → Nat → Nat → Nat
| zero x1 _ := x1
| (suc n) x1 x2 := fib n x2 (x1 + x2);
fibonacci (n : Nat) : Nat := fib n 0 1;
sumList (xs : List Nat) : Nat :=
for (acc := 0) (x in xs)
acc + x;
main : Nat := fibonacci 9 + sumList [1; 2; 3; 4];
```
```
$ juvix compile -t nockma example.juvix
```
This will generate a file `example.nockma` which can be run using the
nockma evaluator:
```
$ juvix dev nockma eval example.nockma
```
Alternatively you can compile JuvixAsm to Nockma:
```
$ juvix dev asm compile -t nockma example.jva
```
## Tests
We compile an evaluate the JuvixAsm tests in
cb3659e08e/test/Nockma/Compile/Asm/Positive.hs
We currently skip some because either:
1. They are too slow to run in the current evaluator (due to arithmetic
operations using the unjetted nock code from the anoma nock stdlib).
2. They trace data types like lists and booleans which are represented
differently by the asm interpreter and the nock interpreter
3. They operate on raw negative numbers, nock only supports raw natural
numbers
## Next steps
On top of this PR we will work on improving the evaluator so that we can
enable the slow compilation tests.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
This PR contains refactors split out from the Nockma compile PR
https://github.com/anoma/juvix/pull/2570. Each refactor is associated
with a separate commit in this PR.
* Closes#2561
* Defines an extended subset of Cairo Assembly, following Section 5 of
[1].
* Adds the commands `juvix dev casm read file.casm` and `juvix dev casm
run file.casm` to print and run `*.casm` files.
* The tests cover CASM semantics. Some are "manual translations" of
corresponding JuvixAsm tests according to the JuvixAsm -> CASM
compilation concept.
This PR adds an parser, pretty printer, evaluator, repl and quasi-quoter
for Nock terms.
## Parser / Pretty Printer
The parser and pretty printer handle both standard Nock terms and
'pretty' Nock terms (where op codes and paths can be named). Standard
and pretty Nock forms can be mixed in the same term.
For example instead of `[0 2]` you can write `[@ L]`.
See
a6028b0d92/src/Juvix/Compiler/Nockma/Language.hs (L79)
for the correspondence between pretty Nock and Nock operators.
In pretty Nock, paths are represented as strings of `L` (for head) and
`R` (for tail) instead of the number encoding in standard nock. The
character `S` is used to refer to the whole subject, i.e it is sugar for
`1` in standard Nock.
See
a6028b0d92/src/Juvix/Compiler/Nockma/Language.hs (L177)
for the correspondence between pretty Nock path and standard Nock
position.
## Quasi-quoter
A quasi-quoter is added so Nock terms can be included in the source, e.g
`[nock| [@ LL] |]`.
## REPL
Launch the repl with `juvix dev nockma repl`.
A Nock `[subject formula]` cell is input as `subject / formula` , e.g:
```
nockma> [1 0] / [@ L]
1
```
The subject can be set using `:set-stack`.
```
nockma> :set-stack [1 0]
nockma> [@ L]
1
```
The subject can be viewed using `:get-stack`.
```
nockma> :set-stack [1 0]
nockma> :get-stack
[1 0]
```
You can assign a Nock term to a variable and use it in another
expression:
```
nockma> r := [@ L]
nockma> [1 0] / r
1
```
A list of assignments can be read from a file:
```
$ cat stack.nock
r := [@ L]
$ juvix dev nockma repl
nockma> :load stack.nock
nockma> [1 0] / r
1
```
* Closes https://github.com/anoma/juvix/issues/2557
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
* Closes#2392
Changes checklist
-----------------
* [X] Abstract out data types for stored module representation
(`ModuleInfo` in `Juvix.Compiler.Store.Language`)
* [X] Adapt the parser to operate per-module
* [X] Adapt the scoper to operate per-module
* [X] Adapt the arity checker to operate per-module
* [X] Adapt the type checker to operate per-module
* [x] Adapt Core transformations to operate per-module
* [X] Adapt the pipeline functions in `Juvix.Compiler.Pipeline`
* [X] Add `Juvix.Compiler.Pipeline.Driver` which drives the per-module
compilation process
* [x] Implement module saving / loading in `Pipeline.Driver`
* [x] Detect cyclic module dependencies in `Pipeline.Driver`
* [x] Cache visited modules in memory in `Pipeline.Driver` to avoid
excessive disk operations and repeated hash re-computations
* [x] Recompile a module if one of its dependencies needs recompilation
and contains functions that are always inlined.
* [x] Fix identifier dependencies for mutual block creation in
`Internal.fromConcrete`
- Fixed by making textually later definitions depend on earlier ones.
- Now instances are used for resolution only after the textual point of
their definition.
- Similarly, type synonyms will be unfolded only after the textual point
of their definition.
* [x] Fix CLI
* [x] Fix REPL
* [x] Fix highlighting
* [x] Fix HTML generation
* [x] Adapt test suite
This patch dramatically increases the efficiency of `juvix dev root`,
which was unnecessarily parsing all dependencies included in the
`Package.juvix` file. Other commands that do not require the `Package`
will also be faster.
It also refactors some functions so that the `TaggedLock` effect is run
globally.
I've added `singletons-base` as a dependency so we can have `++` on the
type level. We've tried to define a type family ourselves but inference
was not working properly.
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
## Overview
This PR makes the compiler pipeline thread-safe so that the test suite
can be run in parallel.
This is achieved by:
* Removing use of `{get, set, with}CurrentDir` functions.
* Adding locking around shared file resources like the the
global-project and internal build directory.
NB: **Locking is disabled for the main compiler target**, as it is
single threaded they are not required.
## Run test suite in parallel
To run the test suite in parallel you must add `--ta '+RTS -N -RTS'` to
your stack test arguments. For example:
```
stack test --fast --ta '+RTS -N -RTS'
```
The `-N` instructs the Haskell runtime to choose the number of threads
to use based on how many processors there are on your machine. You can
use `-Nn` to see the number of threads to `n`.
These flags are already [set in the
Makefile](e6dca22cfd/Makefile (L26))
when you or CI uses `stack test`.
## Locking
The Haskell package
[filelock](https://hackage.haskell.org/package/filelock) is used for
locking. File locks are used instead of MVars because Juvix code does
not control when new threads are created, they are created by the test
suite. This means that MVars created by Juvix code will have no effect,
because they are created independently on each test-suite thread.
Additionally the resources we're locking live on the filesystem and so
can be conveniently tagged by path.
### FileLock
The filelock library is wrapped in a FileLock effect:
e6dca22cfd/src/Juvix/Data/Effect/FileLock/Base.hs (L6-L8)
There is an [IO
interpreter](e6dca22cfd/src/Juvix/Data/Effect/FileLock/IO.hs (L8))
that uses filelock and an [no-op
interpreter](e6dca22cfd/src/Juvix/Data/Effect/FileLock/Permissive.hs (L7))
that just runs actions unconditionally.
### TaggedLock
To make the file locks simpler to use a TaggedLock effect is introduced:
e6dca22cfd/src/Juvix/Data/Effect/TaggedLock/Base.hs (L5-L11)
And convenience function:
e6dca22cfd/src/Juvix/Data/Effect/TaggedLock.hs (L28)
This allows an action to be locked, tagged by a directory that may or
may not exist. For example in the following code, an action is performed
on a directory `root` that may delete the directory before repopulating
the files. So the lockfile cannot be stored in the `root` itself.
e6dca22cfd/src/Juvix/Extra/Files.hs (L55-L60)
## Pipeline
As noted above, we only use locking in the test suite. The main app
target pipeline is single threaded and so locking is unnecessary. So the
interpretation of locks is parameterised so that locking can be disabled
e6dca22cfd/src/Juvix/Compiler/Pipeline/Run.hs (L64)
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
- Closes#2362
This pr implements a new typechecking algorithm. This algorithm can be
activated using the global flag `--new-typechecker`. This flag will only
take effect on the compilation pipeline but not the repl.
The main difference between the new and old algorithm is that the new
one inserts holes during typechecking. Thus, it does not require the
arity checker pass.
The new algorithm does not yet implement default arguments. The plan is
to make the change in the following steps:
1. Merge this pr.
2. Merge #2506.
3. Implement default arguments for the new algorithm.
4. Remove the arity checker and the old algorithm.
---------
Co-authored-by: Łukasz Czajka <62751+lukaszcz@users.noreply.github.com>
This PR adds an initial support for Literate Juvix Markdown files, files
with the extension `.juvix.md`.
Here is a small example of such a file: `Test.juvix.md`.
<pre>
# This is a heading
Lorem ...
```juvix
module Test;
type A := a;
fun : A -> A
| _ := a;
```
Other text
</pre>
This initial support enables users to execute common commands such as
typechecking, compilation, and HTML generation. Additionally, a new
command called `markdown` has been introduced. This command replaces
code blocks marked with the juvix attribute with their respective HTML
output, much like the output we obtain when running `juvix html`. In
this version, comments are ignored in the output, including judoc
blocks.
- We intend to use this new feature in combination with this Python
plugin (https://github.com/anoma/juvix-mkdocs) to enhance our
documentation site.
https://github.com/anoma/juvix/assets/1428088/a0c17f36-3d76-42cc-a571-91f885866874
## Future work
Open as issues once this PR is merged, we can work on the following:
- Support imports of Juvix Markdown modules (update the path resolver to
support imports of Literate Markdown files)
- Support (Judoc) comments in md Juvix blocks
- Support Markdown in Judoc blocks
- Update Text editor support, vscode extension and emacs mode (the
highlighting info is a few characters off in the current state)
- Closes#1839
- Closes#1719
This PR:
* Modifies entry point `_entryPointBuildDir` to use the `BuildDir` type
instead of `SomeBase Dir`. This allows delayed resolution of the default
build directory which was useful for the Package -> Concrete translation
point below.
* Modifies `juvix dev root` to render the current package as a
Package.juvix file.
* Modifies the Package -> Concrete translation to recognise default
arguments. So, for example, an empty `juvix.yaml` file will be
translated into the following (instead of the `name`, `version`, and
`dependencies` arguments being populated).
module Package;
import Stdlib.Prelude open;
import PackageDescription.V1 open;
package : Package := defaultPackage;
* Adds a temporary command (removed when juvix.yaml support is removed)
`juvix dev migrate-juvix-yaml` that translates `juvix.yaml` into an
equivalent `Package.juvix` in the current project.
* Adds a temporary script `migrate-juvix-yaml.sh` (removed when
juvix.yaml support is removed) which can be run in the project to
translate all Juvix projects in the repository.
* Actually translate all of the `juvix.yaml` files to `Package.juvix`
using the script.
* Part of https://github.com/anoma/juvix/issues/2487
When moving to Package.juvix, the package configuration file cannot be
empty. So it's convenient to have a quick way to create a Package.juvix
file (previously you could run `touch juvix.yaml`.
This PR adds the `-n / --non-interactive` option to `juvix init`. This
will create a default `Package.juvix`, using the name of the current
directory to populate the package name.
Similarly for the interactive version of juvix init, if the name of the
current directory is not a valid Juvix module then a fallback name is
used instead.
For example:
```
$ mkdir /tmp/new-package
$ cd /tmp/new-package
$ juvix init -n
$ cat Package.juvix
module Package;
import PackageDescription.V1 open;
package : Package :=
defaultPackage
{name := "new-package";
version := mkVersion 0 0 0;
dependencies := [defaultStdlib]};
```
* Part of https://github.com/anoma/juvix/issues/2487
## Global package configuration
This PR updates the global-project to use `Package.juvix` instead of
`juvix.yaml`.
The global package gets the following `Package.juvix`:
```
module Package;
import PackageDescription.V1 open;
package : Package :=
defaultPackage
{name := "global-juvix-package";
version := mkVersion 0 0 0;
dependencies := [defaultStdlib]};
```
## juvix clean --global
This PR also adds an option `-g/--global` to `juvix clean` that removes
the `$XDG_CONFIG_HOME/juvix/VERSION` directory.
## Testing notes
If you've already run Juvix 0.5.3 you'll need to run `juvix clean -g`
before you'll use the new global project. This will not be an issue for
users of Juvix 0.5.4 (as this version of Juvix will never generate
juvix.yaml in the global project).
Part of:
* https://github.com/anoma/juvix/issues/2487
`juvix init` now generates a `Package.juvix` file in the current
directory instead of a `juvix.yaml` file. It uses the prompts from the
user to fill in the name and version options.
### Validity check
After the file is generated, the Juvix project in the current directory
is loaded to check that the generated file is valid.
### Version support
Each version of the PackageDescription module must have a corresponding
[PackageDescriptionType](c39c27000c/src/Juvix/Compiler/Pipeline/Package/Loader/Versions.hs (L12))
which defines:
* The path relative to `include/package` that the file exists at (e.g
`PackageDescription/V1.juvix`)
* The name of the Package type in the file (e.g `Package`)
* A function that translates a Package type into a Concrete function
definition that represents the code that is generated in the
`Package.juvix`
* A function that returns a Bool that determines if the generated
function definition depends on the standard library. (i.e that the
standard library needs to be imported by Package.juvix).
The last point is necessary because in the V1 spec, the `SemVer` type
uses `Maybe` to encode the release and meta components of the of the
version:
```
package : Package :=
defaultPackage
{name := "dd";
version := mkVersion 1 2 3 {just "prerel"} {just "meta"}};
```
So if the user specifies a release or meta component in their version -
then the standard library needs to be imported to provide the `just`
constructor. If the user only specifies major, minor and patch
components then the standard library does not need to be imported.
* Closes https://github.com/anoma/juvix/issues/2485
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"
};
```
Previously the doctor help links would point to the Juvix documentation
dev URLs.
Now the doctor help links point to the version of the documentation
corresponding to the compiler version.
```
$ juvix doctor
> Checking for clang...
> Checking clang version...
> Checking for wasm-ld...
> Checking that clang supports wasm32...
> Checking that clang supports wasm32-wasi...
> Checking that WASI_SYSROOT_PATH is set...
! Environment variable WASI_SYSROOT_PATH is missing
! https://docs.juvix.org/0.5.2/reference/tooling/doctor/#environment-variable-wasi_sysroot_path-is-not-set
> Checking for wasmer...
> Checking latest Juvix release on Github...
```
Spotted by @agureev
The problem with readFile and writeFile from text
[Data.Text.IO](https://hackage.haskell.org/package/text-2.0.2/docs/Data-Text-IO.html)
is that they use the system locale to determine the text encoding
format.
Our assumption is that all Juvix source files are UTF-8 encoded.
I cannot reproduce the issue with using the old APIs on my machine, it
can be reproduced on Arch linux. I'm not sure how to write a specific
test for this.
* Closes https://github.com/anoma/juvix/issues/2472
This PR introduces FileExt type, and consequently, one can generalise
methods and matches based on the file extension; for example,
`parseInputJuvixAsmFile` is now an app. `parseInputFile FileExtJuvixAsm`
This PR adds `--prefix-id`, `--no-path`, and `only-code` flags to the
HTML backend to manipulate the hyperlinks on the resulting HTML output
and the output itself by only keeping the content of the body in the
Html.
As a usage case, we can support `juvix-standalone` blocks, as
demonstrated in
- https://github.com/anoma/juvix-docs/pull/80
* Introduces the `inline: case` pragma which causes an identifier to be
inlined if it is matched on. This is necessary to support GEB without
compromising optimization for other targets.
* Adapts to the new commits in
https://github.com/anoma/juvix-stdlib/pull/86
This PR adds a new command `juvix dependencies update` that fetches all
dependencies in a project and updates the project lock file.
Currently the only way to update the lock file is to delete it and
generate a new one.
## CLI Docs
```
juvix dependencies --help
Usage: juvix dependencies COMMAND
Subcommands related to dependencies
Available options:
-h,--help Show this help text
Available commands:
update Fetch package dependencies and update the lock file
```
## Example
A project containing the following `juvix.yaml`
```yaml
dependencies:
- .juvix-build/stdlib/
- git:
url: https://github.com/anoma/juvix-test
ref: v0.6.0
name: test
main: Example.juvix
name: example
version: 1.0.0
```
compile to generate the lockfile: `juvix compile`
```yaml
# This file was autogenerated by Juvix version 0.5.1.
# Do not edit this file manually.
dependencies:
- path: .juvix-build/stdlib/
dependencies: []
- git:
name: test
ref: a94c61749678ff57556ee6e4cb1f8fbbddbc4ab1
url: https://github.com/anoma/juvix-test
dependencies:
- git:
name: stdlib
ref: 4facf14d9b2d06b81ce1be1882aa9050f768cb45
url: https://github.com/anoma/juvix-stdlib
dependencies: []
```
Now update the test dependency version:
```yaml
- .juvix-build/stdlib/
- git:
url: https://github.com/anoma/juvix-test
ref: v0.6.1
name: test
main: Example.juvix
name: example
version: 1.0.0
```
And run `juvix dependencies update`
Now the lockfile has updated to the hash of v0.6.1:
```yaml
# This file was autogenerated by Juvix version 0.5.1.
# Do not edit this file manually.
dependencies:
- path: .juvix-build/stdlib/
dependencies: []
- git:
name: test
ref: a7ac74cac0db92e0b5e349f279d797c3788cdfdd
url: https://github.com/anoma/juvix-test
dependencies:
- git:
name: stdlib
ref: 4facf14d9b2d06b81ce1be1882aa9050f768cb45
url: https://github.com/anoma/juvix-stdlib
dependencies: []
```
---------
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
This PR adds lock file support to the compiler pipeline. The lock file
is generated whenever a compiler pipeline command (`juvix {compile,
typecheck, repl}`) is run.
The lock file contains all the information necessary to reproduce the
whole dependency source tree. In particular for git dependencies,
branch/tag references are resolved to git hash references.
## Lock file format
The lock file is a YAML `juvix.lock.yaml` file written by the compiler
alongside the package's `juvix.yaml` file.
```
LOCKFILE_SPEC: { dependencies: { DEPENDENCY_SPEC, dependencies: LOCKFILE_SPEC }
DEPENDENCY_SPEC: PATH_SPEC | GIT_SPEC
PATH_SPEC: { path: String }
GIT_SPEC: { git: {url: String, ref: String, name: String } }
```
## Example
Consider a project containing the following `juvix.yaml`:
```yaml
dependencies:
- .juvix-build/stdlib/
- git:
url: https://github.com/anoma/juvix-containers
ref: v0.7.1
name: containers
name: example
version: 1.0.0
```
After running `juvix compile` the following lockfile `juvix.lock.yaml`
is generated.
```yaml
# This file was autogenerated by Juvix version 0.5.1.
# Do not edit this file manually.
dependencies:
- path: .juvix-build/stdlib/
dependencies: []
- git:
name: containers
ref: 3debbc7f5776924eb9652731b3c1982a2ee0ff24
url: https://github.com/anoma/juvix-containers
dependencies:
- git:
name: stdlib
ref: 4facf14d9b2d06b81ce1be1882aa9050f768cb45
url: https://github.com/anoma/juvix-stdlib
dependencies: []
- git:
name: test
ref: a7ac74cac0db92e0b5e349f279d797c3788cdfdd
url: https://github.com/anoma/juvix-test
dependencies:
- git:
name: stdlib
ref: 4facf14d9b2d06b81ce1be1882aa9050f768cb45
url: https://github.com/anoma/juvix-stdlib
dependencies: []
```
For subsequent runs of the juvix compile pipeline, the lock file
dependency information is used.
## Behaviour when package file and lock file are out of sync
If a dependency is specified in `juvix.yaml` that is not present in the
lock file, an error is raised.
Continuing the example above, say we add an additional dependency:
```
dependencies:
- .juvix-build/stdlib/
- git:
url: https://github.com/anoma/juvix-containers
ref: v0.7.1
name: containers
- git:
url: https://github.com/anoma/juvix-test
ref: v0.6.1
name: test
name: example
version: 1.0.0
```
`juvix compile` will throw an error:
```
/Users/paul/tmp/lockfile/dep/juvix.yaml:1:1: error:
The dependency test is declared in the package's juvix.yaml but is not declared in the lockfile: /Users/paul/tmp/lockfile/dep/juvix.lock.json
Try removing /Users/paul/tmp/lockfile/dep/juvix.lock.yaml and then run Juvix again.
```
Closes:
* https://github.com/anoma/juvix/issues/2334
With `-Os` ill-typed code is generated for the following:
```
module wasmcrash.juvix;
import Stdlib.Prelude open;
{-# inline: false #-}
I {A} (x : A) : A := x;
{-# inline: false #-}
I' {A} (x : A) : A := x;
main : Nat := I' (I I 1);
```
Running the generated WASM file with `wasmer` or `wasmtime` gives an
error:
```
Validation error: type mismatch: expected i32 but nothing on stack (at offset 740)
```
The issue occurs with clang version 16.0.5 but not 16.0.0. The issue
does not occur with any other optimization option (`-O1`, `-O2`, `-O3`).
There is no issue with `-Os` used with the native target.
This is thus likely a bug in a specific version of LLVM. It could be
theoretically some very subtle non-conformance to the C standard in our
generated code, but this seems less likely. Creating a minimum C file
exposing the bug would be very time-consuming, so I propose to just
avoid using the `-Os` option for now.
This PR introduces a global `--offline` flag.
## Doctor
This replaces the `--offline` flag on the doctor command.
## Juvix package builds
The flag applies to juvix build commands like `juvix compile`, `juvix
repl`. This is so that users can continue to build packages offline that
have external dependencies when there's no network connection (as long
as they built the same package online previously).
Specifically, when the `--offline` flag is used in a package that has
external git dependencies.
* No `git clone` or `git fetch` commands are used
* `git checkout` will continue to be used
* Clones from previous builds are reused
This means that you can update the `ref` field in a git dependency, as
long as the ref existed the last time that the project was built without
the `--offline` flag.
* Closes https://github.com/anoma/juvix/issues/2333
This PR adds external git dependency support to the Juvix package
format.
## New dependency Git item
You can now add a `git` block to the dependencies list:
```yaml
name: HelloWorld
main: HelloWorld.juvix
dependencies:
- .juvix-build/stdlib
- git:
url: https://my.git.repo
name: myGitRepo
ref: main
version: 0.1.0
```
Git block required fields:
* `url`: The URL of the git repository
* `ref`: The git reference that should be checked out
* `name`: The name for the dependency. This is used to name the
directory of the clone, it is required. Perhaps we could come up with a
way to automatically name the clone directory. Current ideas are to
somehow encode the URL / ref combination or use a UUID. However there's
some value in having the clone directory named in a friendly way.
NB:
* The values of the `name` fields must be unique among the git blocks in
the dependencies list.
## Behaviour
When dependencies for a package are registered, at the beginning of the
compiler pipeline, all remote dependencies are processed:
1. If it doesn't already exist, the remote dependency is cloned to
`.juvix-build/deps/$name`
2. `git fetch` is run in the clone
3. `git checkout` at the specified `ref` is run in the clone
The clone is then processed by the PathResolver in the same way as path
dependencies.
NB:
* Remote dependencies of transitive dependencies are also processed.
* The `git fetch` step is required for the case where the remote is
updated. In this case we want the user to be able to update the `ref`
field.
## Errors
1. Missing fields in the Git dependency block are YAML parse errors
2. Duplicate `name` values in the dependencies list is an error thrown
when the package file is processed
3. The `ref` doesn't exist in the clone or the clone directory is
otherwise corrupt. An error with a suggestion to `juvix clean` is given.
The package file path is used as the location in the error message.
4. Other `git` command errors (command not found, etc.), a more verbose
error is given with the arguments that were passed to the git command.
## Future work
1. Add an offline mode
2. Add a lock file mechanism that resolves branch/tag git refs to commit
hashes
* closes https://github.com/anoma/juvix/issues/2083
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
- Closes#2293.
- Closes#2319
I've added an effect for termination. It keeps track of which functions
failed the termination checker, which is run just after translating to
Internal. During typechecking, non-terminating functions are not
normalized. After typechecking, if there is at least one function which
failed the termination checker, an error is reported.
Additionally, we now properly check for termination of functions defined
in a let expression in the repl.
- Closes#2188.
This pr introduces a new syntactical statement for defining aliases:
```
syntax alias newName := oldName;
```
where `oldName` can be any name in the expression namespace. Fixity and
module aliases are not supported at the moment.
- The `newName` does not inherit the fixity of `oldName`. We have agreed
that the goal is to inherit the fixity of `oldName` except if `newName`
has a fixity statement, but this will be done in a separate pr as it
requires #2310.
Stack LTS 21.6 uses GHC 9.4.5, binaries for HLS are available via ghcup.
Changes required:
1. Fix warnings about type level `:` and `[]` used without backticks.
2. Fix warnings about deprecation of builtin `~` - replaced with `import
Data.Type.Equality ( type (~) )` in the Prelude
3. SemVer is no longer a monoid
4. `path-io` now contains the `AnyPath` instances we were defining
(thanks to Jan) so they can be removed.
5. Added `aeson-better-errors-0.9.1.1` as an extra-dep. The reason it is
not part of the resolver is only because it has a strict bound on base
which is not compatible with ghc 9.4.5. To work around this I've set:
```
allow-newer: true
allow-newer-deps:
- aeson-better-errors
```
which relaxed the upper constraint bounds for `aeson-better-errors`
only. When the base constraints have been updated we can remove this
workaround.
6. Use stack2cabal to generate the cabal.project file and to freeze
dependency versions.
https://www.stackage.org/lts-21.6/cabal.config now contains the
constraint `haskeline installed`, which means that the version of
haskeline that is globally installed with GHC 9.4.5 will be used, see:
* https://github.com/commercialhaskell/stackage/issues/7002
GHC 9.4.5 comes with haskeline 0.8.2 preinstalled but our configuration
contains the source-repository-package for haskeline 0.8.2.1 (required
because we're using a fork) so if you try to run` cabal build` you get a
conflict.
Constraints from cabal imports cannot yet be overridden so it's not
possible to get rid of this conflict using the import method. So we need
to use stack2cabal with an explicit freeze file instead.
7. Remove `runTempFilePure` as this is unused and depends on
`Polysemy.Fresh` in `polysemy-zoo` which is not available in the
resolver. It turns out that it's not possible to use the `Fresh` effect
in a pure context anyway, so it was not possible to use
`runTempFilePure` for its original purpose.
8. We now use https://github.com/benz0li/ghc-musl as the base container
for static linux builds, this means we don't need to maintain our own
Docker container for this purpose.
9. The PR for the nightly builds is ready
https://github.com/anoma/juvix-nightly-builds/pull/2, it should be
merged as soon as this PR is merged.
Thanks to @benz0li for maintaining https://github.com/benz0li/ghc-musl
and (along with @TravisCardwell) for help with building the static
binary.
* Closes https://github.com/anoma/juvix/issues/2166
- Closes#2258
# Overview
When we define a type with a single constructor and one ore more fields,
a local module is generated with the same name as the inductive type.
This module contains a projection for every field. Projections can be
used as any other function.
E.g. If we have
```
type Pair (A B : Type) := mkPair {
fst : A;
snd : B;
};
```
Then we generate
```
module Pair;
fst {A B : Type} : Pair A B -> A
| (mkPair a b) := a;
snd : {A B : Type} : Pair A B -> B
| (mkPair a b) := b;
end;
```
