feat(idris-lang#3400): generate only es6 -> implement, but not tested…

… on libraries

Makefile

@@ -77,10 +77,11 @@ ${TARGET}: support src/IdrisPaths.idr
 
 # We use FORCE to always rebuild IdrisPath so that the git SHA1 info is always up to date
 src/IdrisPaths.idr: FORCE
-	echo "-- @""generated" > src/IdrisPaths.idr
-	echo 'module IdrisPaths' >> src/IdrisPaths.idr
-	echo 'export idrisVersion : ((Nat,Nat,Nat), String); idrisVersion = ((${MAJOR},${MINOR},${PATCH}), "${VERSION_TAG}")' >> src/IdrisPaths.idr
-	echo 'export yprefix : String; yprefix="${IDRIS2_PREFIX}"' >> src/IdrisPaths.idr
+	@printf '%s\n' \
+	'-- @generated' \
+	'module IdrisPaths' \
+	'export idrisVersion : ((Nat,Nat,Nat), String); idrisVersion = ((${MAJOR},${MINOR},${PATCH}), "${VERSION_TAG}")' \
+	'export yprefix : String; yprefix="${IDRIS2_PREFIX}"' > src/IdrisPaths.idr
 
 FORCE:
 
@@ -126,10 +127,17 @@ ${TEST_PREFIX}/${NAME_VERSION} :
 
 .PHONY: ${TEST_PREFIX}/${NAME_VERSION}
 
-${TEST_IDRIS2_SUPPORT_DIR}/${IDRIS2_SUPPORT}:
+# FIXME:
+# make support
+# 	installs to /home/srghma/projects/Idris2/support/c/libidris2_support.so
+# 	.h files are at /home/srghma/projects/Idris2/support/c/getline.h
+# make test-support
+# 	installs to /home/srghma/projects/Idris2/build/env/idris2-0.7.0/lib/libidris2_support.so
+# 	maybe should to /home/srghma/projects/Idris2/build/env/idris2-0.7.0/support/c/getline.h ???
+${TEST_IDRIS2_SUPPORT_DIR}/lib/${IDRIS2_SUPPORT}:
 	${MAKE} install-support PREFIX=${TEST_PREFIX}
 
-test-support: ${TEST_IDRIS2_SUPPORT_DIR}/${IDRIS2_SUPPORT}
+test-support: ${TEST_IDRIS2_SUPPORT_DIR}/lib/${IDRIS2_SUPPORT}
 
 testenv: test-support
 	mkdir -p ${TEST_PREFIX}/${NAME_VERSION}

docs/source/backends/javascript.rst

@@ -1,5 +1,5 @@
 ***********************************
-Javascript and Node Code Generators
+Browser and Node Code Generators
 ***********************************
 
 There are two javascript code generators, ``node`` and ``javascript``. There are two

docs/source/cookbook/Calculator.idr

@@ -1,3 +1,5 @@
+module Calculator
+
 import Data.List1
 import Text.Lexer
 import Text.Parser

docs/source/cookbook/LambdaCalculus.idr

@@ -1,3 +1,5 @@
+module LambdaCalculus
+
 import Data.List
 import Data.List1
 import Text.Lexer

docs/source/ffi/ffi.rst

@@ -87,8 +87,7 @@ or ``javascript``. The former two are mutually exclusive while ``javascript``
 FFI specifiers apply both when building for the browser and when building for
 NodeJS.
 
-Javascript specifiers must be further specialized as ``lambda``, ``support``,
-or ``stringIterator``.
+Javascript specifiers must be further specialized as ``lambda``, ``support``.
 
 The syntax, therefore, is ``node:lambda:some_func`` (for the NodeJS-specific
 FFI and a lambda that executes a function named ``some_func``).

flake.nix

@@ -85,7 +85,7 @@
           });
           inherit buildIdris;
           devShells.default = pkgs.mkShell.override { stdenv = stdenv'; } {
-            packages = [ idris2Pkg.buildInputs chez ];
+            packages = [ idris2Pkg.buildInputs chez pkgs.python3 ];
             SCHEME="scheme";
           };
         };

idris2api.ipkg

@@ -28,7 +28,7 @@ modules =
     Compiler.ES.Ast,
     Compiler.ES.Codegen,
     Compiler.ES.Doc,
-    Compiler.ES.Javascript,
+    Compiler.ES.Browser,
     Compiler.ES.Node,
     Compiler.ES.State,
     Compiler.ES.TailRec,

libs/base/Makefile

@@ -1,14 +1,22 @@
-all:
+all: build
+.PHONY: all
+
+build:
 	${IDRIS2} --build base.ipkg
+.PHONY: build
 
 install:
 	${IDRIS2} --install base.ipkg
+.PHONY: install
 
 install-with-src:
 	${IDRIS2} --install-with-src base.ipkg
+.PHONY: install-with-src
 
 docs:
 	${IDRIS2} --mkdoc base.ipkg
+.PHONY: docs
 
 clean:
 	$(RM) -r build
+.PHONY: clean

libs/contrib/Data/String/Iterator.idr

@@ -24,7 +24,7 @@ data StringIterator : String -> Type where [external]
 %foreign
   "scheme:blodwen-string-iterator-new"
   "RefC:stringIteratorNew"
-  "javascript:stringIterator:new"
+  "javascript:support"
 private
 fromString : (str : String) -> StringIterator str
 
@@ -39,7 +39,7 @@ withString str f = f (fromString str)
 %foreign
   "scheme:blodwen-string-iterator-to-string"
   "RefC:stringIteratorToString"
-  "javascript:stringIterator:toString"
+  "javascript:support"
 export
 withIteratorString : (str : String)
                   -> (1 it : StringIterator str)
@@ -64,7 +64,7 @@ data UnconsResult : String -> Type where
 %foreign
   "scheme:blodwen-string-iterator-next"
   "RefC:stringIteratorNext"
-  "javascript:stringIterator:next"
+  "javascript:support"
 export
 uncons : (str : String) -> (1 it : StringIterator str) -> UnconsResult str
 

libs/contrib/Makefile

@@ -1,14 +1,22 @@
-all:
+all: build
+.PHONY: all
+
+build:
 	${IDRIS2} --build contrib.ipkg
+.PHONY: build
 
 install:
 	${IDRIS2} --install contrib.ipkg
+.PHONY: install
 
 install-with-src:
 	${IDRIS2} --install-with-src contrib.ipkg
+.PHONY: install-with-src
 
 docs:
 	${IDRIS2} --mkdoc contrib.ipkg
+.PHONY: docs
 
 clean:
 	$(RM) -r build
+.PHONY: clean

libs/linear/Makefile

@@ -1,14 +1,22 @@
-all:
+all: build
+.PHONY: all
+
+build:
 	${IDRIS2} --build linear.ipkg
+.PHONY: build
 
 install:
 	${IDRIS2} --install linear.ipkg
+.PHONY: install
 
 install-with-src:
 	${IDRIS2} --install-with-src linear.ipkg
+.PHONY: install-with-src
 
 docs:
 	${IDRIS2} --mkdoc linear.ipkg
+.PHONY: docs
 
 clean:
 	$(RM) -r build
+.PHONY: clean

libs/network/Makefile

@@ -1,14 +1,23 @@
-all:
+all: build
+.PHONY: all
+
+build:
 	${IDRIS2} --build network.ipkg
+.PHONY: build
 
 install:
 	${IDRIS2} --install network.ipkg
+.PHONY: install
 
 install-with-src:
 	${IDRIS2} --install-with-src network.ipkg
+.PHONY: install-with-src
 
 docs:
 	${IDRIS2} --mkdoc network.ipkg
+.PHONY: docs
 
 clean:
 	$(RM) -r build
+.PHONY: clean
+

libs/papers/Makefile

@@ -1,14 +1,22 @@
-all:
+all: build
+.PHONY: all
+
+build:
 	${IDRIS2} --build papers.ipkg
+.PHONY: build
 
 install:
 	${IDRIS2} --install papers.ipkg
+.PHONY: install
 
 install-with-src:
 	${IDRIS2} --install-with-src papers.ipkg
+.PHONY: install-with-src
 
 docs:
 	${IDRIS2} --mkdoc papers.ipkg
+.PHONY: docs
 
 clean:
 	$(RM) -r build
+.PHONY: clean

libs/prelude/Makefile

@@ -1,14 +1,22 @@
-all:
+all: build
+.PHONY: all
+
+build:
 	${IDRIS2} --build prelude.ipkg
+.PHONY: build
 
 install:
 	${IDRIS2} --install prelude.ipkg
+.PHONY: install
 
 install-with-src:
 	${IDRIS2} --install-with-src prelude.ipkg
+.PHONY: install-with-src
 
 docs:
 	${IDRIS2} --mkdoc prelude.ipkg
+.PHONY: docs
 
 clean:
 	$(RM) -r build
+.PHONY: clean

libs/test/Makefile

@@ -1,14 +1,22 @@
-all:
+all: build
+.PHONY: all
+
+build:
 	${IDRIS2} --build test.ipkg
+.PHONY: build
 
 install:
 	${IDRIS2} --install test.ipkg
+.PHONY: install
 
 install-with-src:
 	${IDRIS2} --install-with-src test.ipkg
+.PHONY: install-with-src
 
 docs:
 	${IDRIS2} --mkdoc test.ipkg
+.PHONY: docs
 
 clean:
 	$(RM) -r build
+.PHONY: clean

libs/test/Test/Golden.idr

@@ -109,7 +109,7 @@ record Options where
   ||| How many threads should we use?
   threads      : Nat
   ||| Should we write the list of failing cases to a file?
-  failureFile     : Maybe String
+  failureFile  : Maybe String
 
 export
 initOptions : String -> Bool -> Options
@@ -126,7 +126,7 @@ initOptions exe color
 export
 usage : String
 usage = unwords
-  ["Usage:"
+  [ "Usage:"
   , "runtests <path>"
   , "[--timing]"
   , "[--interactive]"