Support compilation to Anoma compatible functions #2652

paulcadman · 2024-02-14T19:15:43Z

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 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 to make it compatible with the Anoma calling convention.

Testing

The anoma calling convention is unit tested and smoke tested.

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.

lukaszcz · 2024-02-21T09:59:57Z

src/Juvix/Compiler/Core/Data/TransformationId.hs

@@ -69,7 +69,10 @@ toVampIRTransformations = [CombineInfoTables, FilterUnreachable, CheckVampIR, Le

 toStrippedTransformations :: [TransformationId]
 toStrippedTransformations =
-  [CombineInfoTables, FilterUnreachable, CheckExec, LambdaLetRecLifting, TopEtaExpand, OptPhaseExec, MoveApps, RemoveTypeArgs]
+  [CombineInfoTables, FilterUnreachable, LambdaLetRecLifting, TopEtaExpand, OptPhaseExec, MoveApps, RemoveTypeArgs]


The order was significant here -- "illegal" things (for CheckExec - axioms) may get filtered out or brought in from imported modules. Plus, there should be similar checks for Anoma/Nockma and later Cairo. I'll make a commit to this PR to refactor the transformation pipeline to allow for different kinds of checks.

I see - we moved the CheckExec to a toExec transformation (

juvix/src/Juvix/Compiler/Pipeline.hs

Line 178 in 8f7a642

coreToMiniC = Core.toExec >=> coreToAsm >=> asmToMiniC

) to allow Anoma main functions to have arbitrary signatures. But in the case of Anoma we want to check that axioms are not present so I think your refactor is a good idea, thanks.

I commited a refactor.

lukaszcz · 2024-02-21T12:38:32Z

test/Anoma/Compilation/Positive.hs

+      return Test {..}
+
+    withRootCopy :: (Prelude.Path Abs Dir -> IO a) -> IO a
+    withRootCopy action = withSystemTempDir "test" $ \tmpRootDir -> do


The stored standard library is not shared between different tests, which defeats per-module compilation and makes the tests run around 4 times slower than they otherwise would.

Running the tests concurrently in the same directory triggers the leaking IO bypassing the TaggedLock that we've seen before. It's possible that using Effectful will fix this. An alternative would be to synchronously build the standard library somehow before running the test suite and copy that to each temporary location.

Somehow, it works for the Juvix->Native/Wasm compilation tests (in tests/Compilation/positive). What's different?

I remember I've been dealing specifically with this issue when implementing per-module-compilation, and ultimately used file-level locking which solved the problem.

I don't remember what's happening exactly for the main exec pipeline compilation tests, but the stored standard library modules seem to be reused judging by decrease in runtime after first test.

The anoma compilation tests are using the same functions to run the pipeline as the main exec compilation tests, yet they fail for the leaking IO / tagged lock issue. TaggedLock in general is too unreliable and I'm thinking about a plan to remove it. I propose to leave the anoma compilation tests as they are (using separate directories) for now until we work out how we will replace tagged lock.

lukaszcz · 2024-02-21T12:42:00Z

tests/Anoma/Compilation/positive/test007.juvix

+
+terminating
+map'' {A B} {{Partial}} (f : A → B) (x : List A) : List B :=
+  if (null x) nil (f (phead x) :: map'' f (tail x));


Compiling this to Nockma relies on Core-level optimizations. The function phead can internally call a fail function which takes a string as argument. If Partial is not specialised and this internal call to fail is not inlined to directly call the builtin, you'll be translating strings and get a crash.

We'd like to keep support for Strings so we can intercept messages from builtin fail: #2665

We've re-enabled support for PrimString in the Anoma target and refactored the failing tests to use failwith (i.e builtin fail) directly instead of via the Partial trait.

I don't completely understand the rationale behind this replacement -- if you have strings in the Nockma backend you can use Partial, if you don't you can't use failwith either.

I think I misunderstood something. Our rationale is: we don't support Strings in the Nockma backend yet, but we can support builtin fail because it's compiled directly to OpFail in Tree and we can ignore the String argument in the compilation:

juvix/src/Juvix/Compiler/Nockma/Translation/FromTree.hs

Line 361 in 2a22b2f

Tree.OpFail -> return crash

The proposal in #2665 is to intercept the Strings from OpFail and add them to the CellInfo. This String can be used in the Juvix/Nockma evaluator in the error message of the crash but is not serialised when we output Nockma code for consumption by Anoma/Nockma evaluator.

but we can support builtin fail because it's compiled directly to OpFail in Tree

I think that's not an entirely correct assumption, because of eta-expansions in the pipeline or how failwith is translated from Internal to Core. So lambda-abstractions with string argument type might be added on top of the builtin, and the string argument would be applied to a lambda-function - not to the builtin directly. Otherwise my checks for strings in checkBuiltins' wouldn't fail with only failwith because OpFail is already handled specially there. It might work because of subsequent optimisation which inlines the eta-expanded functions.

I see. I'll restore the PrimString check and modify the tests to avoid using Partial/failwith.

We've now modified the tests to avoid using Partial/failwith and restored the Strings check in the anoma backend.

lukaszcz · 2024-02-21T12:46:56Z

I added checks for strings in the Anoma pipeline, which makes the 4 tests indirectly depending on them fail. They compiled before because you had Core-level optimizations turned on, which inlined the functions taking strings, but we shouldn't rely on this.

paulcadman · 2024-02-21T14:06:08Z

I added checks for strings in the Anoma pipeline, which makes the 4 tests indirectly depending on them fail. They compiled before because you had Core-level optimizations turned on, which inlined the functions taking strings, but we shouldn't rely on this.

Should these tests be removed then?

lukaszcz · 2024-02-21T14:13:35Z

I added checks for strings in the Anoma pipeline, which makes the 4 tests indirectly depending on them fail. They compiled before because you had Core-level optimizations turned on, which inlined the functions taking strings, but we shouldn't rely on this.

Should these tests be removed then?

I don't know, maybe they can be fixed, e.g., by removing functions depending on Partial (test 007 definitely can be). I didn't look too much into them, leaving this decision to you.

lukaszcz · 2024-02-23T09:16:24Z

src/Juvix/Compiler/Pipeline.hs

+upToAnoma ::
+  (Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
+  Sem r (Nockma.Term Natural)
+upToAnoma = upToStoredCore >>= \Core.CoreResult {..} -> Nockma.TermCell <$> coreToAnoma _coreResultModule


It should be storedCoreToAnoma (using storedCoreToTree) instead of coreToAnoma. Otherwise, we're doing the Core.toStored transformations twice.

Thank you. Done

lukaszcz

Change src/Juvix/Compiler/Pipeline.hs as discussed in the comment.

This reverts commit 2a22b2f.

paulcadman assigned paulcadman and janmasrovira Feb 14, 2024

paulcadman marked this pull request as draft February 15, 2024 08:58

paulcadman force-pushed the nockma-anoma branch 3 times, most recently from c11d971 to 92a86e4 Compare February 20, 2024 17:10

paulcadman marked this pull request as ready for review February 20, 2024 17:13

paulcadman requested review from lukaszcz and janmasrovira and removed request for lukaszcz February 20, 2024 17:13

paulcadman added this to the 0.6.0 milestone Feb 20, 2024

paulcadman added backend:nockma CLI enhancement New feature or request labels Feb 20, 2024

paulcadman force-pushed the nockma-anoma branch from 92a86e4 to 8f7a642 Compare February 20, 2024 18:55

lukaszcz reviewed Feb 21, 2024

View reviewed changes

janmasrovira force-pushed the nockma-anoma branch from bd5cf23 to 1904c0f Compare February 21, 2024 16:22

paulcadman force-pushed the nockma-anoma branch from 1904c0f to a3d888d Compare February 22, 2024 11:05

paulcadman requested a review from lukaszcz February 22, 2024 12:23

paulcadman force-pushed the nockma-anoma branch 3 times, most recently from 7df03be to ac79511 Compare February 22, 2024 20:52

lukaszcz reviewed Feb 23, 2024

View reviewed changes

lukaszcz requested changes Feb 23, 2024

View reviewed changes

paulcadman and others added 26 commits February 23, 2024 11:20

Add Nockma compiler to program with Anoma calling convention

cf178be

Add anoma compile target

1c94573

Add Resource example

c1cbb8e

Move nockNil' to Nockma.Language

c27226f

Add unit tests for Anoma calling convention

3528fd5

Print help text in Nockma repl

723bedf

Nockma REPL load the initial subject from a file

6bcf512

Add a smoke test for the anoma target

3203115

Remove Resource example for now

4eb6af9

Fix toExec transformations

aac744d

Add end-to-end compilation test for Anoma

6c2c460

Fix compiler warnings

0e41794

Move location of anoma compilation tests

69a14ca

Fix after rebase

0c1f41d

Add more end-to-end tests

d642dd4

Use helper functions to check output

085d03d

Add missing files

00a91a5

Run each anoma compilation test in a separate temp dir

d213045

Add end-to-end compilation tests

35dd24c

refactor toStripped pipeline

8005c36

Allow PrimString type in Anoma so that builtin fail is supported

0cf2395

Fix anoma tests to use failwith instead of partial

f914f2f

Restore check for strings in Anoma backend

5485e6c

Revert "Fix anoma tests to use failwith instead of partial"

3b03546

This reverts commit 2a22b2f.

Anoma compilation tests now avoid using Partial/failwith

fb1f10f

Fix pipeline upToAnoma

f615a0a

paulcadman force-pushed the nockma-anoma branch from c6ed50f to f615a0a Compare February 23, 2024 11:20

paulcadman merged commit be24abb into main Feb 23, 2024
4 checks passed

paulcadman deleted the nockma-anoma branch February 23, 2024 12:54

paulcadman mentioned this pull request Feb 29, 2024

Add an Anoma target to the compiler #2609

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support compilation to Anoma compatible functions #2652

Support compilation to Anoma compatible functions #2652

paulcadman commented Feb 14, 2024 •

edited by lukaszcz

Loading

lukaszcz Feb 21, 2024

paulcadman Feb 21, 2024

lukaszcz Feb 21, 2024

lukaszcz Feb 21, 2024 •

edited

Loading

paulcadman Feb 21, 2024

lukaszcz Feb 21, 2024

lukaszcz Feb 21, 2024

paulcadman Feb 22, 2024

lukaszcz Feb 21, 2024

paulcadman Feb 22, 2024

lukaszcz Feb 22, 2024

paulcadman Feb 22, 2024

lukaszcz Feb 22, 2024 •

edited

Loading

paulcadman Feb 22, 2024 •

edited

Loading

paulcadman Feb 22, 2024

lukaszcz commented Feb 21, 2024

paulcadman commented Feb 21, 2024

lukaszcz commented Feb 21, 2024

lukaszcz Feb 23, 2024

paulcadman Feb 23, 2024

lukaszcz left a comment

Support compilation to Anoma compatible functions #2652

Support compilation to Anoma compatible functions #2652

Conversation

paulcadman commented Feb 14, 2024 • edited by lukaszcz Loading

Anoma calling convention

Testing

Nockma REPL

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lukaszcz Feb 21, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lukaszcz Feb 22, 2024 • edited Loading

Choose a reason for hiding this comment

paulcadman Feb 22, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lukaszcz commented Feb 21, 2024

paulcadman commented Feb 21, 2024

lukaszcz commented Feb 21, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lukaszcz left a comment

Choose a reason for hiding this comment

paulcadman commented Feb 14, 2024 •

edited by lukaszcz

Loading

lukaszcz Feb 21, 2024 •

edited

Loading

lukaszcz Feb 22, 2024 •

edited

Loading

paulcadman Feb 22, 2024 •

edited

Loading