Skip to content
Snippets Groups Projects
Commit b6af20ad authored by Shachar Itzhaky's avatar Shachar Itzhaky
Browse files

[refactor] [build] Shuffled things around in Makefile.

So that we can create both jsCoq and waCoq packages.
parent 2eeae0f2
No related branches found
No related tags found
No related merge requests found
......@@ -17,10 +17,8 @@ _build
# Node stuff
node_modules
# (webpack, if building in source dir)
ui-js/addon/*.png
*.browser.js
*.js.map
# - npm packages
/*.tgz
# Links for in-place serving
coq-pkgs
......
......@@ -19,7 +19,7 @@ OS := ${shell uname}
ARCH := $(OS)/$(WORD_SIZE)
ifeq ($(WORD_SIZE),64)
DUNE_WORKSPACE = $(current_dir)/dune-workspace-64
DUNE_WORKSPACE = $(current_dir)/dune-workspace.64
VARIANT = +64bit
else
VARIANT = +32bit
......@@ -66,13 +66,15 @@ endif
all:
@echo "Welcome to jsCoq makefile. Targets are:"
@echo ""
@echo " jscoq: build jscoq [javascript and libraries]"
@echo " jscoq: build jsCoq [JavaScript and libraries]"
@echo " wacoq: build waCoq [JavaScript, frontend only; depends on wacoq-bin]"
@echo ""
@echo " links: create links that allow to serve pages from the source tree"
@echo ""
@echo " dist: create a distribution suitable for a web server"
@echo " dist-npm: create NPM packages suitable for `npm install`"
@echo " coq: download and build Coq and addon libraries"
@echo " install: install Coq and jsCoq to ~/.opam/$(BUILD_CONTEXT)"
@echo " install: install Coq version used by jsCoq to ~/.opam/$(BUILD_CONTEXT)"
jscoq: force
$(DUNE) build @jscoq $(DUNE_FLAGS)
......@@ -97,6 +99,11 @@ coq-pkgs/%.symb: coq-pkgs/%.json
libs-symb: ${patsubst %.json, %.symb, coq-pkgs/init.json ${wildcard coq-pkgs/coq-*.json}}
wacoq:
# Currently, this builds in the source tree
[ -d node_modules ] || npm install
npm run build
########################################################################
# Developer Zone #
########################################################################
......@@ -132,9 +139,8 @@ distclean: clean
########################################################################
BUILDOBJ = ${addprefix $(BUILDDIR)/./, \
cli.js coq-js/jscoq_worker.bc.js coq-pkgs \
ui-js ui-css ui-images examples \
node_modules ui-external/CodeMirror-TeX-input}
coq-js/jscoq_worker.bc.js coq-pkgs \
ui-js ui-css ui-images ui-external examples dist}
DISTOBJ = README.md index.html package.json package-lock.json $(BUILDOBJ)
DISTDIR = _build/dist
......@@ -144,7 +150,8 @@ dist: jscoq
mkdir -p $(DISTDIR)
rsync -apR --delete $(DISTOBJ) $(DISTDIR)
TAREXCLUDE = --exclude assets --exclude node_modules --exclude '*.cma' \
TAREXCLUDE = --exclude assets --exclude '*.cma' \
--exclude '*.bak' --exclude '*.tar.gz' \
${foreach dir, Coq Ltac2 mathcomp, \
--exclude '${dir}/**/*.vo' --exclude '${dir}/**/*.cma.js'}
......@@ -152,25 +159,36 @@ dist-tarball: dist
# Hack to make the tar contain a jscoq-x.x directory
@rm -f _build/jscoq-$(PACKAGE_VERSION)
ln -fs dist _build/jscoq-$(PACKAGE_VERSION)
tar zcf /tmp/jscoq-$(PACKAGE_VERSION).tar.gz \
-C _build $(TAREXCLUDE) --exclude '*.bak' --exclude '*.tar.gz' \
tar zcf /tmp/jscoq-$(PACKAGE_VERSION).tar.gz -C _build $(TAREXCLUDE) \
--dereference jscoq-$(PACKAGE_VERSION)
mv /tmp/jscoq-$(PACKAGE_VERSION).tar.gz $(DISTDIR)
@rm -f _build/jscoq-$(PACKAGE_VERSION)
NPMOBJ = ${filter-out %/node_modules %/index.html, $(DISTOBJ)}
NPMOBJ = ${filter-out index.html package-lock.json, $(DISTOBJ)}
NPMSTAGEDIR = _build/package
NPMEXCLUDE = --delete-excluded --exclude assets --exclude '*.cma' \
${foreach dir, Coq Ltac2 mathcomp, \
--exclude '${dir}/**/*.vo' --exclude '${dir}/**/*.cma.js'}
NPMEXCLUDE = --delete-excluded --exclude assets
dist-npm:
mkdir -p $(NPMSTAGEDIR) $(DISTDIR)
rsync -apR --delete $(NPMEXCLUDE) $(NPMOBJ) $(NPMSTAGEDIR)
cp docs/npm-landing.html $(NPMSTAGEDIR)/index.html
sed -i.bak 's/\(is_npm:\) false/\1 true/' $(NPMSTAGEDIR)/ui-js/jscoq-loader.js
tar zcf $(DISTDIR)/jscoq-$(PACKAGE_VERSION)-npm.tar.gz \
-C ${dir $(NPMSTAGEDIR)} --exclude '*.bak' ${notdir $(NPMSTAGEDIR)}
npm pack ./$(NPMSTAGEDIR)
WACOQ_NPMOBJ = README.md \
ui-js ui-css ui-images ui-external examples dist
# ^ plus `package.json` and `docs/npm-landing.html` that have separate treatment
dist-npm-wacoq:
mkdir -p $(NPMSTAGEDIR) $(DISTDIR)
rm -rf ${add-prefix $(NPMSTAGEDIR)/, coq-js coq-pkgs} # in case these were created by jsCoq :/
rsync -apR --delete $(NPMEXCLUDE) $(NPMOBJ) $(NPMSTAGEDIR)
cp package.json.wacoq $(NPMSTAGEDIR)/package.json
cp docs/npm-landing.html $(NPMSTAGEDIR)/index.html
npm pack ./$(NPMSTAGEDIR)
# The need to maintain and update `package.json.wacoq` alongside `package.json`
# is absolutely bothersome. I could not conjure a more sustainable way to emit
# two separate NPM packages from the same source tree, though.
########################################################################
# Local stuff and distributions
......
This diff is collapsed.
......@@ -2,10 +2,8 @@
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="content-type" content="text/html;charset=utf-8" />
<title>Using jsCoq with NPM (a template)</title>
<title>jsCoq NPM package</title>
<!-- important: this will not work from *within* the jsCoq package dir; -->
<!-- this template is meant to be copied to your project dir and edited -->
<script src="./ui-js/jscoq-loader.js"></script>
</head>
......@@ -34,12 +32,11 @@ Inductive and_they_run := too(*!*).
var jscoq_opts = {
prelude: true,
implicit_libs: true,
base_path: './node_modules/jscoq/',
editor: { mode: { 'company-coq': true }, keyMap: 'default' },
editor: { mode: { 'company-coq': true } },
init_pkgs: ['init'],
all_pkgs: ['coq']
};
JsCoq.start(jscoq_opts.base_path, '..', jscoq_ids, jscoq_opts);
JsCoq.start(jscoq_ids, jscoq_opts);
</script>
</body>
File moved
......@@ -51,8 +51,12 @@
"ui-js",
"ui-css",
"ui-images",
"ui-external/CodeMirror-TeX-input/addon",
"examples"
"ui-external",
"coq-js/*.bc.js",
"coq-pkgs",
"examples",
"dist",
"index.html"
],
"scripts": {
"build": "webpack --mode production",
......
{
"name": "wacoq",
"version": "0.13.2",
"description": "A port of Coq to WebAssembly -- run Coq in your browser",
"bin": {
"wacoqdoc": "ui-js/jscoqdoc.js"
},
"dependencies": {
"@corwin.amber/hastebin": "^0.1.1",
"array-equal": "^1.0.0",
"bootstrap": "^3.4.1",
"child-process-promise": "^2.2.1",
"codemirror": "^5.61.0",
"commander": "^5.0.0",
"fflate-unzip": "^0.7.0",
"find": "^0.3.0",
"glob": "^7.1.3",
"jquery": "^3.6.0",
"jszip": "^3.5.0",
"localforage": "^1.7.3",
"lodash": "^4.17.20",
"minimatch": "^3.0.4",
"mkdirp": "^1.0.4",
"neatjson": "^0.8.3",
"path": "^0.12.7",
"vue": "^2.6.12",
"vue-context": "^5.1.0",
"wacoq-bin": "0.13.2"
},
"devDependencies": {
"@types/find": "^0.2.1",
"@types/mkdirp": "^1.0.1",
"@types/node": "^13.11.1",
"assert": "^2.0.0",
"css-loader": "^5.2.4",
"file-loader": "^6.0.0",
"mocha": "^9.0.3",
"process": "^0.11.10",
"sass": "^1.26.3",
"sass-loader": "^8.0.2",
"stream-browserify": "^3.0.0",
"style-loader": "^1.1.3",
"ts-loader": "^9.2.5",
"typescript": "^4.3.5",
"vue-loader": "^15.9.8",
"vue-template-compiler": "^2.6.12",
"webpack": "^5.49.0",
"webpack-cli": "^4.7.2"
},
"files": [
"ui-js",
"ui-css",
"ui-images",
"ui-external",
"examples",
"dist",
"index.html"
],
"scripts": {
"build": "webpack --mode production",
"build:dev": "webpack",
"watch": "webpack -w",
"prepack": "sed -i.bak 's/\\(is_npm:\\) false/\\1 true/' ui-js/jscoq-loader.js"
},
"repository": {
"type": "git",
"url": "git+https://github.com/ejgallego/jscoq.git"
},
"author": "ejgallego",
"license": "AGPL-3.0-or-later",
"bugs": {
"url": "https://github.com/ejgallego/jscoq/issues"
},
"homepage": "https://jscoq.github.io"
}
......@@ -6,5 +6,6 @@
"esModuleInterop": true,
"resolveJsonModule": true,
"downlevelIteration": true
}
},
"exclude": ["_build", "dist"]
}
\ No newline at end of file
......@@ -122,7 +122,7 @@ module.exports = (env, argv) => [
},
output: {
filename: 'collab.browser.js',
path: path.join(__dirname, '../dist/addon'),
path: path.join(__dirname, 'dist/addon'),
library: 'addonCollab',
libraryTarget: 'umd'
},
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment