Remix.run Logo
maplant 3 hours ago

Idris is bootstrapped on scheme if I recall correctly

attila-lendvai 2 hours ago | parent [-]

it's bootstrapped off of GHC.

it was only using ChezScheme as an optimizing compiler backend.

(i created a PR to refactor their build system to reify the bootstrap process all the way down from GHC. it basically generalized the normal build workflow of Idris2 to be able to animate the entire bootstrap chain from GHC. sadly, it was pretty much ignored, and later abandoned: https://github.com/idris-lang/Idris2/pull/1990)

soegaard 2 hours ago | parent [-]

From the Idris 2 documentation:

    >> Can Idris 2 compile itself?
    > Yes, Idris 2 is implemented in Idris 2. By default, it targets Chez Scheme, 
    > so you can bootstrap from the generated Scheme code, as described in Section 
    > Getting Started.
Also, check this talk:

https://www.youtube.com/watch?v=h9YAOaBWuIk

attila-lendvai an hour ago | parent [-]

well, i wouldn't call that beeing bootstrapped.

in this case the generated scheme code is just a strange form of executable file that happens to need ChezScheme to be executed.

i.e. an ELF64 idris2 linux binary vs. an idris2.scm file that needs ChezScheme to come alive.

as for Idris2 implemented in Idris2: well, yes, that's true for the current version of Idris2. but the first version of Idris2 was written in Idris1. and the first version of Idris1 was written in Haskell.