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.
Avoid excessive backtracking in iterator and named arguments parsing.
This also improves error messages by committing to a parsing branch as
early as possible.
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
This PR fixes an issue with formatting ADT definitions.
Previously the pretty printer would remove required parentheses from
aggregate constructor arguments: `type t (A : Type) := c A (t A) ` ->
`type t (A : Type) := c A t A`.
We now handle this in the same way as patterns.
* https://github.com/anoma/juvix/issues/2277
- Closes#2269
Example:
```
type Sum (A B : Type) :=
| inj1 {
fst : A;
snd : B
}
| inj2 {
fst : A;
snd2 : B
};
sumSwap {A B : Type} : Sum A B -> Sum B A
| inj1@{fst; snd := y} := inj2 y fst
| inj2@{snd2 := y; fst := fst} := inj1 y fst;
```
- Closes#1642.
This pr introduces syntax for convenient record updates.
Example:
```
type Triple (A B C : Type) :=
| mkTriple {
fst : A;
snd : B;
thd : C;
};
main : Triple Nat Nat Nat;
main :=
let
p : Triple Nat Nat Nat := mkTriple 2 2 2;
p' :
Triple Nat Nat Nat :=
p @Triple{
fst := fst + 1;
snd := snd * 3
};
f : Triple Nat Nat Nat -> Triple Nat Nat Nat := (@Triple{fst := fst * 10});
in f p';
```
We write `@InductiveType{..}` to update the contents of a record. The
`@` is used for parsing. The `InductiveType` symbol indicates the type
of the record update. Inside the braces we have a list of `fieldName :=
newValue` items separated by semicolon. The `fieldName` is bound in
`newValue` with the old value of the field. Thus, we can write something
like `p @Triple{fst := fst + 1;}`.
Record updates `X@{..}` are parsed as postfix operators with higher
priority than application, so `f x y @X{q := 1}` is equivalent to `f x
(y @X{q := 1})`.
It is possible the use a record update with no argument by wrapping the
update in parentheses. See `f` in the above example.
- merge #2260 first
Allows constructors to be defined using Haskell-like Adt syntax.
E.g.
```
module Adt;
type Bool :=
| true
| false;
type Pair (A B : Type) :=
| mkPair A B;
type Nat :=
| zero
| suc Nat;
```
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
- 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;
```
- Closes#1641
This pr adds the option to declare constructors with fields. E.g.
```
type Pair (A B : Type) :=
| mkPair {
fst : A;
snd : B
};
```
Which is desugared to
```
type Pair (A B : Type) :=
| mkPair : (fst : A) -> (snd : B) -> Pair A B;
```
making it possible to write ` mkPair (fst := 1; snd := 2)`.
Mutli-constructor types are also allowed to have fields.
- closes#1991
This pr implements named arguments as described in #1991. It does not
yet implement optional arguments, which should be added in a later pr as
they are not required for record syntax.
# Syntax Overview
Named arguments are a convenient mehcanism to provide arguments, where
we give the arguments by name instead of by position. Anything with a
type signature can have named arguments, i.e. functions, types,
constructors and axioms.
For instance, if we have (note that named arguments can also appear on
the rhs of the `:`):
```
fun : {A B : Type} (f : A -> B) : (x : A) -> B := ... ;
```
With the traditional positional application, we would write
```
fun suc zero
```
With named arguments we can write the following:
1. `fun (f := suc) (x := zero)`.
2. We can change the order: `fun (x := zero) (f := suc)`.
3. We can group the arguments: `fun (x := zero; f := suc)`.
4. We can partially apply functions with named arguments: `fun (f :=
suc) zero`.
5. We can provide implicit arguments analogously (with braces): `fun {A
:= Nat; B := Nat} (f := suc; x := zero)`.
6. We can skip implicit arguments: `fun {B := Nat} (f := suc; x :=
zero)`.
What we cannot do:
1. Skip explicit arguments. E.g. `fun (x := zero)`.
2. Mix explicit and implicit arguments in the same group. E.g. `fun (A
:= Nat; f := suc)`
3. Provide explicit and implicit arguments in different order. E.g. `fun
(f := suc; x := zero) {A := Nat}`.
