WebAssembly Backend

.circleci/config.yml

@@ -32,23 +32,23 @@ common_steps: &common_steps
           opam init --disable-sandboxing -j 1 -n -y
           sed -i "s/^jobs: [0-9]*/jobs: $NJOBS/g" ~/.opam/config
           eval $(opam env)
-          opam switch create 4.07.1 || true
-          opam switch set 4.07.1
+          opam switch create $OCAML_VERSION || true
+          opam switch set $OCAML_VERSION
           opam repo add coq-released https://coq.inria.fr/opam/released || true
           opam update || true
     - run:
         name: "Install OCaml deps"
         command: |
-          opam install -y -v --jobs=2 ocamlbuild menhir base64 js_of_ocaml js_of_ocaml-ppx yojson atdgen re calendar uri
+          opam install -y -v --jobs=2 dune menhir base64 js_of_ocaml js_of_ocaml-ppx yojson atdgen re calendar uri wasm.1.0.1
     - run:
         name: "Install Coq"
         command: |
-          opam install -y -v coq.8.8.2 coq-flocq coq-jsast
+          opam install -y -v coq.8.12.0 coq-flocq coq-jsast
         no_output_timeout: 30m
     - run:
         name: "Install Q*cert"
         command: |
-          opam install -y -v coq-qcert.1.4.1
+          opam install -y -v coq-qcert.2.1.0
         no_output_timeout: 30m
     - save_cache:
         <<: *common_cache_key
@@ -64,7 +64,7 @@ common_steps: &common_steps
         name: 'Build the Ergo compiler'
         command:  |
           eval $(opam env)
-          make setup
+          make configure
           make all
     - run:
         name: 'Testing'
@@ -73,12 +73,12 @@ common_steps: &common_steps
 
 version: 2
 jobs:
-  4.07.1:
+  4.09.1:
     docker:
     - image: circleci/openjdk:8-jdk
     environment:
       - TERM: dumb
-      - OCAML_VERSION: "4.07.x"
+      - OCAML_VERSION: "4.09.1"
       - CIRCLE_TEST_REPORTS: /tmp/circleci-test-results
       - NJOBS: 2
       - NPM_CONFIG_PREFIX: "~/.npm-global"
@@ -88,4 +88,4 @@ workflows:
   version: 2
   build-deploy:
     jobs:
-      - 4.07.1
+      - 4.09.1

.gitignore

@@ -18,9 +18,13 @@ Makefile.config
 *~
 .#*
 *.vo
+*.vos
+*.vok
 *.v.d
 *.glob
 *.aux
+*.lia.cache
+.Makefile.coq.d
 *.ctoj
 .DS_Store
 _CoqProject
@@ -44,3 +48,7 @@ website/i18n/*
 !website/i18n/en.json
 *.sw[p]
 thumbs.db
+
+# generated by dune
+*.merlin
+*.install

DEVELOPERS.md

@@ -29,12 +29,12 @@ Before you can build Ergo, you must install and configure the following prerequi
 $ npm install -g lerna@^3.15.0
 ```
 
-* [opam](https://opam.ocaml.org): the OCaml package manager, for OCaml 4.07.1. To install:
+* [opam](https://opam.ocaml.org): the OCaml package manager, for OCaml 4.09.1. To install:
 
 ```sh
 $ sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)
 $ eval $(opam env)
-$ opam switch create 4.07.1
+$ opam switch create 4.09.1
 ```
 
 #### Install development version
@@ -53,8 +53,8 @@ To rebuild the compiler from the source, you will need Coq 8.8.2 and OCaml 4.07.
 
 ```sh
 $ opam repo add coq-released https://coq.inria.fr/opam/released
-$ opam install ocamlbuild menhir base64 js_of_ocaml js_of_ocaml-ppx yojson atdgen re calendar uri
-$ opam install coq.8.8.2 coq-qcert.1.4.1
+$ opam install dune menhir base64 js_of_ocaml js_of_ocaml-ppx yojson atdgen re calendar uri wasm.1.0.1
+$ opam install coq.8.8.2 coq-qcert.2.0.0
 ```
 
 ##### Build the Ergo Compiler and REPL
@@ -63,7 +63,7 @@ To recompile Ergo from its source, do:
 
 ```sh
 $ make cleanall
-$ make setup
+$ make configure
 $ make all
 ```
 
@@ -80,7 +80,7 @@ If successful, you should find the following binaries in the `bin/` directory:
 We write unit and integration tests with Mocha and Cucumber. To run all of the tests once run:
 
 ```text
-lerna run test
+npm run test
 ```
 
 ###  Writing Documentation

Makefile

@@ -20,48 +20,95 @@ include Makefile.coq_modules
 #
 CP=cp
 
-FILES = $(addprefix mechanization/,$(MODULES:%=%.v))
+FILES = $(addprefix compiler/core/,$(MODULES:%=%.v))
 
 ## Compiler
 all:
+	@$(MAKE) prepare
 	@$(MAKE) MAKEFLAGS= ergo
 
-# Setup
-setup:
-	@$(MAKE) npm-setup
+# Stdlib
+
+%.ctoj: %.cto
+	./scripts/cto2ctoj.js parse $<
+
+compiler/lib/resources.ml: compiler/stdlib/accordproject.ctoj \
+                           compiler/stdlib/stdlib.ergo \
+                           compiler/stdlib/etime.ergo \
+                           compiler/stdlib/template.ergo \
+                           runtimes/javascript/ergo-runtime.js
+	echo '(* generated ocaml file *)' > compiler/lib/resources.ml
+	(for i in accordproject; do \
+         echo "let $$i = {xxx|"; \
+         cat compiler/stdlib/$$i.ctoj; \
+         echo "|xxx}"; \
+         done) >> compiler/lib/resources.ml
+	(for i in stdlib etime template; do \
+         echo "let $$i = {xxx|"; \
+         cat compiler/stdlib/$$i.ergo; \
+         echo "|xxx}"; \
+         done) >> compiler/lib/resources.ml
+	(for i in runtime; do \
+         echo "let ergo_$$i = {xxx|"; \
+         cat ./runtimes/javascript/ergo-$$i.js; \
+         echo "|xxx}"; \
+         done) >> compiler/lib/resources.ml
+	(echo `date "+let builddate = {xxx|%b %d, %Y|xxx}"`) >> compiler/lib/resources.ml
+
+# Configure
+runtimes/javascript/ergo-runtime.js: runtimes/javascript/ergo-runtime-core.js \
+                           runtimes/javascript/ergo-runtime-tostring.js \
+                           runtimes/javascript/ergo-runtime-date-time.js \
+                           runtimes/javascript/ergo-runtime-log.js \
+                           runtimes/javascript/ergo-runtime-math.js \
+                           runtimes/javascript/ergo-runtime-uri.js
+	$(MAKE) -C ./runtimes/javascript
+
+./compiler/lib/js_runtime.ml: ./runtimes/javascript/ergo_runtime.ml
+	cp ./runtimes/javascript/ergo_runtime.ml ./compiler/lib/js_runtime.ml
+
+./compiler/lib/static_config.ml:
+	echo "(* This file is generated *)" > ./compiler/lib/static_config.ml
+	echo "let ergo_home = \"$(CURDIR)\"" >> ./compiler/lib/static_config.ml
+
+prepare: ./compiler/lib/static_config.ml compiler/lib/resources.ml Makefile.coq
+	$(MAKE) -C ./runtimes/javascript
+
+configure:
+	@echo "[Ergo] "
+	@echo "[Ergo] Configuring Build"
+	@echo "[Ergo] "
+	npm install
+	@$(MAKE) prepare
 
 # Regenerate the npm directory
 ergo:
 	@$(MAKE) ergo-mechanization
-	@$(MAKE) MAKEFLAGS= ergo-extraction-refresh
+	@$(MAKE) MAKEFLAGS= ergo-ocaml-extraction
+	@$(MAKE) MAKEFLAGS= ergo-js-extraction
 
 ergo-mechanization: _CoqProject Makefile.coq
 	@echo "[Ergo] "
 	@echo "[Ergo] Compiling Coq Mechanization"
 	@echo "[Ergo] "
 	@$(MAKE) -f Makefile.coq
 
-ergo-extraction:
+ergo-ocaml-extraction:
 	@echo "[Ergo] "
-	@echo "[Ergo] Compiling the extracted OCaml"
+	@echo "[Ergo] Extracting Ergo Compiler to OCaml"
 	@echo "[Ergo] "
-	@$(MAKE) -C extraction all
+	@$(MAKE) -C compiler/extraction
+	dune build @install
 
-ergo-extraction-refresh:
+ergo-js-extraction:
 	@echo "[Ergo] "
-	@echo "[Ergo] Extracting mechanization to OCaml"
+	@echo "[Ergo] Extracting Ergo Compiler to JavaScript"
 	@echo "[Ergo] "
-	@$(MAKE) -C extraction all-refresh
-
-npm-setup:
-	@echo "[Ergo] "
-	@echo "[Ergo] Setting up for Node.js build"
-	@echo "[Ergo] "
-	npm install
+	@$(MAKE) -C compiler/libjs
 
 ## Documentation
 documentation:
-	$(MAKE) -C mechanization documentation
+	$(MAKE) -C compiler/core documentation
 
 ## Testing
 test:
@@ -73,20 +120,26 @@ clean-mechanization: Makefile.coq
 
 cleanall-mechanization:
 	- @$(MAKE) -f Makefile.coq cleanall
+	- @rm -f ./compiler/lib/js_runtime.ml ./compiler/lib/static_config.ml compiler/lib/resources.ml
 	- @rm -f Makefile.coq
 	- @rm -f Makefile.coq.conf
 	- @rm -f _CoqProject
-	- @find mechanization \( -name '*.vo' -or -name '*.v.d' -or -name '*.glob'  -or -name '*.aux' \) -print0 | xargs -0 rm -f
+	- @find compiler/core \( -name '*.vo' -or -name '*.v.d' -or -name '*.glob'  -or -name '*.aux' \) -print0 | xargs -0 rm -f
+
+clean-ocaml-extraction:
+	- @$(MAKE) -C compiler/extraction clean
+
+cleanall-ocaml-extraction:
+	- @$(MAKE) -C compiler/extraction cleanall
+	- dune clean
 
-clean-extraction:
-	- @$(MAKE) -C extraction clean
+clean-js-extraction:
+	- @$(MAKE) -C compiler/libjs clean
 
-cleanall-extraction:
-	- @$(MAKE) -C extraction cleanall
+cleanall-js-extraction:
+	- @$(MAKE) -C compiler/libjs cleanall
 
 clean-npm:
-	- @rm -f package-lock.json
-	- @rm -rf dist
 
 cleanall-npm: clean-npm
 	- @node ./scripts/external/cleanExternalModels.js
@@ -99,31 +152,34 @@ cleanall-npm: clean-npm
 
 clean: Makefile.coq
 	- @$(MAKE) clean-npm
-	- @$(MAKE) clean-extraction
+	- @$(MAKE) clean-ocaml-extraction
+	- @$(MAKE) clean-js-extraction
 	- @$(MAKE) -C packages/ergo-compiler clean
 	- @$(MAKE) -C packages/ergo-engine clean
 	- @$(MAKE) -C packages/ergo-cli clean
+	- @$(MAKE) -C runtimes/javascript clean
 
 cleanall: Makefile.coq
 	@echo "[Ergo] "
 	@echo "[Ergo] Cleaning up"
 	@echo "[Ergo] "
 	- @$(MAKE) cleanall-npm
-	- @$(MAKE) cleanall-extraction
+	- @$(MAKE) cleanall-ocaml-extraction
 	- @$(MAKE) cleanall-mechanization
 	- @$(MAKE) -C packages/ergo-compiler cleanall
 	- @$(MAKE) -C packages/ergo-engine cleanall
 	- @$(MAKE) -C packages/ergo-cli cleanall
+	- @$(MAKE) -C runtimes/javascript cleanall
 
 ##
 _CoqProject: Makefile.config
 	@echo "[Ergo] "
 	@echo "[Ergo] Setting up Coq"
 	@echo "[Ergo] "
 ifneq ($(QCERT),)
-	(echo "-R mechanization ErgoSpec -R $(QCERT)/coq Qcert";) > _CoqProject
+	(echo "-R compiler/core ErgoSpec -R $(QCERT)/compiler/core Qcert";) > _CoqProject
 else
-	(echo "-R mechanization ErgoSpec";) > _CoqProject
+	(echo "-R compiler/core ErgoSpec";) > _CoqProject
 endif
 
 Makefile.coq: _CoqProject Makefile $(FILES)

Makefile.config

@@ -13,4 +13,4 @@
 #
 
 ## Qcert compiler location
-#QCERT=../qcert-master
+QCERT=qcert