Merge branch 'master' into better-names

INSTALL.md

@@ -12,7 +12,7 @@ On Windows, it has been reported that installing via `MSYS2` works
 (https://www.msys2.org/). On Raspberry Pi, you can bootstrap via Racket.
 
 By default, code generation is via Chez Scheme. You can use Racket instead,
-by passing `CG=racket` to `make` for the commands below.
+by setting the environment variable `IDRIS2_CG=racket` before running `make`.
 
 [Note: a couple of tests are currently known to fail when installing via
 Racket. This will be addressed soon!]

Makefile

@@ -24,13 +24,7 @@ endif
 
 export IDRIS2_VERSION := ${MAJOR}.${MINOR}.${PATCH}
 IDRIS2_SUPPORT := libidris2_support${SHLIB_SUFFIX}
-
-CG ?= ${IDRIS2_CG}
-ifneq (${CG},racket)
 IDRIS2_IPKG := idris2.ipkg
-else
-    IDRIS2_IPKG := idris2rkt.ipkg
-endif
 
 ifeq ($(OS), windows)
 	IDRIS2_PREFIX := $(shell cygpath -m ${PREFIX})

bootstrap-rkt.sh

@@ -23,8 +23,8 @@ echo ${PREFIX}
 IDRIS2_BOOT_PATH="${PREFIX}/idris2-0.2.0/prelude:${PREFIX}/idris2-0.2.0/base:${PREFIX}/idris2-0.2.0/contrib:${PREFIX}/idris2-0.2.0/network"
 DYLIB_PATH="${PREFIX}/lib"
 
-make libs CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH}
+make libs IDRIS2_CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH}
-make install CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH}
+make install IDRIS2_CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH}
 make clean IDRIS2_BOOT=${PREFIX}/bin/idris2 LD_LIBRARY_PATH=${DYLIB_PATH}
-make all IDRIS2_BOOT=${PREFIX}/bin/idris2 CG=racket IDRIS2_PATH=${IDRIS2_BOOT_PATH} LD_LIBRARY_PATH=${DYLIB_PATH}
+make all IDRIS2_BOOT=${PREFIX}/bin/idris2 IDRIS2_CG=racket IDRIS2_PATH=${IDRIS2_BOOT_PATH} LD_LIBRARY_PATH=${DYLIB_PATH}
 #make test INTERACTIVE='' IDRIS2_BOOT=${PREFIX}/bin/idris2 CG=racket IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_LIBS=${PREFIX}/idris2-0.2.0/lib LD_LIBRARY_PATH=${DYLIB_PATH}

docs/source/backends/gambit.rst

@@ -8,9 +8,15 @@ The Gambit Scheme code generator can be accessed via the REPL command:
 
     Main> :set cg gambit
 
-Ergo, to run Idris programs with this generator, you will need to install
+Alternatively, you can set it via the `IDRIS2_CG` environment variable:
+
+::
+
+    $ export IDRIS2_CG=gambit
+
+To run Idris programs with this generator, you will need to install
 `Gambit Scheme <https://gambitscheme.org>`_. Gambit Scheme is free software,
-and available via most pacakge managers.
+and available via most package managers.
 
 You can compile an expression ``expr`` of type ``IO ()`` to an executable as
 follows, at the REPL:

docs/source/backends/index.rst

@@ -40,6 +40,8 @@ Again, ``expr`` must have type ``IO ()``.
 There are three code generators provided in Idris 2, and (later) there will be
 a system for plugging in new code generators for a variety of targets. The
 default is to compile via Chez Scheme, with an alternative via Racket or Gambit.
+You can set the code generator at the REPL with the `:set codegen` command,
+or via the `IDRIS2_CG` environment variable.
 
 .. toctree::
    :maxdepth: 1

docs/source/backends/racket.rst

@@ -8,6 +8,12 @@ The Racket code generator is accessed via a REPL command:
 
     Main> :set cg racket
 
+Alternatively, you can set it via the `IDRIS2_CG` environment variable:
+
+::
+
+    $ export IDRIS2_CG=racket
+
 You can compile an expression ``expr`` of type ``IO ()`` to an executable as
 follows, at the REPL:
 

src/Compiler/Scheme/Chez.idr

@@ -71,7 +71,8 @@ schHeader chez libs
     "(case (machine-type)\n" ++
     "  [(i3le ti3le a6le ta6le) (load-shared-object \"libc.so.6\")]\n" ++
     "  [(i3osx ti3osx a6osx ta6osx) (load-shared-object \"libc.dylib\")]\n" ++
-    "  [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")]\n" ++
+    "  [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")" ++ 
+    "                           (load-shared-object \"ws2_32.dll\")]\n" ++
     "  [else (load-shared-object \"libc.so\")])\n\n" ++
     showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeString x ++ "\")") libs) ++ "\n\n" ++
     "(let ()\n"
@@ -332,7 +333,7 @@ startChezWinSh chez appdir target = unlines
     , "DIR=\"`realpath \"$0\"`\""
     , "CHEZ=$(cygpath \"" ++ chez ++"\")"
     , "export PATH=\"`dirname \"$DIR\"`/\"" ++ appdir ++ "\":$PATH\""
-    , "\"$CHEZ\" --script \"$(dirname \"$DIR\")/" ++ target ++ "\" \"$@\""
+    , "$CHEZ --script \"$(dirname \"$DIR\")/" ++ target ++ "\" \"$@\""
     ]
 
 ||| Compile a TT expression to Chez Scheme
@@ -374,7 +375,7 @@ compileToSO chez appDirRel outSsAbs
          Right () <- coreLift $ writeFile tmpFileAbs build
             | Left err => throw (FileErr tmpFileAbs err)
          coreLift $ chmodRaw tmpFileAbs 0o755
-         coreLift $ system ("\"" ++ chez ++ "\" --script \"" ++ tmpFileAbs ++ "\"")
+         coreLift $ system (chez ++ " --script \"" ++ tmpFileAbs ++ "\"")
          pure ()
 
 makeSh : String -> String -> String -> Core ()

src/Idris/Main.idr

@@ -37,11 +37,10 @@ findInput [] = Nothing
 findInput (InputFile f :: fs) = Just f
 findInput (_ :: fs) = findInput fs
 
--- Add extra library directories from the "BLODWEN_PATH"
+-- Add extra data from the "IDRIS2_x" environment variables
--- environment variable
+updateEnv : {auto c : Ref Ctxt Defs} ->
-updatePaths : {auto c : Ref Ctxt Defs} ->
             Core ()
-updatePaths
+updateEnv
     = do bprefix <- coreLift $ getEnv "IDRIS2_PREFIX"
          the (Core ()) $ case bprefix of
               Just p => setPrefix p
@@ -58,6 +57,13 @@ updatePaths
          the (Core ()) $ case blibs of
               Just path => do traverse_ addLibDir (map trim (split (==pathSep) path))
               Nothing => pure ()
+         cg <- coreLift $ getEnv "IDRIS2_CG"
+         the (Core ()) $ case cg of
+              Just e => case getCG e of
+                             Just cg => setCG cg
+                             Nothing => throw (InternalError ("Unknown code generator " ++ show e))
+              Nothing => pure ()
+
          -- IDRIS2_PATH goes first so that it overrides this if there's
          -- any conflicts. In particular, that means that setting IDRIS2_PATH
          -- for the tests means they test the local version not the installed
@@ -78,7 +84,7 @@ updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->
 updateREPLOpts
     = do opts <- get ROpts
          ed <- coreLift $ getEnv "EDITOR"
-         case ed of
+         the (Core ()) $ case ed of
               Just e => put ROpts (record { editor = e } opts)
               Nothing => pure ()
 
@@ -133,7 +139,7 @@ stMain opts
          addPrimitives
 
          setWorkingDir "."
-         updatePaths
+         updateEnv
          let ide = ideMode opts
          let ideSocket = ideModeSocket opts
          let outmode = if ide then IDEMode 0 stdin stdout else REPL False

tests/chez/chez014/Echo.idr

@@ -52,7 +52,6 @@ runClient serverPort = do
 
 main : IO ()
 main = do
-  when (os == "windows") (schemeCall () "load-shared-object" ["ws2_32"])
   Right (serverPort, tid) <- runServer
     | Left err => putStrLn $ "[server] " ++ err
   runClient serverPort