Open jbsolomon opened 4 years ago
I've tried to build Prelude as follows:
First I set IDRIS2_PATH
and IDRIS2_DATA
in my environment to equal the values (with Windows-style path separators) from the Makefile.
Then I cd to libs\prelude
and run ..\..\idris2.exe --install prelude.ipkg
. The library builds successfully but I get the error Uncaught error: File error (prelude): File Read Error
.
I wonder if some of the mixed-up path separators in these variables are causing the error?
C:\Users\bodie\meta\build\Idris2\libs\prelude>..\..\idris2.exe --paths
+ Working Directory :: "C:\\Users\\bodie\\meta\\build\\Idris2\\libs\\prelude"
+ Source Directory :: Nothing
+ Build Directory :: "build"
+ Executable Directory :: "build/exec"
+ Installation Prefix :: "C:\\Users\\bodie\\.idris2"
+ Extra Directories :: [".", "C:\\Users\\bodie\\meta\\build\\Idris2\\libs\\prelude\\build\\ttc", "C:\\Users\\bodie\\meta\\build\\Idris2\\libs\\base\\build\\ttc", "C:\\Users\\bodie\\.idris2/idris2-0.0.0/prelude", "C:\\Users\\bodie\\.idris2/idris2-0.0.0/base"]
+ CG Library Directories :: [".", "C:\\Users\\bodie\\.idris2/idris2-0.0.0/lib"]
+ Data Directories :: ["C:\\Users\\bodie\\meta\\build\\Idris2\\support", "C:\\Users\\bodie\\.idris2/idris2-0.0.0/support"]
Hi,
I built Idris2 from source on 28b7c62521a01ec4e4924cd77b904387fca47137 without using Make or MSYS2 by simply writing
YafflePaths.idr
by hand, uncommentingopts = "--partial-eval -O2 --cg-opt -lws2_32"
inidris2.ipkg
, and runningidris --build idris2.ipkg
.Edit: I realize now that the missing libs is already mentioned in the Idris repo: https://github.com/idris-lang/Idris-dev/wiki/Windows-Binaries#troubleshooting
The rest of my comments deal with building Prelude and the rest of the base libs.