Racket bytecode

[benhormann]

raco exe vs. raco make

I reckon the Racket backend should use raco make instead of raco exe: https://docs.racket-lang.org/raco/make.html

Pros:
(1) produces bytecode (more consistent with the Chez backend)
      - much smaller than wrapping the bytecode around Racket's binary
      - slightly simpler (avoids idris2 vs. idris2.exe)
(2) faster! — saves 15-20% for idris2.rkt / 75-85% for hello.rkt (ymmv)
(3) skips compilation if the source didn't change (SHA-1)
Cons:
(4) programs die after upgrading Racket
      - error message: loading code: version mismatch expected: "8.2" found: "8.0"
      - the user must rm -rf compiled; raco make *.rkt
Other:
(5) you can easily run make exe later (bonus: it uses the bytecode)
(6?) fixes the M1 macOS / support dylib issue (speculation — tested on 10.15)

So if someone can confirm (6), this is a double win.

You can try it out, like so:

raco make bootstrap/idris2_app/idris2.rkt
LD_LIBRARY_PATH=$PWD/support/c racket bootstrap/idris2_app/idris2.rkt --version

---

Other improvements

• Fixes some shell quoting (i.e. pathnames with spaces)
  • Normalises* quotes for system on windows
  • Removes shebang and calls to /usr/bin/env
• Checks exit status of system calls to Chez / Raco / Gambit compiler
• Better bootstrap
  • Uses separate build directory (no longer cleans libs/*/build)
  • Remove redundant --build step for libs (still does --install)
  • You can rerun ./bootstrap-stage2.sh directly
  • no left over bootstrap files in your ~/.idris2/bin

* I chose parameter separater ; since it doesn't conflict with PowerShell. It even works with goto labels... It's the closest thing to whitespace that isn't whitespace.

cmd | MS Docs
If the previous conditions aren't met, string is processed by examining the first character to verify whether it is an opening quotation mark. If the first character is an opening quotation mark, it is stripped along with the closing quotation mark. Any text following the closing quotation marks is preserved.

[attila-lendvai]

FWIW, these two will have loads of conflict: #1990

[benhormann]

Not really. Sure, #1990 will drop my bootstrap change. I kept changes to Makefile minimal to reduce merging effort (most merge conflicts are deletes / pick yours).

I'm happy to help with 1990 btw, though it looks like you have it under control. Note: raco make idris2.racket produces compiled/idris2_racket.zo.

[benhormann]

There is also a conflict with #1749. I'm not sure of the implications memory wise, but I can update my code if 1749 gets accepted.

[benhormann]

The change to bytecode allows us to execute racket directly, avoiding macOS System Integrity Protection issues (libidris2_support.dylib not found). All that remains to fix #1032 are any M1 specific quirks (e.g. Rosetta — according to reddit).

FYI: GitHub are upgrading the macos-latest label tomacos-11 soon.

---

This PR also fixes path quoting issues and closes #1244. But if anyone is passing options via SCHEME, that will no longer work.

[gallais]

(2) faster! — saves 15-20% for idris2.rkt / 75-85% for hello.rkt (ymmv)

Faster to compile or to run?

[gallais]

Why are we installing racket for the chezscheme test?

[benhormann]

It was more to prove that the Racket backend tests work on the CI (there are no Racket tests enabled otherwise — currently the windows build is the only use of Racket).

Seemed like a good idea at the time. With ubuntu-bootstrap-racket disabled, I'd say it still is.

[benhormann]

It'd be tidier to have a separate job. The test prefix makes things a bit awkward, or can it just run make -C tests only=racket?

[benhormann]

I have removed this workflow change.

[benhormann]

(2) faster! — saves 15-20% for idris2.rkt / 75-85% for hello.rkt (ymmv)

Faster to compile or to run?

Compile. The bytecode ought to be equivalent, so no difference at runtime.

[benhormann]

@gallais I'm rebasing, but saw this. This file/dir appears unused, removing it didn't break anything.

Regardless, shouldn't it be: install ${TARGET}_app/${IDRIS2_SUPPORT} ${PREFIX}/lib? (i.e. the same file it was compiled against, otherwise it could differ from the one in bin/idris2_app)
edit: it's support/c/Makefile that should be changed, not here.

[benhormann]

Actually, shouldn't it be compiling bytecode against the freshly built lib instead of the previous version's copy? We can use IDRIS2_LIBS to make that happen.

[benhormann]

@gallais This is now waiting on you. Unless you want me to add a ubuntu-test-racket-codegen job?

[benhormann]

@gallais I'd like to also reinstate Racket bootstrap to the CI, but that needs #2279.

How about adding another Ubuntu job to build Racket from previous-version (Chez), then self-host from it?
Could even have self-hosted racket and bootstrapped racket running make test in parallel.

I'm tidying up the Windows shell using msys2 as the default, so all the CI work could go together in another PR.

[gallais]

Sorry I don't have the headspace for that atm, I'm trying to get #1990 mergd first.
I'm happy to see a racket build come back, it's only turned off because it was broken
and no one was willing to investigate & fix it. Reactivating it should be as simple as
removing a fale && from the if: condition IIRC.

[CodingCellist]

With the closure of #1990, what does the status of this become? Should it still be considered for merging (possibly with some changes), or should it be closed?

[CodingCellist]

Given that this was labelled abandoned ~2 months ago and no work or complaints have arisen, including during the IDM in early December 2022, I'm closing this. If it is still relevant, please make the required changes before reopening.