Thanks!

[yurrriq]

I'm very interested in this. Somewhere, I have a totally bitrotten attempt at a Core Erlang backend for Idris 1.x, but this seems much more promising. Realistically, I probably only have a few hours a week, but is there anything I might help with?

Thanks for this project!

[chrrasmussen]

Thanks for showing interest in this project! Cool that you have worked on a similar project :-)

Have you tried to run the Erlang code generator on some Idris 2 code? If not, I just pushed some updates to the documentation that might help to get started. Note that installation method 1 and 2 in the README.md is not quite ready, which means that one needs to have idris2 installed already.

Later this week I will start to migrate my notes onto to the issue tracker. Hopefully that will make it easier to see if there is anything interesting that you want to tackle.

Contributing to Idris 2 itself is also very helpful to this project.

If you have any questions, feel free to ask!

[yurrriq]

I just came across it, so haven't even cloned yet. I'll audit the docs and PR with updates if I have any trouble. I use NixOS which might make things more interesting, too.

Re: notes -> issues. Sounds good, thanks!

Why target Erlang instead of Core Erlang, given the stated non-goal of making the generated code readable. I'm not sure how outdated it is, but the simplicity and brevity of the Core Erlang 1.0.3 language specification from 2004 seems appealing to me.

[chrrasmussen]

When I started working on the Erlang code generator I was only somewhat familiar with Erlang. Before that I had built a project using Elixir and Phoenix (which was a nice experience). It seemed easier to get something working by generating Erlang source code. I have since then added two intermediate representations: ErlExpr and AbstractFormat. AbstractFormat tries to be a faithful representation of the Erlang Abstract Format. ErlExpr is similiar to NamedCExp but it include some Erlang-specific functionality. The AbstractFormat could be used to build Erlang modules entirely from memory (using compile:forms/2), but this is not implemented yet.

The Erlang codegen is able to generate both Erlang source code (idris2erl --output-dir . -o main_erl --directive "format erl" Main.idr) and the Erlang Abstract Format serialized to files (idris2erl --output-dir . -o main_abstr --directive "format abstr" Main.idr). Both formats are generated from AbstractFormat.

As a reference, the Idris 2 compiler (including the Erlang codegen) has the following intermediate representations:

  +-----------+                   
  |   PTerm   | (High-level Idris)
  +-----------+                   
        |                         
        |                         
  +-----------+                   
  |   TTImp   |                   
  +-----------+                   
        |                         
        |                         
  +-----------+                   
  |   Term    | (TT)
  +-----------+                   
        |                         
        |                         
  +-----------+                   
  |   CExp    |------------+      
  +-----------+            |      
        |                  |      
        |                  |      
  +-----------+      +-----------+
  | NamedCExp |      |  Lifted   |
  +-----------+      +-----------+
        |                  |      
        |                  |      
  +-----------+      +-----------+
  |  ErlExpr  |      |    ANF    |
  +-----------+      +-----------+
        |                  |      
        |                  |      
+---------------+    +-----------+
|AbstractFormat |    |  VMCode   |
+---------------+    +-----------+

I am still not very familiar with Core Erlang. What benefits do you think targeting Core Erlang could bring? If it can bring performance gains I would be very interested in such a change.

[yurrriq]

Thanks for that explanation. That makes a lot of sense. I'm still using Idris 1.x, and had forgotten about the compiler redesign. This is very exciting. I'm not sure there would be any meaningful efficiency boost. The main benefit, I think, would be that Core Erlang is smaller and easier to reason about. It's also more explicit about scoping. But if you're already targeting the Erlang Abstract Format, I'd say it would be just for the novelty. I'll have a play, maybe tonight or tomorrow. Great stuff.

[yurrriq]

Some progress here, but I'm not yet able to build successfully.

make[1]: Entering directory '/build/idris2/tests'
idris2 --build tests.ipkg
1/1: Building Main (Main.idr)
make[1]: Leaving directory '/build/idris2/tests'
make -C libs/prelude IDRIS2=../../build/exec/idris2erl IDRIS2_PATH="/build/idris2/libs/prelude/build/ttc:/build/idris2/libs/base/build/ttc:/build/idris2/libs/contrib/build/ttc:/build/idris2/libs/network/build/ttc"
make[1]: Entering directory '/build/idris2/libs/prelude'
../../build/exec/idris2erl --build prelude.ipkg
Exception in foreign-procedure: no entry for "idris2_setupTerm"
make[1]: *** [Makefile:2: all] Error 255
make[1]: Leaving directory '/build/idris2/libs/prelude'
make: *** [Makefile:66: prelude] Error 2
builder for '/nix/store/qd5vfjczyw86vdz1w8z5dlz6y8xs86r9-idris2erl-0.1.0.drv' failed with exit code 2
error: build of '/nix/store/qd5vfjczyw86vdz1w8z5dlz6y8xs86r9-idris2erl-0.1.0.drv' failed

[chrrasmussen]

Very cool! The error message that you pasted (Exception in foreign-procedure: no entry for "idris2_setupTerm") is related to a recent change in Idris 2 (idris-lang/Idris2#576). Do I understand it correctly that your default.nix depends on an existing idris2 Nix package (seen in nativeBuildInputs)? The problem might be that the existing idris2 package is too old to build Idris2-Erlang. Could you possibly build idris2 from master? Or maybe pin it to a more recent commit.

There are a few steps this repository could do to improve the installation process:

1. Fix the Chez bootstrap process (This repository is already containing the Idris 2 compiler)
2. Make the Erlang code generator standalone

In the short-term I will try to fix the Chez bootstrap process so that it is possible to build the Erlang code generator without relying on an existing installation of idris2.

[yurrriq]

Yeah, the version of idris2 I'm using comes from NixOS/nixpkgs@3c95f06 by way of nix/sources.json, which builds Idris 2 v0.2.1 (see pkgs/development/compilers/idris2/default.nix). Do you have a more recent commit to suggest? I can easily override and pin a different commit.

1. Maybe we can make use of the existing Nix expression (and complete the TODO while we're at it). I made a brief attempt at that, but between it being the first time I tried building Idris 2 at all, and it being late at night, I gave up easily.
2. Why not both? 😃

Også så jeg på CV-en din at du studerte ved NTNU. Før pandemien jobbet jeg i Trondheim nesten hver måned på Sportradar. Jeg elsker den byen. (jeg prøver å lære meg norsk, så dette er god praksis, sammen med å lese Naiv Super 😉)

[chrrasmussen]

I have now fixed the Chez bootstrapping process. It might still be easier for you to depend on the idris2 Nix package.

I have also updated the Erlang code generator with the latest changes in Idris 2. It compiles using the latest commit of Idris 2 (idris-lang/Idris2@d56b090).

Regarding building via Nix: I don't have much experience using/configuring Nix packages so can't help with that, but if you see something Idris 2 can improve to make it easier to use with Nix, I will gladly assist to fix this upstream.

For et sammentreff 😄 Trondheim er en flott by!

[yurrriq]

Thanks. I've updated to use idris-lang/Idris2@d56b090 now, and the Nix build works, as well as all the samples.

[chrrasmussen]

Nice, that's great to hear! 😃 Hope you will enjoy Idris 2 as much as I do 😁

Thanks for the PR! I will look at it tomorrow (Sunday) 😊

[brandongalbraith]

@chrrasmussen can you block the spammer mesidharth from your repo? I've reported to GH.

[brokenthumbs]

New form of phishing by getting tagged in a random repository.
Please block or delete message. @chrrasmussen

[chrrasmussen]

Thanks for reporting! I blocked and reported the spammer.