diff --git a/Makefile b/Makefile index 84aee6b58..7860e2e35 100644 --- a/Makefile +++ b/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,9 +235,6 @@ 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 @@ -253,12 +242,6 @@ 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] " diff --git a/compiler/dune b/compiler/dune index 185f72efb..7efbc3046 100644 --- a/compiler/dune +++ b/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}) diff --git a/compiler/wasm/wasm_backend.ml b/compiler/wasm/wasm_backend.ml index df7a74b9d..b56024cf6 100644 --- a/compiler/wasm/wasm_backend.ml +++ b/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 diff --git a/runtimes/assemblyscript/assemblyscript.ml b/runtimes/assemblyscript/assemblyscript.ml deleted file mode 100644 index 105814721..000000000 --- a/runtimes/assemblyscript/assemblyscript.ml +++ /dev/null @@ -1,11 +0,0 @@ -module Runtime = struct - 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 - ) -end diff --git a/runtimes/assemblyscript/assemblyscript_runtime.ml b/runtimes/assemblyscript/assemblyscript_runtime.ml new file mode 100644 index 000000000..7539d78c4 --- /dev/null +++ b/runtimes/assemblyscript/assemblyscript_runtime.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 + ) diff --git a/runtimes/assemblyscript/dune b/runtimes/assemblyscript/dune index bc95f8c23..78757fce6 100644 --- a/runtimes/assemblyscript/dune +++ b/runtimes/assemblyscript/dune @@ -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) diff --git a/runtimes/assemblyscript/test_ml/dune b/runtimes/assemblyscript/test_ml/dune index ca15013fc..186bbae00 100644 --- a/runtimes/assemblyscript/test_ml/dune +++ b/runtimes/assemblyscript/test_ml/dune @@ -1,3 +1,3 @@ (tests (names force_wasm_ast) - (libraries coq-qcert.assemblyscript)) + (libraries coq-qcert.runtime.assemblyscript)) diff --git a/runtimes/assemblyscript/test_ml/force_wasm_ast.ml b/runtimes/assemblyscript/test_ml/force_wasm_ast.ml index a0f16ee1e..9c33ba4fb 100644 --- a/runtimes/assemblyscript/test_ml/force_wasm_ast.ml +++ b/runtimes/assemblyscript/test_ml/force_wasm_ast.ml @@ -1 +1 @@ -let _ = Lazy.force Assemblyscript.Runtime.wasm_ast +let _ = Lazy.force Assemblyscript_runtime.wasm_ast diff --git a/runtimes/javascript/.gitignore b/runtimes/javascript/.gitignore index d908e1359..8366ba46a 100644 --- a/runtimes/javascript/.gitignore +++ b/runtimes/javascript/.gitignore @@ -1,2 +1 @@ qcert-runtime.js -qcert_runtime.ml diff --git a/runtimes/javascript/Makefile b/runtimes/javascript/Makefile deleted file mode 100644 index 494a2ae98..000000000 --- a/runtimes/javascript/Makefile +++ /dev/null @@ -1,34 +0,0 @@ -# -# Licensed under the Apache License, Version 2.0 (the "License"); -# you may not use this file except in compliance with the License. -# You may obtain a copy of the License at -# -# http://www.apache.org/licenses/LICENSE-2.0 -# -# Unless required by applicable law or agreed to in writing, software -# distributed under the License is distributed on an "AS IS" BASIS, -# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -# See the License for the specific language governing permissions and -# limitations under the License. -# - -############# Shouldn't have to be changed after this -all: qcert-runtime.js qcert_runtime.ml - -qcert-runtime.js: qcert-runtime-core.js qcert-runtime-tostring.js qcert-runtime-sql-date.js qcert-runtime-uri.js - (for i in qcert-runtime-core.js qcert-runtime-tostring.js qcert-runtime-sql-date.js qcert-runtime-uri.js; do \ - cat $$i; \ - done) > qcert-runtime.js - -qcert_runtime.ml: qcert-runtime.js - (echo "let runtime = {runtime|"; \ - cat qcert-runtime.js; \ - echo '|runtime}' \ - ) > qcert_runtime.ml - -clean: - -rm -f qcert-runtime.js qcert_runtime.ml - -rm -f *~ - -cleanall: clean - diff --git a/runtimes/javascript/dune b/runtimes/javascript/dune new file mode 100644 index 000000000..51afa9f39 --- /dev/null +++ b/runtimes/javascript/dune @@ -0,0 +1,33 @@ +(library + (name js_runtime) + (public_name coq-qcert.runtime.js)) + +(rule ; We promote to source dir because this file is also used from nodejs. + (target qcert-runtime.js) + (mode promote) + (deps + qcert-runtime-core.js + qcert-runtime-tostring.js + qcert-runtime-sql-date.js + qcert-runtime-uri.js) + (action + (with-stdout-to + qcert-runtime.js + (progn (echo "/* include: qcert-runtime-core.js */\n\n") + (cat qcert-runtime-core.js) + (echo "/* include: qcert-runtime-tostring.js */\n\n") + (cat qcert-runtime-tostring.js) + (echo "/* include: qcert-runtime-sql-date.js */\n\n") + (cat qcert-runtime-sql-date.js) + (echo "/* include: qcert-runtime-uri */\n\n") + (cat qcert-runtime-uri.js))))) + +(rule + (target js_runtime.ml) + (deps qcert-runtime.js) + (action + (with-stdout-to + js_runtime.ml + (progn (echo "let runtime = {|\n") + (cat qcert-runtime.js) + (echo "|}\n")))))