Closed g-pechorin closed 5 years ago
(my rawSystem
problem was an unrelated typo)
Hi,
This should be fixed now. Please try it again and reopen this issue if you still have issues.
Thank you, it works great now.
For my sanity (or vanity) I've attached the .bat
file that I am testing it with.
@ECHO OFF
REM check for idris and add it to the path
IF EXIST %~dp0/idris/idris.exe (
ECHO "Idris exists"
) ELSE (
ECHO "I need Idris extracted to %~dp0"
ECHO "... so the main program should land as %~dp0/idris/idris.exe"
ECHO "> https://neon.se/idris/idris-1.3.1-win64.exe"
EXIT /B 1
)
SET IDRIS_HOME=%~dp0\idris
SET PATH=%IDRIS_HOME%;%IDRIS_HOME%/mingw/bin;%PATH%
REM check for idris-jvm, run the install and add it to the path
IF EXIST %~dp0/idris-jvm\bin\install.bat (
ECHO "idris-jvm is present"
) ELSE (
ECHO "I need idris-jvm extracted to %~dp0"
ECHO "... so that i can reach the .bat file at %~dp0/idris-jvm/bin/install.bat"
ECHO "> https://github.com/mmhelloworld/idris-jvm/releases/tag/v1.0-SNAPSHOT-20190525"
EXIT /B 1
)
CMD /C "cd idris-jvm\bin && install.bat"
SET PATH=%~dp0/idris-jvm/codegen/bin;%PATH%
REM do a hello-world program
ECHO module Main > hello.idr
ECHO main : IO () >> hello.idr
ECHO main = putStrLn "Hello idris-jvm" >> hello.idr
idris --portable-codegen jvm.bat %~dp0/hello.idr -o %~dp0/target/hello
java -cp %~dp0/idris-jvm/idris-jvm-runtime.jar;%~dp0/target/hello main.Main
Thank you.
I'm using idris-jvm on Windows 7 and 10 and have encountered a (non-blocking) error during setup.
The install "runs" but emits the error "Error: Could not find or load main class io.github.mmhelloworld.idrisjvm.runtime.ffi.TypeProvider" about halfway through.
steps to reproduce on Windows7/10
install.bat
from itsbin/
folderC:\Users\Peter\Desktop\error\idris-jvm\bin λ SET PATH=%IDRIS_HOME%;%IDRIS_HOME%/mingw/bin;%PATH%
C:\Users\Peter\Desktop\error\idris-jvm\bin λ install.bat Type checking .\IdrisJvm\FFI.idr Type checking .\Java\Lang.idr Type checking .\IdrisJvm\IO.idr Type checking .\Java\Nio.idr Type checking .\Java\Util\Concurrent.idr Type checking .\Java\Util\Function.idr Type checking .\Java\Util\Stream.idr Type checking .\Java\Util.idr Type checking .\Java\IO.idr Type checking .\IdrisJvm\JvmImport.idr Type checking .\Java\Math.idr Type checking .\IdrisJvm\File.idr Error: Could not find or load main class io.github.mmhelloworld.idrisjvm.runtime.ffi.TypeProvider Type checking .\IdrisJvm\Data\Buffer.idr Type checking .\IdrisJvm\System.idr Type checking .\IdrisJvm\Effects.idr Installing IdrisJvm\Data\Buffer.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\IdrisJvm\Data Installing IdrisJvm\FFI.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\IdrisJvm Installing IdrisJvm\IO.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\IdrisJvm Installing IdrisJvm\File.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\IdrisJvm Installing IdrisJvm\JvmImport.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\IdrisJvm Installing IdrisJvm\System.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\IdrisJvm Installing Java\Util\Concurrent.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\Java\Util Installing Java\Util\Function.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\Java\Util Installing Java\Util\Stream.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\Java\Util Installing IdrisJvm\Effects.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\IdrisJvm Installing Java\IO.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\Java Installing Java\Lang.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\Java Installing Java\Nio.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\Java Installing Java\Util.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\Java Installing Java\Math.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi\Java Installing 00idrisjvmffi-idx.ibc to C:\Users\Peter\Desktop\error\idris./libs\libs\idrisjvmffi