Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Javascript #415

Merged
merged 30 commits into from Jul 8, 2020
Merged

Javascript #415

merged 30 commits into from Jul 8, 2020

Conversation

rbarreiro
Copy link
Contributor

javascript backend

Copy link
Collaborator

@melted melted left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Bah, trying to disable the merge button with request changes didn't work.

@melted
Copy link
Collaborator

melted commented Jul 5, 2020

Can you make this a draft? This requires discussions, and @edwinb need to decide if we want to put in another backend.

@melted
Copy link
Collaborator

melted commented Jul 5, 2020

Related, backends don't have to live in the idris2 source tree: https://idris2.readthedocs.io/en/latest/backends/custom.html

@melted melted marked this pull request as draft July 5, 2020 19:06
@melted
Copy link
Collaborator

melted commented Jul 5, 2020

Hey, I could make it a draft!

@edwinb
Copy link
Collaborator

edwinb commented Jul 5, 2020

On the "should we have another backend" question, I think while we should be careful not to have to maintain too many, JS is too useful to not be included by default. (And, as a tiebreaker, Idris 1 has a JS back end by default.)

Beyond that, I'm not really well qualified to comment, so I'll see how the discussion goes!

@rbarreiro
Copy link
Contributor Author

Related, backends don't have to live in the idris2 source tree: https://idris2.readthedocs.io/en/latest/backends/custom.html

Yes I know, I don't mind making it a separate backend. When I started that possibility was not available so I forked. And since there is a request for javascript in CONTRIBUTING.md I decided to make a merge request, but I am perfectly fine to make it separate.

@edwinb
Copy link
Collaborator

edwinb commented Jul 5, 2020

Oh, one thing that is worth checking is what adding a new back end does to build times - code generation from the generated Chez already takes a bit too long. I don't expect it'll be too disastrous, but let's at least be a bit careful at least until we have a way of generating code faster.

@@ -1509,9 +1510,32 @@ prim__putChar : Char -> (1 x : %World) -> IORes ()
%foreign "C:getchar,libc 6"
%extern prim__getChar : (1 x : %World) -> IORes Char

read_line_js : String
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

move this to a separate module and import it.

why are there two read_line_js?

@@ -17,26 +17,71 @@ support fn = "C:" ++ fn ++ ", libidris2_support"
libc : String -> String
libc fn = "C:" ++ fn ++ ", libc 6"

js_try_catch_lasterr_Int : String -> String
js_try_catch_lasterr_Int x = "{try{" ++ x ++ ";return 0n}catch(e){process.__lasterr = e; return 1n}}"
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

move all these functions to a separate module.

use camelcase names


read_line_js : String
read_line_js =
"(file_ptr =>{
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

move to a separate module

camelcase names

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

An alternative is to put functions such as these in a file in support/js.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It'd probably be neater to put them in support/js, especially for consistency with the Scheme back ends

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

An alternative is to put functions such as these in a file in support/js.

I can go that way, I didn't went that way to avoid unnecessary definitions on the generated js. Should I do it?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it will scale better than leaving javascript code scattered around the libs as string literals. If you are concerned about code bloat, you could put the functions in separate files.

@edwinb
Copy link
Collaborator

edwinb commented Jul 5, 2020

I've tried this out - build time doesn't increase significantly, so that's no problem, and the tests pass. I just have a couple of small requests:

  • I had to update my node because the version I had on my system (Ubuntu LTS) was too old. Please could you add a note to the README saying what the minimum requirement is?
  • For consistency, please could the generated executable be put under build/exec - at first I couldn't find them because that's where I looked!

Thanks for the contribution, anyway! I think this is something which will interested quite a few people (me included).

@chrrasmussen
Copy link
Contributor

Regarding the output location that @edwinb mentioned: Changing let out = outfile to let out = outputDir </> outfile should fix this (in src/Compiler/ES/Javascript.idr and src/Compiler/ES/Node.idr).

By default this will output the generated file(s) to build/exec, but by specifying --output-dir it is possible to change the output directory: idris2 --cg node --output-dir . -o foo.js Main.idr will generate foo.js in the current directory.

@rbarreiro
Copy link
Contributor Author

I think I have addressed all issues, you may check again.

@melted
Copy link
Collaborator

melted commented Jul 6, 2020

I wondered if the Imperative was more generally useful and could be moved out. But that can easily be done later.

@melted melted marked this pull request as ready for review July 6, 2020 18:39
melted
melted previously approved these changes Jul 6, 2020
@melted melted dismissed their stale review July 6, 2020 18:40

not a review

@clayrat clayrat mentioned this pull request Jul 7, 2020
@edwinb
Copy link
Collaborator

edwinb commented Jul 8, 2020

If nobody else has any comments, I think this is good to go now (and, it certainly doesn't do any harm!).

Ideally we'll also need documentation (like the other backends: https://idris2.readthedocs.io/en/latest/backends/index.html) but this can be added in later PRs.

Thanks again for the contribution!

@edwinb edwinb merged commit 23cbc28 into idris-lang:master Jul 8, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

6 participants