When specifying the idris-jvm backend as the idris2 url for a package set, building an Idris2 project with pack causes the build to fail with the following error:
43/95: Building Debug.Trace (Debug/Trace.idr)
Error: The given specifier '["jvm:toString(java/lang/Object java/lang/String),java/util/Objects"]' was not accepted
by any backend. Available backends:
chez, chez-sep, racket, node, javascript, refc, gambit, vmcode-interp
Some backends have additional specifier rules, refer to their documentation.
This is because the pack bootstrapping process does not use a previous version of the idris-jvm compiler to build the idris-jvm compiler. Instead, it will try to run make bootstrap as part of Pack.Runner.Install.mkIdris, which idris-jvm does not use. Idris-jvm bootstraps the compiler by running the following commands (as seen in its GitHub Actions install workflow):
These commands use Maven to download a previous version of the Idris2 compiler from Maven Central, and then use that downloaded compiler to build the new compiler.
I think pack should allow a custom bootstrapping script to be specified to allow external backends like idris-jvm to be used with pack.
When specifying the idris-jvm backend as the idris2 url for a package set, building an Idris2 project with
pack
causes the build to fail with the following error:This is because the
pack
bootstrapping process does not use a previous version of the idris-jvm compiler to build the idris-jvm compiler. Instead, it will try to runmake bootstrap
as part ofPack.Runner.Install.mkIdris
, which idris-jvm does not use. Idris-jvm bootstraps the compiler by running the following commands (as seen in its GitHub Actions install workflow):These commands use Maven to download a previous version of the Idris2 compiler from Maven Central, and then use that downloaded compiler to build the new compiler.
I think
pack
should allow a custom bootstrapping script to be specified to allow external backends like idris-jvm to be used withpack
.