Align Js_runtime build and Assemblyscript_runtime build.

Author: pkel

Makefile

@@ -113,17 +113,11 @@ cleanmost-qcert-compiler:
 
 ## Configure
 
-runtimes/javascript/qcert_runtime.ml:
-	$(MAKE) -C runtimes/javascript
-
-compiler/lib/js_runtime.ml: runtimes/javascript/qcert_runtime.ml
-	cp runtimes/javascript/qcert_runtime.ml compiler/lib/js_runtime.ml
-
 compiler/lib/static_config.ml:
 	echo "(* This file is generated *)" > compiler/lib/static_config.ml
 	echo "let qcert_home = \"$(CURDIR)\"" >> compiler/lib/static_config.ml
 
-prepare: compiler/lib/js_runtime.ml compiler/lib/static_config.ml Makefile.coq
+prepare: compiler/lib/static_config.ml Makefile.coq
 
 configure:
 	@echo "[Q*cert] "
@@ -134,8 +128,6 @@ configure:
 clean-configure:
 
 cleanall-configure:
-	$(MAKE) -C runtimes/javascript cleanall
-	rm -rf compiler/lib/js_runtime.ml
 	rm -rf compiler/lib/static_config.ml
 	rm -f compiler/.merlin compiler/*/.merlin
 
@@ -243,22 +235,13 @@ qcert-runtimes:
 	@echo "[Q*cert] "
 	@echo "[Q*cert] Building runtimes"
 	@echo "[Q*cert] "
-ifneq ($(JAVASCRIPT),)
-	@$(MAKE) javascript-runtime
-endif
 ifneq ($(JAVA),)
 	@$(MAKE) java-runtime
 endif
 ifneq ($(SPARK),)
 	@$(MAKE) spark2-runtime
 endif
 
-javascript-runtime:
-	@echo "[Q*cert] "
-	@echo "[Q*cert] JavaScript runtime"
-	@echo "[Q*cert] "
-	@$(MAKE) -C runtimes/javascript
-
 java-runtime:
 	@echo "[Q*cert] "
 	@echo "[Q*cert] Java runtime"
@@ -272,14 +255,12 @@ spark2-runtime:
 	@$(MAKE) -C runtimes/spark2
 
 clean-runtimes:
-	- @$(MAKE) -C runtimes/javascript clean
 	- @$(MAKE) -C runtimes/java clean
 	- @$(MAKE) -C runtimes/spark2 clean
 	- @rm -rf bin/lib
 	- @rm -f bin/javaRunner.jar
 
 cleanall-runtimes:
-	- @$(MAKE) -C runtimes/javascript cleanall
 	- @$(MAKE) -C runtimes/java cleanall
 	- @$(MAKE) -C runtimes/spark2 cleanall
 	- @rm -rf bin/lib
@@ -337,10 +318,7 @@ demo:
 bin/qcertJS.js:
 	@$(MAKE) qcert-javascript
 
-runtimes/javascript/qcert-runtime.js:
-	@$(MAKE) javascript-runtime
-
-qcert-demo: bin/qcertJS.js runtimes/javascript/qcert-runtime.js
+qcert-demo: bin/qcertJS.js
 	@echo "[Q*cert] "
 	@echo "[Q*cert] Compiling Web Demo in TypeScript"
 	@echo "[Q*cert] "

compiler/dune

@@ -9,8 +9,9 @@
 (library
  (name qcert_lib)
  (public_name coq-qcert)
- (libraries base64 uri calendar wasm coq-qcert.assemblyscript)
-)
+ (libraries base64 uri calendar wasm
+            coq-qcert.runtime.assemblyscript
+            coq-qcert.runtime.js))
 
 (copy_files util/*.{ml,mli})
 (copy_files wasm/*.{ml,mli})

compiler/wasm/wasm_backend.ml

@@ -21,7 +21,7 @@ end = struct
   open ImpEJson
   module Encoding = Wasm_binary_ejson.Make(ImpEJson)
 
-  let runtime = Lazy.force Assemblyscript.Runtime.wasm_ast
+  let runtime = Lazy.force Assemblyscript_runtime.wasm_ast
 
   let ejson_of_cejson = function
     | Coq_cejnull -> Coq_ejnull

runtimes/assemblyscript/assemblyscript.ml

@@ -0,0 +1,9 @@
+let string = Stringified.runtime
+
+let wasm_ast =
+  lazy (
+    let open Wasm in
+    let m = Decode.decode "runtime.wasm" string in
+    let () = Valid.check_module m in
+    m
+  )

runtimes/assemblyscript/assemblyscript_runtime.ml

@@ -1,6 +1,6 @@
 (library
-  (name assemblyscript)
-  (public_name coq-qcert.assemblyscript)
+  (name assemblyscript_runtime)
+  (public_name coq-qcert.runtime.assemblyscript)
   (libraries wasm))
 
 (rule ; not evaluated for package release (-p flag)

runtimes/assemblyscript/dune

@@ -1,3 +1,3 @@
 (tests
   (names force_wasm_ast)
-  (libraries coq-qcert.assemblyscript))
+  (libraries coq-qcert.runtime.assemblyscript))

runtimes/assemblyscript/test_ml/dune

@@ -1 +1 @@
-let _ = Lazy.force Assemblyscript.Runtime.wasm_ast
+let _ = Lazy.force Assemblyscript_runtime.wasm_ast

runtimes/assemblyscript/test_ml/force_wasm_ast.ml

@@ -1,2 +1 @@
 qcert-runtime.js
-qcert_runtime.ml