[build] Some cleanup.

Makefile

@@ -5,10 +5,10 @@
 -include ./config.inc
 
 # Coq Version
-COQ_VERSION:=v8.12
-JSCOQ_BRANCH:=
+COQ_VERSION := v8.12
+JSCOQ_BRANCH :=
 
-JSCOQ_VERSION:=$(COQ_VERSION)
+JSCOQ_VERSION := $(COQ_VERSION)
 
 ifdef JSCOQ_BRANCH
 JSCOQ_VERSION:=$(JSCOQ_VERSION)-$(JSCOQ_BRANCH)
@@ -26,6 +26,7 @@ VARIANT = +32bit
 endif
 
 BUILD_CONTEXT = jscoq$(VARIANT)
+BUILDDIR = _build/$(BUILD_CONTEXT)
 
 # ugly but I couldn't find a better way
 current_dir := $(dir $(realpath $(lastword $(MAKEFILE_LIST))))
@@ -54,9 +55,6 @@ export COQBUILDDIR_REL
 export ADDONS_PATH
 export COQPKGS_ROOT
 
-# Addons supported in jsCoq 0.11
-ADDONS = mathcomp # extlib simpleio quickchick elpi equations dsp
-
 all:
 	@echo "Welcome to jsCoq makefile. Targets are:"
 	@echo ""
@@ -69,23 +67,21 @@ all:
 	@echo "   install: install Coq and jsCoq to ~/.opam/$(BUILD_CONTEXT)"
 
 jscoq: force
-	ADDONS="$(ADDONS)" dune build @jscoq $(DUNE_FLAGS)
+	dune build @jscoq $(DUNE_FLAGS)
 
 jscoq_worker:
-	ADDONS="$(ADDONS)" dune build @jscoq_worker $(DUNE_FLAGS)
+	dune build @jscoq_worker $(DUNE_FLAGS)
 
 install:
-	dune build $(COQBUILDDIR_REL)/coq.install jscoq.install $(DUNE_FLAGS)
-	dune install coq jscoq $(DUNE_FLAGS)
+	dune build $(COQBUILDDIR_REL)/coq.install $(DUNE_FLAGS)
+	dune install coq $(DUNE_FLAGS)
 
 links:
 	ln -sf _build/$(BUILD_CONTEXT)/coq-pkgs .
 	ln -sf ../_build/$(BUILD_CONTEXT)/coq-js/jscoq_worker.bc.js coq-js/jscoq_worker.js
-#	ln -sf ../_build/$(BUILD_CONTEXT)/ui-js/coq-build.browser.js ui-js
 
 links-clean:
 	rm -f coq-pkgs coq-js/jscoq_worker.js
-#	ui-js/coq-build.browser.js
 
 # Build symbol database files for autocomplete
 coq-pkgs/%.symb: coq-pkgs/%.json
@@ -104,13 +100,12 @@ clean:
 # Dists                                                                #
 ########################################################################
 
-BUILDDIR=_build/$(BUILD_CONTEXT)
-BUILDOBJ=${addprefix $(BUILDDIR)/./, \
+BUILDOBJ = ${addprefix $(BUILDDIR)/./, \
 	coq-js/jscoq_worker.bc.js coq-pkgs \
 	ui-js ui-css ui-images examples \
 	node_modules ui-external/CodeMirror-TeX-input}
 DISTOBJ = README.md index.html package.json package-lock.json $(BUILDOBJ)
-DISTDIR=_build/dist
+DISTDIR = _build/dist
 
 PACKAGE_VERSION = ${shell node -p 'require("./package.json").version'}
 
@@ -169,9 +164,9 @@ all-dist: dist dist-release dist-upload
 
 .PHONY: coq coq-get coq-get-latest coq-build
 
-COQ_BRANCH=V8.12.0
-COQ_BRANCH_LATEST=v8.12
-COQ_REPOS=https://github.com/coq/coq.git
+COQ_BRANCH = V8.12.0
+COQ_BRANCH_LATEST = v8.12
+COQ_REPOS = https://github.com/coq/coq.git
 
 COQ_PATCHES = trampoline cps timeout $(COQ_PATCHES|$(WORD_SIZE)) $(COQ_PATCHES|$(ARCH))
 
@@ -183,32 +178,31 @@ $(COQSRC):
 	cd $@ && git apply ${foreach p,$(COQ_PATCHES),$(current_dir)/etc/patches/$p.patch}
 
 coq-get: $(COQSRC)
+	eval `opam env --switch=$(BUILD_CONTEXT)` && \
 	cd $(COQSRC) && ./configure -prefix $(COQDIR) -native-compiler no -bytecode-compiler no -coqide no
 
 coq-get-latest: COQ_BRANCH = $(COQ_BRANCH_LATEST)
 coq-get-latest: coq-get
 
-# Coq should be now be built by composition with the Dune setup
-coq-build:
-	true
+coq: coq-get
+
+test:
+	@cp -r tests $(BUILDDIR)
+	cd $(BUILDDIR) && npx mocha tests/main.js
+
+server:
+	npx http-server $(BUILDDIR) -p 8012
+
 
-coq: coq-get coq-build
+# - These are deprecated (use jscoq/addons repo instead)
 
 addon-%-get:
 	make -f coq-addons/$*.addon get
 
 addon-%-build:
 	make -f coq-addons/$*.addon build
-#	make -f coq-addons/$*.addon jscoq-install
 
 addons-get: ${foreach v,$(ADDONS),addon-$(v)-get}
 addons-build: ${foreach v,$(ADDONS),addon-$(v)-build}
 
 addons: addons-get addons-build
-
-test:
-	npx mocha tests/main.js
-
-server:
-	npx http-server _build/jscoq+32bit &
-	google-chrome http://127.0.0.1:8080 &

etc/docker/Dockerfile

@@ -60,7 +60,7 @@ RUN eval $(opam env) && make dist-tarball && make dist-npm \
 
 # - install to OPAM for use by package builds
 RUN eval $(opam env) && make install &&   \
-    ln -s /root/jscoq/_build/jscoq+64bit/coq-pkgs $OPAM_SWITCH_PREFIX/bin
+    cd _build/jscoq+* && npm link
 
 ARG ADDONS_REPO=https://github.com/jscoq/addons
 ARG ADDONS_BRANCH=v8.12

index.html

@@ -3,6 +3,7 @@
   <head>
     <meta http-equiv="content-type" content="text/html;charset=utf-8" />
     <meta name="description" content="An Online IDE for the Coq Theorem Prover" />
+    <link rel="icon" href="ui-images/favicon.ico">
 
     <link rel="stylesheet" type="text/css" href="node_modules/bootstrap/dist/css/bootstrap.min.css">
     <style>

package.json

@@ -2,6 +2,9 @@
   "name": "jscoq",
   "version": "0.12.0-rc1",
   "description": "A port of Coq to JavaScript -- run Coq in your browser",
+  "bin": {
+      "jscoq" : "./cli.js"
+  },
   "dependencies": {
     "array-equal": "^1.0.0",
     "bootstrap": "^3.4.1",

ui-js/dune

@@ -11,6 +11,7 @@
  (targets ide-project.browser.js ide-project.browser.js.map)
  (deps
   (source_tree .)
-  (source_tree ../coq-jslib/build))
+  (source_tree ../coq-jslib/build)
+  ../node_modules)
  (action
   (bash "npx webpack --config-name ide-project")))

ui-js/webpack.config.js

@@ -4,6 +4,9 @@ module.exports = {
   mode: 'development',
   entry: './ide-project.js',
   devtool: "source-map",
+  stats: {
+    hash: false, version: false, modules: false  // reduce verbosity
+  },
   output: {
     filename: 'ide-project.browser.js',
     path: __dirname,