* Closes#2962
* Depends on #2963
* In Isabelle/HOL comments cannot appear in internal syntax. All
comments inside a Juvix definition are moved outside: to before the
definition or before the earliest function clause.
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
- Closes#2797
Changes:
1. The global flag `--dev-show-thread-ids` is now properly being passed.
Before it was ignored.
3. The progress log has been refactored out of the `ParallelTemplate`
into the `Pipeline.Driver`. With the extra information available, I've
improved how we display the progress log:
1. We show `Compiling`, `Recompiling`, `Loading` to tell if the module
is compiled for the first time (the jvo is missing), or it needs to be
recompiled (with the reason displayed in parentheses), or is loaded from
a jvo file. In the latter case, the message is only showed with
`--log-level verbose|debug`.
2. The modules in other packages are displayed as dependencies with
their own progress counter.
2. When using `-N 1` and compiling a whole project we also get progress
log.
Example screencast:
https://github.com/user-attachments/assets/7cc43cd4-9b23-4ad5-a863-832abacc1b6c
Example file:
```
module error;
import empty; -- error only happens if we have at least one import
type T := t;
x : T := t t; -- type error
```
If one loads this file into emacs (or vscode) they'll get a type error
as expected, but name colors and go-to information is lost, which is
annoying. This pr fixes this.
I'm not sure why, but this bug only occurs when there is at least one
import.
This pr has two relevant changes:
## Errors instead of crases
When registering a builtin, we perform some sanity checks. When
unsuccessful, the compiler crashes. This seldom happens because builtins
are defined in libraries that we write ourselves. However, any compiler
crash is a bug, so this pr refactors these crashes into proper errors.
## Registering builtins during scoping
Before this pr, builtins are registered and sanity checked during the
translation from Concrete to Internal. This imposes that the order in
which we translate stuff is relevant, as we must register a builtin
before we use it. For the most part this is fine when the dependency is
explicit in the code, but sometimes there are explicit dependencies.
E.g. do notation and the builtin `monad-bind`. In order to avoid adding
special rules, it is easier to just register builtins during scoping, so
I've refactored the code to do this.
I've also removed the `Builtins` effect and moved its methods to the
`InfoTableBuilder` since the builtins table is now part of the Scoped
InfoTable. Consequently, I've removed the the field `_artifactBuiltins`.
## Future work
- Fix#2952. I didn't find a good way to fix this problem in this pr, so
it is left for a separate pr.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
This pr adds the `--statements` flag to `juvix dev latex export`. It can
be used like this:
```
juvix dev latex export --statements "List; elem; find" List.juvix
```
All statements are selectable by their 'label'. The label of a statement
is defined as:
1. The function/type/operator/alias/axiom/local_module/fixity/iterator
name being defined.
2. The module name being imported.
## Limitations:
1. Only top statements are allowed. I.e. statements inside local modules
cannot be selected.
1. Open statements are not selectable. Giving `--statements "My.Module"`
will refer to the import statement `import My.Module`.
4. Single constructors are not selectable. Only the whole type
definition.
5. No comments will be printed.
This pr adds two new commands related to latex.
1. `juvix dev latex getJuvixSty`. This command prints the contents of
the `juvix.sty` latex package to stdout. It has no options and the
expected usage is `juvix dev latex getJuvixSty > juvix.sty`.
2. `juvix dev latex export`. Expects a .juvix file as an argument and
outputs to stdout the highlighted module in latex format. Optional flags
`--from LINE`, `--to LINE` to output only the specified line range.
There is a `--mode` flag to choose how you want the output.
```
• standalone: Output a ready to compile LaTeX file
• wrap: Wrap the code in a Verbatim environment
• raw: Output only the code (default: standalone)
```
4. As shown in the standalone output, one is allowed to choose the theme
when importing the juvix package like this: `\usepackage[theme =
latte]{juvix}`. Available themes are `latte`, `frappe`, `macchiato`,
`mocha`.
Examples:
To generate the following output I ran these commands:
```
cd examples/milestones/HelloWorld
mkdir latex
juvix dev latex getJuvixSty > latex/juvix.sty
juvix dev latex export HelloWorld.juvix > latex/main.tex
cd latex
xelatex main.tex
open main.pdf
```
1. with `\usepackage[theme = latte]{juvix}`:
1. with `\usepackage[theme = frappe]{juvix}`:
1. with `\usepackage[theme = macchiato]{juvix}`:
1. with `\usepackage[theme = mocha]{juvix}`:
This pr:
- Removes the light `ayu` theme.
- Adds the light `latte` theme (this now becomes the default theme).
- Adds the dark `frappe` theme.
- Adds the dark `moccha` theme.
- Refactor all source themes to use css variables instead of inlined
color definitions. This makes it much easier to maintain.
1. When the flatparse scanner fails and we fallback to megaparsec, a
warning is issued.
2. The flatparse scanner has been fixed so it is not confused when a
name starts with `import`.
1. Adds the `--log-level LOG_LEVEL` flag to the CLI. This flag can be
given `error`, `warn`, `info`, `progress`, `debug` as argument to filter
the logged messages.
2. Removes the `--only-errors` flag.
3. Adds the `--ide-end-error-char CHAR`, which receives a character as
an argument, which is appended to the end of error messages. This is
handy to facilitate parsing of errors messages from the ide. This
functionality was previously embeded in the old `--only-errors` flag.
* Closes#2813
Implements a translation from Juvix functions to Isabelle/HOL functions.
This extends the previous Juvix -> Isabelle translation which could
handle only type signatures.
Checklist
---------
- [x] Basic translation
- [x] Polymorphism
- [x] Arithmetic operators
- [x] Numeric literals
- [x] List literals
- [x] Comparison operators
- [x] Boolean operators
- [x] `if` translated to Isabelle `if`
- [x] `true` and `false` translated to Isabelle `True` and `False`
- [x] `zero` and `suc` translated to Isabelle `0` and `Suc`
- [x] `Maybe` translated to Isabelle `option`
- [x] Pairs translated to Isabelle tuples
- [x] Quote Isabelle identifier names (e.g. cannot begin with `_`)
- [x] Rename variables to avoid clashes (in Isabelle/HOL pattern
variables don't shadow function identifiers)
- [x] Common stdlib functions (`map`, `filter`, etc) translated to
corresponding Isabelle functions
- [x] Multiple assignments in a single `let`
- [x] CLI
- [x] Test
- The test is very fragile, similar to the markdown test. It just
compares the result of translation to Isabelle against a predefined
expected output file.
Limitations
-----------
The translation is not designed to be completely correct under all
circumstances. There are aspects of the Juvix language that cannot be
straightforwardly translated to Isabelle/HOL, and these are not planned
to ever be properly handled. There are other aspects that are difficult
but not impossible to translate, and these are left for future work.
Occasionally, the generated code may need manual adjustments to
type-check in Isabelle/HOL.
In particular:
* Higher-rank polymorphism or functions on types cannot be translated as
these features are not supported by Isabelle/HOL. Juvix programs using
these features will not be correctly translated (the generated output
may need manual adjustment).
* In cases where Juvix termination checking diverges from Isabelle/HOL
termination checking, providing a termination proof manually may be
necessary. Non-terminating Juvix functions cannot be automatically
translated and need to be manually modelled in Isabelle/HOL in a
different way (e.g. as relations).
* Comments (including judoc) are ignored. This is left for future work.
* Traits are not translated to Isabelle/HOL type classes / locales. This
is left for future work.
* Mutually recursive functions are not correctly translated. This is
left for future work.
* Record creation, update, field access and pattern matching are not
correctly translated. This is left for future work.
* Named patterns are not correctly translated. This is left for future
work.
* Side conditions in patterns are not supported. This is left for future
work.
* If a Juvix function in the translated module has the same name as some
function from the Isabelle/HOL standard library, there will be a name
clash in the generated code.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Currently formatting a project is equivalent to running `juvix format`
on each individual file. Hence, the performance is quadratic wrt the
number of modules in the project. This pr fixes that and we now we only
process each module once.
# Benchmark (1236% faster 🚀)
Checking the standard library
```
hyperfine --warmup 1 'juvix format --check' 'juvix-main format --check'
Benchmark 1: juvix format --check
Time (mean ± σ): 450.6 ms ± 33.7 ms [User: 707.2 ms, System: 178.7 ms]
Range (min … max): 396.0 ms … 497.0 ms 10 runs
Benchmark 2: juvix-main format --check
Time (mean ± σ): 6.019 s ± 0.267 s [User: 9.333 s, System: 1.512 s]
Range (min … max): 5.598 s … 6.524 s 10 runs
Summary
juvix format --check ran
13.36 ± 1.16 times faster than juvix-main format --check
```
# Other changes:
1. The `EntryPoint` field `entryPointModulePath` is now optional.
2. I've introduced a new type `TopModulePathKey` which is analogous to
`TopModulePath` but wihout location information. It is used in hashmap
keys where the location in the key is never used. This is useful as we
can now get a `TopModulePathKey` from a `Path Rel File`.
3. I've refactored the `_formatInput` field in `FormatOptions` so that
it doesn't need to be a special case anymore.
4. I've introduced a new effect `Forcing` that allows to individually
force fields of a record type with a convenient syntax.
5. I've refactored some of the constraints in scoping so that they only
require `Reader Package` instead of `Reader EntryPoint`.
6. I've introduced a new type family so that local modules are no longer
required to have `ModuleId` from their type. Before, they were assigned
one, but it was never used.
# Future work:
1. For project-wise formatting, the compilation is done in parallel, but
the formatting is still done sequentially. That should be improved.
* Closes#2703
* Adds [peephole
optimization](https://en.wikipedia.org/wiki/Peephole_optimization) of
Cairo assembly.
* Adds a transformation framework for the CASM IR.
* Adds `--transforms`, `--run` and `--no-print` options to the `dev casm
read` command.
* Closes#2827
* Adds an optimization phase to the JuvixReg -> Casm pipeline, which
consists of repeated copy & constant propagation and dead code
elimination.
* Types of arguments to `main` can now be field elements, numbers,
booleans and (nested) records and lists.
* Type of `main` result can now be a record of field elements, numbers
and booleans. Lists or nested records are not allowed for the result.
* Adds checks for the type of `main` in the Cairo pipeline.
* Requires updating
[juvix-cairo-vm](https://github.com/anoma/juvix-cairo-vm). The input can
be provided in a Json file via the `--program_input` option of
`juvix-cairo-vm`.
* Adds a RISC0 backend which generates Rust code that can be compiled
with the official RISC0 toolchain.
* The RISC0 backend is a wrapper around the Rust backend.
* Adds the `risc0-rust` to the `compile` CLI command, which creates a
directory containing host and guest Rust sources for the RISC0 zkVM. The
generated code can be compiled/run using `cargo` from inside the created
directory (requires having RISC0 installed:
https://dev.risczero.com/api/zkvm/install).
* Closes#2689
* Adds the command `juvix isabelle program.juvix` which translates a
given file to an Isabelle/HOL theory.
* Currently, only a single module is translated.
* By default translates types and function signatures. Translating
function signatures can be disabled with the `--only-types` option.
Blocked by:
- https://github.com/anoma/juvix/issues/2763
---------
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
This pr introduces parallelism in the pipeline to gain performance. I've
included benchmarks at the end.
- Closes#2750.
# Flags:
There are two new global flags:
1. `-N / --threads`. It is used to set the number of capabilities.
According to [GHC
documentation](https://hackage.haskell.org/package/base-4.20.0.0/docs/GHC-Conc.html#v:setNumCapabilities):
_Set the number of Haskell threads that can run truly simultaneously (on
separate physical processors) at any given time_. When compiling in
parallel, we create this many worker threads. The default value is `-N
auto`, which sets `-N` to half the number of logical cores, capped at 8.
2. `--dev-show-thread-ids`. When given, the thread id is printed in the
compilation progress log. E.g.
# Parallel compilation
1. I've added `src/Parallel/ParallelTemplate.hs` which contains all the
concurrency related code. I think it is good to keep this code separated
from the actual compiler code.
2. I've added a progress log (only for the parallel driver) that outputs
a log of the compilation progress, similar to what stack/cabal do.
# Code changes:
1. I've removed the `setup` stage where we were registering
dependencies. Instead, the dependencies are registered when the
`pathResolver` is run for the first time. This way it is safer.
1. Now the `ImportTree` is needed to run the pipeline. Cycles are
detected during the construction of this tree, so I've removed `Reader
ImportParents` from the pipeline.
3. For the package pathresolver, we do not support parallelism yet (we
could add support for it in the future, but the gains will be small).
4. When `-N1`, the pipeline remains unchanged, so performance should be
the same as in the main branch (except there is a small performance
degradation due to adding the `-threaded` flag).
5. I've introduced `PipelineOptions`, which are options that are used to
pass options to the effects in the pipeline.
6. `PathResolver` constraint has been removed from the `upTo*` functions
in the pipeline due to being redundant.
7. I've added a lot of `NFData` instances. They are needed to force the
full evaluation of `Stored.ModuleInfo` in each of the threads.
2. The `Cache` effect uses
[`SharedState`](https://hackage.haskell.org/package/effectful-core-2.3.0.1/docs/Effectful-State-Static-Shared.html)
as opposed to
[`LocalState`](https://hackage.haskell.org/package/effectful-core-2.3.0.1/docs/Effectful-Writer-Static-Local.html).
Perhaps we should provide different versions.
3. I've added a `Cache` handler that accepts a setup function. The setup
is triggered when a miss is detected. It is used to lazily compile the
modules in parallel.
# Tests
1. I've adapted the smoke test suite to ignore the progress log in the
stderr.
5. I've had to adapt `tests/positive/Internal/Lambda.juvix`. Due to
laziness, a crash happening in this file was not being caught. The
problem is that in this file we have a lambda function with different
number of patterns in their clauses, which we currently do not support
(https://github.com/anoma/juvix/issues/1706).
6. I've had to comment out the definition
```
x : Box ((A : Type) → A → A) := box λ {A a := a};
```
From the test as it was causing a crash
(https://github.com/anoma/juvix/issues/2247).
# Future Work
1. It should be investigated how much performance we lose by fully
evaluating the `Stored.ModuleInfo`, since some information in it will be
discarded. It may be possible to be more fine-grained when forcing
evaluation.
8. The scanning of imports to build the import tree is sequential. Now,
we build the import tree from the entry point module and only the
modules that are imported from it are in the tree. However, we have
discussed that at some point we should make a distinction between
`juvix` _the compiler_ and `juvix` _the build tool_. When using `juvix`
as a build tool it makes sense to typecheck/compile (to stored core) all
modules in the project. When/if we do this, scanning imports in all
modules in parallel becomes trivial.
9. The implementation of the `ParallelTemplate` uses low level
primitives such as
[forkIO](https://hackage.haskell.org/package/base-4.20.0.0/docs/Control-Concurrent.html#v:forkIO).
At some point it should be refactored to use safer functions from the
[`Effectful.Concurrent.Async`](https://hackage.haskell.org/package/effectful-2.3.0.0/docs/Effectful-Concurrent-Async.html)
module.
10. The number of cores and worker threads that we spawn is determined
by the command line. Ideally, we could use to import tree to compute an
upper bound to the ideal number of cores to use.
11. We could add an animation that displays which modules are being
compiled in parallel and which have finished being compiled.
# Benchmarks
On some benchmarks, I include the GHC runtime option
[`-A`](https://downloads.haskell.org/ghc/latest/docs/users_guide/runtime_control.html#rts-flag--A%20%E2%9F%A8size%E2%9F%A9),
which sometimes makes a good impact on performance. Thanks to
@paulcadman for pointing this out. I've figured a good combination of
`-N` and `-A` through trial and error (but this oviously depends on the
cpu and juvix projects).
## Typecheck the standard library
### Clean run (88% faster than main):
```
hyperfine --warmup 1 --prepare 'juvix clean' 'juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432' 'juvix -N 4 typecheck Stdlib/Prelude.juvix' 'juvix-main typecheck Stdlib/Prelude.juvix'
Benchmark 1: juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432
Time (mean ± σ): 444.1 ms ± 6.5 ms [User: 1018.0 ms, System: 77.7 ms]
Range (min … max): 432.6 ms … 455.9 ms 10 runs
Benchmark 2: juvix -N 4 typecheck Stdlib/Prelude.juvix
Time (mean ± σ): 628.3 ms ± 23.9 ms [User: 1227.6 ms, System: 69.5 ms]
Range (min … max): 584.7 ms … 670.6 ms 10 runs
Benchmark 3: juvix-main typecheck Stdlib/Prelude.juvix
Time (mean ± σ): 835.9 ms ± 12.3 ms [User: 788.5 ms, System: 31.9 ms]
Range (min … max): 816.0 ms … 853.6 ms 10 runs
Summary
juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432 ran
1.41 ± 0.06 times faster than juvix -N 4 typecheck Stdlib/Prelude.juvix
1.88 ± 0.04 times faster than juvix-main typecheck Stdlib/Prelude.juvix
```
### Cached run (43% faster than main):
```
hyperfine --warmup 1 'juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432' 'juvix -N 4 typecheck Stdlib/Prelude.juvix' 'juvix-main typecheck Stdlib/Prelude.juvix'
Benchmark 1: juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432
Time (mean ± σ): 241.3 ms ± 7.3 ms [User: 538.6 ms, System: 101.3 ms]
Range (min … max): 231.5 ms … 251.3 ms 11 runs
Benchmark 2: juvix -N 4 typecheck Stdlib/Prelude.juvix
Time (mean ± σ): 235.1 ms ± 12.0 ms [User: 405.3 ms, System: 87.7 ms]
Range (min … max): 216.1 ms … 253.1 ms 12 runs
Benchmark 3: juvix-main typecheck Stdlib/Prelude.juvix
Time (mean ± σ): 336.7 ms ± 13.3 ms [User: 269.5 ms, System: 67.1 ms]
Range (min … max): 316.9 ms … 351.8 ms 10 runs
Summary
juvix -N 4 typecheck Stdlib/Prelude.juvix ran
1.03 ± 0.06 times faster than juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432
1.43 ± 0.09 times faster than juvix-main typecheck Stdlib/Prelude.juvix
```
## Typecheck the test suite of the containers library
At the moment this is the biggest juvix project that we have.
### Clean run (105% faster than main)
```
hyperfine --warmup 1 --prepare 'juvix clean' 'juvix -N 6 typecheck Main.juvix +RTS -A67108864' 'juvix -N 4 typecheck Main.juvix' 'juvix-main typecheck Main.juvix'
Benchmark 1: juvix -N 6 typecheck Main.juvix +RTS -A67108864
Time (mean ± σ): 1.006 s ± 0.011 s [User: 2.171 s, System: 0.162 s]
Range (min … max): 0.991 s … 1.023 s 10 runs
Benchmark 2: juvix -N 4 typecheck Main.juvix
Time (mean ± σ): 1.584 s ± 0.046 s [User: 2.934 s, System: 0.149 s]
Range (min … max): 1.535 s … 1.660 s 10 runs
Benchmark 3: juvix-main typecheck Main.juvix
Time (mean ± σ): 2.066 s ± 0.010 s [User: 1.939 s, System: 0.089 s]
Range (min … max): 2.048 s … 2.077 s 10 runs
Summary
juvix -N 6 typecheck Main.juvix +RTS -A67108864 ran
1.57 ± 0.05 times faster than juvix -N 4 typecheck Main.juvix
2.05 ± 0.03 times faster than juvix-main typecheck Main.juvix
```
### Cached run (54% faster than main)
```
hyperfine --warmup 1 'juvix -N 6 typecheck Main.juvix +RTS -A33554432' 'juvix -N 4 typecheck Main.juvix' 'juvix-main typecheck Main.juvix'
Benchmark 1: juvix -N 6 typecheck Main.juvix +RTS -A33554432
Time (mean ± σ): 551.8 ms ± 13.2 ms [User: 1419.8 ms, System: 199.4 ms]
Range (min … max): 535.2 ms … 570.6 ms 10 runs
Benchmark 2: juvix -N 4 typecheck Main.juvix
Time (mean ± σ): 636.7 ms ± 17.3 ms [User: 1006.3 ms, System: 196.3 ms]
Range (min … max): 601.6 ms … 655.3 ms 10 runs
Benchmark 3: juvix-main typecheck Main.juvix
Time (mean ± σ): 847.2 ms ± 58.9 ms [User: 710.1 ms, System: 126.5 ms]
Range (min … max): 731.1 ms … 890.0 ms 10 runs
Summary
juvix -N 6 typecheck Main.juvix +RTS -A33554432 ran
1.15 ± 0.04 times faster than juvix -N 4 typecheck Main.juvix
1.54 ± 0.11 times faster than juvix-main typecheck Main.juvix
```
* Implements code generation through Rust.
* CLI: adds two `dev` compilation targets:
1. `rust` for generating Rust code
2. `native-rust` for generating a native executable via Rust
* Adds end-to-end tests for compilation from Juvix to native executable
via Rust.
* A target for RISC0 needs to be added in a separate PR building on this
one.
* Closes#2781
* This PR only implements the Rust runtime. The Rust backend / code
generation need to be implemented in a separate PR.
* The tests are unit tests for different modules and tests with
"manually" compiled Juvix programs.
* Adds building & testing of the Rust runtime to the CI.
- Contributes to #2750
# New commands:
1. `dev import-tree scan FILE`. Scans a single file and lists all the
imports in it.
2. `dev import-tree print`. Scans all files in the package and its
dependencies. Builds an import dependency tree and prints it to stdin.
If the `--stats` flag is given, it reports the number of scanned
modules, the number of unique imports, and the length of the longest
import chain.
Example: this is the truncated output of `juvix dev import-tree print
--stats` in the `juvix-stdlib` directory.
```
[...]
Stdlib/Trait/Partial.juvix imports Stdlib/Data/String/Base.juvix
Stdlib/Trait/Partial.juvix imports Stdlib/Debug/Fail.juvix
Stdlib/Trait/Show.juvix imports Stdlib/Data/String/Base.juvix
index.juvix imports Stdlib/Cairo/Poseidon.juvix
index.juvix imports Stdlib/Data/Int/Ord.juvix
index.juvix imports Stdlib/Data/Nat/Ord.juvix
index.juvix imports Stdlib/Data/String/Ord.juvix
index.juvix imports Stdlib/Prelude.juvix
Import Tree Statistics:
=======================
• Total number of modules: 56
• Total number of edges: 193
• Height (longest chain of imports): 15
```
Bot commands support the `--scan-strategy` flag, which determines which
parser we use to scan the imports. The possible values are:
1. `flatparse`. It uses the low-level
[FlatParse](https://hackage.haskell.org/package/flatparse-0.5.1.0/docs/FlatParse-Basic.html)
parsing library. This parser is made specifically to only parse imports
and ignores the rest. So we expect this to have a much better
performance. It does not have error messages.
2. `megaparsec`. It uses the normal juvix parser and we simply collect
the imports from it.
4. `flatparse-megaparsec` (default). It uses the flatparse backend and
fallbacks to megaparsec if it fails.
# Internal changes
## Megaparsec Parser (`Concrete.FromSource`)
In order to be able to run the parser during the scanning phase, I've
adjusted some of the effects used in the parser:
1. I've removed the `NameIdGen` and `Files` constraints, which were
unused.
2. I've removed `Reader EntryPoint`. It was used to get the `ModuleId`.
Now the `ModuleId` is generated during scoping.
3. I've replaced `PathResolver` by the `TopModuleNameChecker` effect.
This new effect, as the name suggests, only checks the name of the
module (same rules as we had in the `PathResolver` before). It is also
possible to ignore the effect, which is needed if we want to use this
parser without an entrypoint.
## `PathResolver` effet refactor
1. The `WithPath` command has been removed.
2. New command `ResolvePath :: ImportScan -> PathResolver m
(PackageInfo, FileExt)`. Useful for resolving imports during scanning
phase.
3. New command `WithResolverRoot :: Path Abs Dir -> m a -> PathResolver
m a`. Useful for switching package context.
4. New command `GetPackageInfos :: PathResolver m (HashMap (Path Abs
Dir) PackageInfo)` , which returns a table with all packages. Useful to
scan all dependencies.
The `Package.PathResolver` has been refactored to be more like to normal
`PathResolver`. We've discussed with @paulcadman the possibility to try
to unify both implementations in the near future.
## Misc
1. `Package.juvix` no longer ends up in
`PackageInfo.packageRelativeFiles`.
1. I've introduced string definitions for `--`, `{-` and `-}`.
2. I've fixed a bug were `.juvix.md` was detected as an invalid
extension.
3. I've added `LazyHashMap` to the prelude. I've also added `ordSet` to
create ordered Sets, `ordMap` for ordered maps, etc.
# Benchmarks
I've profiled `juvix dev import-tree --scan-strategy [megaparsec |
flatparse] --stats` with optimization enabled.
In the images below we see that in the megaparsec case, the scanning
takes 54.8% of the total time, whereas in the flatparse case it only
takes 9.6% of the total time.
- **Megaparsec**
- **Flatparse**
## Hyperfine
```
hyperfine --warmup 1 'juvix dev import-tree print --scan-strategy flatparse --stats' 'juvix dev import-tree print --scan-strategy megaparsec --stats' --min-runs 20
Benchmark 1: juvix dev import-tree print --scan-strategy flatparse --stats
Time (mean ± σ): 82.0 ms ± 4.5 ms [User: 64.8 ms, System: 17.3 ms]
Range (min … max): 77.0 ms … 102.4 ms 37 runs
Benchmark 2: juvix dev import-tree print --scan-strategy megaparsec --stats
Time (mean ± σ): 174.1 ms ± 2.7 ms [User: 157.5 ms, System: 16.8 ms]
Range (min … max): 169.7 ms … 181.5 ms 20 runs
Summary
juvix dev import-tree print --scan-strategy flatparse --stats ran
2.12 ± 0.12 times faster than juvix dev import-tree print --scan-strategy megaparsec --stats
```
In order to compare (almost) only the parsing, I've forced the scanning
of each file to be performed 50 times (so that the cost of other parts
get swallowed). Here are the results:
```
hyperfine --warmup 1 'juvix dev import-tree print --scan-strategy flatparse --stats' 'juvix dev import-tree print --scan-strategy megaparsec --stats' --min-runs 10
Benchmark 1: juvix dev import-tree print --scan-strategy flatparse --stats
Time (mean ± σ): 189.5 ms ± 3.6 ms [User: 161.7 ms, System: 27.6 ms]
Range (min … max): 185.1 ms … 197.1 ms 15 runs
Benchmark 2: juvix dev import-tree print --scan-strategy megaparsec --stats
Time (mean ± σ): 5.113 s ± 0.023 s [User: 5.084 s, System: 0.035 s]
Range (min … max): 5.085 s … 5.148 s 10 runs
Summary
juvix dev import-tree print --scan-strategy flatparse --stats ran
26.99 ± 0.52 times faster than juvix dev import-tree print --scan-strategy megaparsec --stats
```
The judoc examples feature is currently unused. This feature was added
in https://github.com/anoma/juvix/pull/1442
Keeping support for this feature adds a cost to HTML generation. We are
removing this to improve the performance of `juvix html`.
To just render the HTML documentation we only require the scoper result
from the pipeline. To support the examples we need the type checking
result. The cost is significant in larger projects as the pipeline is
run for each import.
Part of https://github.com/anoma/juvix/issues/2744
This PR implements generic support for Cairo VM builtins. The calling
convention in the generated CASM code is changed to allow for passing
around the builtin pointers. Appropriate builtin initialization and
finalization code is added. Support for specific builtins (e.g. Poseidon
hash, range check, Elliptic Curve operation) still needs to be
implemented in separate PRs.
* Closes#2683
- refactor `--target` into subcommands for `dev tree compile`.
- prepend `App` to all `CompileTarget` constructors to avoid name
clashes with `Target`.
- parameterize compile options type with the input kind. The input kind
indicates the expected file extension of the input file. If the input
file is a .juvix file, then it is optional, otherwise it is mandatory.
- Add `AppError MegaparsecError` instance and simplify some related
code.
Implements a disassembler which converts Cairo bytecode into textual
CASM representation. Useful for debugging the Cairo backend.
* Adds the `juvix dev casm from-cairo` command
Each commit in this PR is a separate improvement.
* Tag any Term with a string instead of just cells using `@`. e.g
`"myTag" @ opCall ...`
* `:dump FILE` in the nockma REPL to dump the last REPL result to a
file.
* More tagging in the pretty nockma output.
# Changes
The main goal of this pr is to remove the `--target` flag for `juvix
compile` and use subcommands instead. The targets that are relevant to
normal users are found in `juvix compile --help`. Targets that are
relevant only to developers are found in `juvix dev compile --help`.
Below I list some of the changes in more detail.
## Compile targets for user-facing languages
- `juvix compile native`
- `juvix compile wasi`. I wasn't sure how to call this: `wasm`,
`wasm32-wasi`, etc. In the end I thought `wasi` was short and accurate,
but we can change it.
- `juvix compile vampir`
- `juvix compile anoma`
- `juvix compile cairo`
## *New* compile targets for internal languages
See `juvix dev compile --help`.
1. `dev compile core` has the same behaviour as `dev core
from-concrete`. The `dev core from-concrete` is redundant at the moment.
2. `dev compile tree` compiles to Tree and prints the InfoTable to the
output file wihout any additional checks.
3. `dev compile reg` compiles to Reg and prints the InfoTable to the
output file wihout any additional checks.
4. `dev compile asm` compiles to Asm and prints the InfoTable to the
output file wihout any additional checks.
5. 4. `dev compile casm` compiles to Asm and prints the Result to the
output file wihout any additional checks. TODO: should the Result be
printed or something else? At the moment the Result lacks a pretty
instance.
6.
## Optional input file
1. The input file for commands that expect a .juvix file as input is now
optional. If the argument is ommited, he main file given in the
package.yaml will be used. This applies to the following commands:
1. `juvix compile [native|wasi|geb|vampir|anoma|cairo]`
8. `juvix dev compile [core|reg|tree|casm|asm]`
1. `juvix html`
3. `juvix markdown`.
4. `juvix dev internal [typecheck|pretty]`.
5. `juvix dev [parse|scope]`
7. `juvix compile [native|wasi|geb|vampir|anoma|cairo]`
9. note that `juvix format` has not changed its behaviour.
## Refactor some C-like compiler flags
Both `juvix compile native` and `juvix compile wasi` support `--only-c`
(`-C`), `--only-preprocess` (`-E`), `--only-assemble` (`-S`). I propose
to deviate from the `gcc` style and instead use a flag with a single
argument:
- `--cstage [source|preprocess|assembly|exec(default)]`. I'm open to
suggestions. For now, I've kept the legacy flags but marked them as
deprecated in the help message.
## Remove code duplication
I've tried to reduce code duplication. This is sometimes in tension with
code readability so I've tried to find a good balance. I've tried to
make it so we don't have to jump to many different files to understand
what a single command is doing. I'm sure there is still room for
improvement.
## Other refactors
I've implemented other small refactors that I considered improved the
quality of the code.
## TODO/Future work
We should refactor commands (under `compile dev`) which still use
`module Commands.Extra.Compile` and remove it.
* Closes#2687
* Adds hint support in CASM. The supported hints are `Input(var)` and
`Alloc(size)`. These are the hints currently implemented in
[juvix-cairo-vm](https://github.com/anoma/juvix-cairo-vm).
* Adds the `--program_input` option to the `juvix dev casm run` command.
* Enables private inputs via `main` arguments. In generated CASM/Cairo
code, the arguments to `main` are fetched using the `Input` hint.
* Modifies the CI to use
[juvix-cairo-vm](https://github.com/anoma/juvix-cairo-vm)
* Closes#2563
Checklist
------------
- [x] Serialization of the Haskell CASM representation to the JSON
format accepted by the Cairo VM.
- [x] Add the `cairo` target to the `compile` commands.
- [x] Output via the Cairo `output` builtin.
- [x] Relativize jumps. Cairo VM doesn't actually support absolute
jumps.
- [x] Test the translation from CASM to Cairo by running the output in
the Cairo VM
- [x] Add Cairo VM to the CI
When we first implemented the Nockma backend we wrongly assumed that the
only entry point for Juvix compiled Nockma modules would be the main
function. Using this assumption we could add a setup step in the main
function that put the Anoma stdlib and compiled functions from the Juvix
module in a static place in the Nockma subject. References to the Anoma
stdlib and functions in the module could then be resolved statically.
However, one of the use cases for Juvix -> Nockma compilation is for
Anoma to run logic functions that are fields of a transaction. So the
user writes a Juvix program with main function that returns a
transaction. The result of the main function is passed to Anoma. When
Anoma calls the logic function on a field of the transaction, the setup
part of the main function is not run so the subject is not in the
required state. In fact, the logic function is not even callable by
Anoma because non-main functions in the Juvix module use a calling
convention that assumes the subject has a particular shape.
This PR solves the problem by making all functions in the Juvix module
use the Anoma calling convention. We make all compiled closures
(including, for example, the logic functions stored on resources in a
transaction) self contained, i.e they contain the functions library and
anoma standard library.
Modules that contain many closures produce large nockma output files
which slows down the evaluator. This will need to be fixed in the future
either with Nockma compression ([jam
serialization](https://developers.urbit.org/reference/hoon/stdlib/2p))
or otherwise. But it does not block the compilation and execution of
Anoma transactions.
Other fixes / additions:
* Extra tracing. You can now annotate output cells with a tag that will
be displayed in the output
* Unittests for listToTuple, appendRights helper functions
* Fixes for the nockma parser when parsing 'pretty nockma', specifically
stdlib calls, tags and functions_library atom.
* Adds `juvix dev nock run` command that can run a program output with
the `anoma` target.
* Remove the `nockma` target. As described above we always use the Anoma
calling convention so there's no need for a separate target for the
'juvix calling convention'
* Adds a `--profile` flag to `juvix dev nock run` which outputs a count
of Nockma ops used in the evaluation
* In tests we no longer serialise the compiled program to force full
evaluation of the compiled code. We added a negative test to check that
strings are not allowed in Nockma/Anoma programs,
it is output in a file `OUTPUT.profile` and has the following form:
```
quote : 15077
apply : 0
isCell : 0
suc : 0
= : 4517
if : 5086
seq : 5086
push : 0
call : 4896
replace : 1
hint : 8
scry : 0
trace : 0
```
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
The following benchmark compares juvix 0.6.0 with polysemy and a new
version (implemented in this pr) which replaces polysemy by effectful.
# Typecheck standard library without caching
```
hyperfine --warmup 2 --prepare 'juvix-polysemy clean' 'juvix-polysemy typecheck Stdlib/Prelude.juvix' 'juvix-effectful typecheck Stdlib/Prelude.juvix'
Benchmark 1: juvix-polysemy typecheck Stdlib/Prelude.juvix
Time (mean ± σ): 3.924 s ± 0.143 s [User: 3.787 s, System: 0.084 s]
Range (min … max): 3.649 s … 4.142 s 10 runs
Benchmark 2: juvix-effectful typecheck Stdlib/Prelude.juvix
Time (mean ± σ): 2.558 s ± 0.074 s [User: 2.430 s, System: 0.084 s]
Range (min … max): 2.403 s … 2.646 s 10 runs
Summary
juvix-effectful typecheck Stdlib/Prelude.juvix ran
1.53 ± 0.07 times faster than juvix-polysemy typecheck Stdlib/Prelude.juvix
```
# Typecheck standard library with caching
```
hyperfine --warmup 1 'juvix-effectful typecheck Stdlib/Prelude.juvix' 'juvix-polysemy typecheck Stdlib/Prelude.juvix' --min-runs 20
Benchmark 1: juvix-effectful typecheck Stdlib/Prelude.juvix
Time (mean ± σ): 1.194 s ± 0.068 s [User: 0.979 s, System: 0.211 s]
Range (min … max): 1.113 s … 1.307 s 20 runs
Benchmark 2: juvix-polysemy typecheck Stdlib/Prelude.juvix
Time (mean ± σ): 1.237 s ± 0.083 s [User: 0.997 s, System: 0.231 s]
Range (min … max): 1.061 s … 1.476 s 20 runs
Summary
juvix-effectful typecheck Stdlib/Prelude.juvix ran
1.04 ± 0.09 times faster than juvix-polysemy typecheck Stdlib/Prelude.juvix
```
* Closes#2562
Checklist
---------
- [x] Translation from JuvixReg to CASM
- [x] CASM runtime
- [x] Juvix to CASM pipeline: combine the right transformations and
check prerequisites
- [x] CLI commands: add target `casm` to the `compile` commands
- [x] Tests:
- [x] Test the translation from JuvixReg to CASM
- [x] Test the entire pipeline from Juvix to CASM
This PR adds some flags to tune the (html/md) output.
For Markdown subcommand:
```
--strip-prefix ARG Strip the given prefix from the input file path for
HTML hyperlinks
--folder-structure Generate HTML following the module's folder structure
```
For HTML subcommand, we have the ones above plus the following:
```
--ext ARG File extension in hyperlinks for the input file
(default: ".html")
```
* 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>
Builtin information needs to be propagated from stored modules to REPL
artifacts to avoid "The builtin _ has not been defined" errors.
This PR adds a test suite for the REPL in the Haskell test code. This
means some of the slow smoke tests can be moved to fast haskell unit
tests. In future we should refactor the REPL code by putting in the main
src target and unit testing more features (e.g :doc, :def).
* Closes https://github.com/anoma/juvix/issues/2638
This PR adds a `anoma` target to the `juvix compile`. This target
compiles a Juvix `main` function to a Nockma/Anoma "function". Unlike
the native, wasm, and nockma targets the main function may have any type
signature.
## Anoma calling convention
[Anoma calls
functions](6a4e15fe9c/lib/anoma/resource.ex (L122))
by evaluating the formula `[call L replace [RL args] @ S]` against a
subject equal to the function. Here `args` is a Nockma term that
evaluates to a tuple of arguments that should be passed to the function.
The anoma target compiles the `main` function to Nockma in the same way
as the nockma target. The main function is then
[wrapped](9a658465ae/src/Juvix/Compiler/Nockma/Translation/FromTree.hs (L627))
to make it compatible with the Anoma calling convention.
## Testing
The anoma calling convention is [unit
tested](9a658465ae/test/Nockma/Eval/Positive.hs (L117))
and [smoke
tested](9a658465ae/tests/smoke/Commands/compile.smoke.yaml (L159)).
This PR also adds versions of the end-to-end compilation tests. Most
tests are included, tests for builtin IO operations and string builtins
are omitted. Other tests that use Strings have been adapted to use other
types that are compatible with this backend.
## Nockma REPL
To facilitate testing the Nockma REPL can now load a nockma file as an
initial subject.
---------
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
Now the prelude exports this function:
```
readFile :: (MonadIO m) => Path Abs File -> m Text
readFile = liftIO . Utf8.readFile . toFilePath
```
It is more convenient to use because it uses typed `Path` and works in
any `MonadIO`.
* Implements JuvixReg recursors, which will allow to implement JuvixReg
transformations more succinctly and effectively.
* Adds a transformation framework to JuvixReg.
* Adds identity transformation tests.
* Depends on #2635
- ⚠️ Depends on #2644
The `effectful` library does not support the `Embed` effect out of the
box. However, it offers `IOE`, which is equivalent to `Embed IO` from
polysemy. In preparation to a possible migration to `effectful`, this pr
hides the general `Embed` effect from the prelude and it exports a
specialized `EmbedIO` in its place.
