[feature] SDK wrapper script.

Currently separate from the main cli, but for no good reason.
Should be a sub-command.

coq-jslib/build/sdk/sdk.ts

+// UNTIL THIS IS MERGED INTO THE CLI:
+//   tsc --allowSyntheticDefaultImports --esModuleInterop bin/sdk.ts
+import fs from 'fs';
+import path from 'path';
+import mkdirp from 'mkdirp';
+import findUp from 'find-up';
+import glob from 'glob';
+import unzip from 'fflate-unzip';
+import chld from 'child-process-promise';
+import type commander from 'commander';
+
+
+const SDK = '/tmp/wacoq-sdk';
+
+
+async function sdk(basedir = SDK, includeNative = true) {
+    mkdirp.sync(basedir);
+
+    // Locate `coq-pkgs`
+    var nm = findNM(), coqpkgsDir: string;
+    for (let sp of ['jscoq/coq-pkgs', 'wacoq-bin/bin/coq']) {
+        var fp = path.join(nm, sp);
+        if (fs.existsSync(fp)) coqpkgsDir = fp;
+    }
+    if (!coqpkgsDir) throw {err: "Package bundles (*.coq-pkg) not found"};
+
+    // - unzip everything in `coqlib`
+    var coqlibDir = path.join(basedir, 'coqlib');
+    mkdirp.sync(coqlibDir);
+    await cas(path.join(coqlibDir, '_coq-pkgs'), dirstamp(coqpkgsDir), async () => {
+        for (let fn of glob.sync('*.coq-pkg', {cwd: coqpkgsDir})) {
+            var fp = path.join(coqpkgsDir, fn);
+            await unzip(fp, coqlibDir);
+        }
+
+        // - link `theories` and `plugins` to be consistent with Coq dist structure
+        for (let link of ['theories', 'plugins'])
+            ln_sf('Coq', path.join(coqlibDir, link));
+    });
+
+    // Locate native Coq
+    if (includeNative) {
+        var coqlibNative = await findCoq();
+
+        // - link libs in `ml`
+        var mlDir = path.join(basedir, 'ml');
+        mkdirp.sync(mlDir);
+        await cas(path.join(mlDir, '_coqlib-native'), dirstamp(coqlibNative), () => {
+            for (let fn of glob.sync('**/*.cmxs', {cwd: coqlibNative}))
+                ln_sf(
+                    path.join(coqlibNative, fn),
+                    path.join(mlDir, path.basename(fn)));
+        });
+    }
+    else mlDir = undefined;
+
+    return {coqlib: coqlibDir, include: mlDir};
+}
+
+async function runCoqC(cfg: {coqlib: string, include: string},
+                       args: string[]) {
+    var {coqlib, include} = cfg,
+        args = ['-coqlib', coqlib, '-include', include, ...args];
+    try {
+        return await chld.spawn('coqc', args, {stdio: 'inherit'});
+    }
+    catch { throw {err: 'coqc error'}; }
+}
+
+/*- specific helpers -*/
+
+function findNM() {
+    var nm = findUp.sync('node_modules', {type: 'directory'});
+    if (!nm) throw {err: "node_modules directory not found"};
+    return nm;
+}
+
+async function findCoq() {
+    var cfg = await chld.exec("coqc -config"),
+        mo = cfg.stdout.match(/^COQCORELIB=(.*)/m);
+    if (!mo) throw {err: "Coq config COQCORELIB=_ not found"};
+    return mo[1];
+}
+
+/*- some shutil -*/
+
+function cat(fn: string) {
+    try {
+        return fs.readFileSync(fn, 'utf-8');
+    }
+    catch { return undefined; }
+}
+
+/**
+ * If `fn` contains `expectedValue`, do nothing;
+ * Otherwise run `whenNeq` and update `fn`.
+ * @returns `true` iff `fn` already contained `expectedValue`.
+ */
+async function cas(fn: string, expectedValue: string, whenNeq: () => void | Promise<void>) {
+    if (cat(fn) === expectedValue) return true;
+    else {
+        await whenNeq();
+        fs.writeFileSync(fn, expectedValue);
+        return false;
+    }
+}
+
+function dirstamp(fn: string) {
+    try { var s = fs.statSync(fn).mtime.toISOString(); } catch { s = '??'; }
+    return `${fn} @ ${s}`;
+}
+
+function ln_sf(target: string, source: string) {
+    try { fs.unlinkSync(source); }
+    catch { }
+    fs.symlinkSync(target, source);
+}
+
+/*- main entry point -*/
+
+async function main(args: string[]) {
+    try {
+        var cfg = await sdk();
+        var ret = await runCoqC(cfg, args);
+        return ret.code;
+    }
+    catch (e) {
+        if (e.err) console.log('oops: ' + e.err);
+        else console.error(e);
+        return 1;
+    }
+}
+
+function installCommand(commander: commander.CommanderStatic) {
+    commander.command('coqc')
+        .description("Runs `coqc` with waCoq's standard library.")
+        .allowUnknownOption(true)
+        .helpOption('-z', '(run `wacoq coqc -help` instead)')
+        .action(async opts => { await main(opts.args); });
+}
+
+
+export { main, sdk, installCommand }

coq-jslib/build/sdk/toolkit.js

+
+const fs = require('fs'), path = require('path'), os = require('os'),
+      child_process = require('child_process'),
+      sdk = require('./sdk');
+
+const ME = 'jscoq',
+      SDK_FLAGS = (process.env['JSCOQ'] || '').split(',').filter(x => x);
+
+
+class Phase {
+
+    constructor(basedir='/tmp/jscoq-sdk') {
+        this.basedir = basedir;
+    }
+
+    which(progname, skipSelf=false) {
+        if (progname.indexOf('/') >= 0) return progname;
+
+        for (let pe of process.env['PATH'].split(':')) {
+            if (skipSelf && pe.startsWith(this.basedir)) continue;
+            var full = path.join(pe, progname);
+            if (this.existsExec(full)) return full;
+        }
+        throw new Error(`${progname}: not found`);
+    }
+    
+    _exec(prog, args) {
+        if (SDK_FLAGS.includes('verbose')) {
+            console.log(`[${ME}-sdk]  `, prog, args.join(' '));
+        }
+        return child_process.execFileSync(prog, args, {stdio: 'inherit'});
+    }
+}
+
+class Hijack extends Phase {
+
+    progs = ['coqc', 'coqdep', 'coqtop']
+
+    run(prog, args) {
+        this.mkBin();
+        if (args.length > 0)
+            this._exec(this.which(args[0]), args.slice(1));
+    }
+
+    mkBin(bindir=path.join(this.basedir, 'hijack'), script=__filename) {
+        if (!fs.existsSync(bindir)) {
+            fs.mkdirSync(bindir, {recursive: true});
+            for (let tool of this.progs) {
+                fs.symlinkSync(script, path.join(bindir, tool));
+            }
+        }
+        process.env['PATH'] = `${bindir}:${process.env['PATH']}`;
+    }
+
+    existsExec(p) {
+        try {
+            let stat = fs.statSync(p);
+            return stat && stat.isFile() && (stat.mode & fs.constants.S_IXUSR);
+        }
+        catch (e) { return false; }
+    }
+
+    existsDir(p) {
+        try {
+            let stat = fs.statSync(p);
+            return stat && stat.isDirectory();
+        }
+        catch (e) { return false; }        
+    }
+}
+
+class DockerTool extends Phase {
+    dockerImage = `${ME}:sdk`
+    incdir = '/opt/jscoq/lib/coq-core';  /* points to Docker image */
+
+    async run(prog, args) {
+        const cfg = await sdk.sdk(this.basedir, false);
+        cfg.include = this.incdir;
+        this.runInContainer(prog, args, cfg);
+    }
+
+    mounts(cfg) {
+        var cwd = process.cwd(),
+            mnt = cwd.match(/[/][^/]+/)[0],
+            coqlib = cfg.coqlib;
+    
+        if (!mnt)
+            console.warn(`[${ME}-sdk] cannot detect working directory root for '${cwd}';\n` +
+                         `            this will probably not work.`)
+    
+        return [mnt, coqlib].filter(x => x).map(d => `-v${d}:${d}`);
+    }
+    
+    user() {
+        if (os.platform() === 'darwin') return [];  // seems to not work in macOS, and also unneeded
+        else {
+            var {uid, gid} = os.userInfo();
+            return ['-e', `LOCAL_USER_ID=${uid}`, '-e', `LOCAL_GROUP_ID=${gid}`];
+        }
+    }
+    
+    env(cfg) {
+        var e = {COQLIB: cfg.coqlib, COQCORELIB: cfg.include};
+        return [].concat(...Object.entries(e).map(
+            ([k, v]) => v ? ['-e', `${k}=${v}`] : []));
+    }
+    
+    runInContainer(prog, args, cfg={}) {
+        this._exec('docker', [
+            'run', ...this.mounts(cfg), ...this.user(), ...this.env(cfg),
+            `-w${process.cwd()}`, '--rm', this.dockerImage,
+            prog, ...args
+        ]);
+    }
+}
+
+
+async function main() {
+    var prog = path.basename(process.argv[1]),
+        args = process.argv.slice(2);
+
+    var Phase = {
+            'coqc': DockerTool, 'coqdep': DockerTool, 'coqtop': DockerTool
+        }[prog] ?? Hijack;
+
+    try {
+        await new Phase().run(prog, args);
+    }
+    catch (e) {
+        if (typeof e.status === 'number') process.exit(e.status);
+        console.error(`[${ME}-sdk]`, e);
+        process.exit(1);
+    }
+}
+
+main(); 
\ No newline at end of file

examples/sdk-demo/Makefile

@@ -2,13 +2,10 @@
 REPO = https://github.com/coq-contribs/group-theory.git
 WORKDIR = workdir
 
-PATH := $(PWD)/bin:$(PATH)
-export PATH
-
 build: $(WORKDIR)
 	cp dune-files/dune $(WORKDIR)/
 	# Use current workspace, not jsCoq's
-	dune build --root .
+	../../dist/toolkit.js dune build --root .
 
 $(WORKDIR):
 	git clone --recursive --depth=1 $(REPO) $@

package.json

@@ -4,6 +4,7 @@
   "description": "A port of Coq to JavaScript -- run Coq in your browser",
   "bin": {
     "jscoq": "./dist/cli.js",
+    "jscoq-sdk": "./dist/toolkit.js",
     "jscoqdoc": "ui-js/jscoqdoc.js"
   },
   "dependencies": {

webpack.config.js

@@ -3,47 +3,88 @@ const webpack = require('webpack'),
       path = require('path'),
       { VueLoaderPlugin } = require('vue-loader');
 
-module.exports = (env, argv) => [
-/**
- * jsCoq CLI
- * (note: the waCoq CLI is located in package `wacoq-bin`)
- */
-{
-  name: 'cli',
-  target: 'node',
-  entry: './coq-jslib/cli.ts',
+const
+  basics = (argv) => ({
     mode: 'development',
     devtool: argv.mode !== 'production' ? "source-map" : undefined,
     stats: {
       hash: false, version: false, modules: false  // reduce verbosity
     },
-  module: {
-    rules: [
-      {
+    performance: {
+      maxAssetSize: 1e6, maxEntrypointSize: 1e6   // 250k is too small
+    },
+  }),
+  ts = {
     test: /\.tsx?$/,
     use: 'ts-loader',
     exclude: /node_modules/,
   },
-    ],
+  css = {
+    test: /\.css$/i,
+    use: ['style-loader', 'css-loader'],
   },
-  externals: {  /* do not bundle the worker */
-    '../coq-js/jscoq_worker.bc.js': 'commonjs2 ../coq-js/jscoq_worker.bc.js',
-    'wacoq-bin/dist/subproc': 'commonjs2'
+  scss = {
+    test: /\.scss$/i,  /* Vue.js has some */
+    use: ['style-loader', 'css-loader', 'sass-loader'],
   },
-  resolve: {
-    extensions: [ '.tsx', '.ts', '.js' ],
+  imgs = {
+    test: /\.(png|jpe?g|gif)$/i,
+    loader: 'file-loader',
+    options: {
+      outputPath: 'ide-project-images',
+    }
   },
-  output: {
-    filename: 'cli.js',
-    path: path.join(__dirname, 'dist')
+  vuesfc = {
+    test: /\.vue$/,
+    use: 'vue-loader'
   },
-  plugins: [
+  cliPlugins = (scriptName) => [
     new webpack.BannerPlugin({banner: '#!/usr/bin/env node', raw: true}),
     new webpack.optimize.LimitChunkCountPlugin({maxChunks: 1}),
     function() {
-      this.hooks.afterDone.tap('chmod', () => fs.chmodSync('dist/cli.js', 0755));
+      this.hooks.afterDone.tap('chmod', () => fs.chmodSync(scriptName, 0755));
     }
   ],
+  resolve = {
+    extensions: [ '.tsx', '.ts', '.js' ]
+  },
+  output = (dirname, filename) => ({
+    filename, path: path.join(__dirname, dirname)
+  });
+
+module.exports = (env, argv) => [
+/**
+ * jsCoq CLI
+ * (note: the waCoq CLI is located in package `wacoq-bin`)
+ */
+{
+  name: 'cli',
+  target: 'node',
+  entry: './coq-jslib/cli.ts',
+  ...basics(argv),
+  module: {
+    rules: [ts]
+  },
+  externals: {  /* do not bundle the worker */
+    '../coq-js/jscoq_worker.bc.js': 'commonjs2 ../coq-js/jscoq_worker.bc.js',
+    'wacoq-bin/dist/subproc': 'commonjs2'
+  },
+  resolve,
+  output: output('dist', 'cli.js'),
+  plugins: cliPlugins('dist/cli.js'),
+  node: false
+},
+{
+  name: 'toolkit',
+  target: 'node',
+  entry: './coq-jslib/build/sdk/toolkit.js',
+  ...basics(argv),
+  module: {
+    rules: [ts]
+  },
+  resolve,
+  output: output('dist', 'toolkit.js'),
+  plugins: cliPlugins('dist/toolkit.js'),
   node: false
 },
 /**
@@ -51,15 +92,8 @@ module.exports = (env, argv) => [
  */
 {
   name: 'ide-project',
-  mode: 'development',
   entry: './ui-js/ide-project.js',
-  devtool: argv.mode !== 'production' ? "source-map" : undefined,
-  stats: {
-    hash: false, version: false, modules: false  // reduce verbosity
-  },
-  performance: {
-    maxAssetSize: 1e6, maxEntrypointSize: 1e6   // 250k is too small
-  },
+  ...basics(argv),
   output: {
     filename: 'ide-project.browser.js',
     path: path.join(__dirname, 'dist'),
@@ -71,35 +105,10 @@ module.exports = (env, argv) => [
     'wacoq-bin/dist/subproc': 'commonjs2'
   },
   module: {
-    rules: [
-      {
-        test: /\.tsx?$/,
-        use: 'ts-loader',
-        exclude: /node_modules/,
-      },
-      {
-        test: /\.css$/i,
-        use: ['style-loader', 'css-loader'],
-      },
-      {
-        test: /\.scss$/i,  /* Vue.js has some */
-        use: ['style-loader', 'css-loader', 'sass-loader'],
-      },
-      {
-        test: /\.(png|jpe?g|gif)$/i,
-        loader: 'file-loader',
-        options: {
-          outputPath: 'ide-project-images',
-        }
-      },
-      {
-        test: /\.vue$/,
-        use: 'vue-loader'
-      }
-    ],
+    rules: [ts, css, scss, imgs, vuesfc]
   },
   resolve: {
-    extensions: [ '.tsx', '.ts', '.js' ],
+    ...resolve,
     fallback: { "stream": require.resolve("stream-browserify") }
   },
   plugins: [new VueLoaderPlugin(), 
@@ -111,15 +120,8 @@ module.exports = (env, argv) => [
  */
 {
   name: 'collab',
-  mode: 'development',
   entry: './ui-js/addon/collab.js',
-  devtool: argv.mode !== 'production' ? "source-map" : undefined,
-  stats: {
-    hash: false, version: false, modules: false  // reduce verbosity
-  },
-  performance: {
-    maxAssetSize: 1e6, maxEntrypointSize: 1e6   // 250k is too small
-  },
+  ...basics(argv),
   output: {
     filename: 'collab.browser.js',
     path: path.join(__dirname, 'dist/addon'),
@@ -127,19 +129,7 @@ module.exports = (env, argv) => [
     libraryTarget: 'umd'
   },
   module: {
-    rules: [
-      {
-        test: /\.css$/i,
-        use: ['style-loader', 'css-loader'],
-      },
-      {
-        test: /\.(png|jpe?g|gif)$/i,
-        loader: 'file-loader',
-        options: {
-          outputPath: 'collab-images',
-        }
-      }
-    ]
+    rules: [css, imgs]
   }
 }
 ];