Merge pull request #2 from jscoq/v8.17

ejgallego · web-flow · commit 00d2f7c16502 · 2023-10-10T10:44:32.000-07:00
[version] Port to Coq 8.17
diff --git a/CHANGES.md b/CHANGES.md
@@ -0,0 +1,7 @@
+unreleased
+----------
+
+- Allow `?backend=js` in the URL to set backend to JS instead of WASM
+  (@ejgallego, #2)
+- Port to jsCoq 8.17 , thanks to Shachar for a lot of help! (@ejgallego, #2)
+- Initial version, thanks to all in Zulip for lots of feedback.
diff --git a/Makefile b/Makefile
@@ -7,7 +7,7 @@ FILES_HTML=$(addsuffix .html,$(FILES))
 
 all: $(FILES_HTML)
 
-%.html: %.v %.glob
+%.html: %.v %.glob jscoqdoc
 	./jscoqdoc $<
 
 %.glob: %.v
diff --git a/README.md b/README.md
@@ -22,7 +22,9 @@ We have customized the following files from the oficial distro:
 + custom load of packages in `jscoq-agent.js`
 + custom paths in `jscoqdoc` binary
 
-We default to the WebAssembly jsCoq version.
+We default to the WebAssembly jsCoq version, to update that set the
+`backend:` parameter in the `jscoq-agent` file to `js` or use the
+query `?backend=wa` in the jsCoq URL.
 
 You may want to tweak more stuff too.
 
diff --git a/jscoq-agent.js b/jscoq-agent.js
@@ -4,7 +4,7 @@
  * This script is adapted from the Software Foundations jsCoq build.
  * So, it may require some tweaking depending on your development and styles.
  */
-import { JsCoq, Deprettify } from './node_modules/wacoq/ui-js/index.js';
+import { JsCoq, Deprettify } from './node_modules/jscoq/dist/frontend/index.js';
 
 function jsCoqInject() {
     var b = document.body;
@@ -22,7 +22,11 @@ var jsCoqShow = location.search === '?jscoq=on' ||
                 location.search !== '?jscoq=off' && localStorage.jsCoqShow === 'true';
 
 var jscoq_ids  = ['#main > div.code, #main > div.HIDEFROMHTML > div.code'];
+
+var sp = new URLSearchParams(location.search);
+
 var jscoq_opts = {
+    backend:   sp.get('backend') || 'wa',
     layout:    'flex',
     show:      jsCoqShow,
     focus:     false,
@@ -47,8 +51,8 @@ async function jsCoqLoad() {
     page.setAttribute('tabindex', '-1');
     page.focus();
 
-    // - load and start jsCoq
-    await JsCoq.load(jscoq_opts.base_path);
+    // - load and start jsCoq, not needed in 8.17
+    // await JsCoq.load(jscoq_opts.base_path);
 
     Deprettify.REPLACES.push(   // LF,PLF define their own versions (for Imp)
         [/∨/g, '\\/'], [/∧/g, '/\\'], [/↔/g, '<->'], [/≤/g, '<='], [/≠/g, '<>'],
diff --git a/jscoqdoc b/jscoqdoc
@@ -6,8 +6,8 @@ const fs = require('fs'),
       chld = require('child-process-promise');
 
 const JSCOQ_URL = process.env['JSCOQ_URL'] || '.',
-      SCRIPTS = ["node_modules/wacoq/ui-js/jscoq-loader.js", "jscoq-agent.js"],
-      STYLES = ["node_modules/wacoq/ui-css/jscoqdoc.css"];
+      SCRIPTS = ["node_modules/jscoq/dist/frontend/index.js", "jscoq-agent.js"],
+      STYLES = ["node_modules/jscoq/dist/frontend/index.css", "node_modules/jscoq/frontend/classic/css/jscoqdoc.css"];
 
 const DEFAULT_TEMPLATE =`
 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
diff --git a/package-lock.json b/package-lock.json
diff --git a/package.json b/package.json
