Merge pull request #1304 from cryspen/manual-use-latest-hax-playground

feat(manual): hax-playground integration: use latest `main`
cryspen · Feb 10, 2025 · af5483c · af5483c
2 parents e0ea99a + df9f02a
commit af5483c
Showing 1 changed file with 12 additions and 5 deletions.
diff --git a/docs/javascripts/hax_playground.js b/docs/javascripts/hax_playground.js
@@ -1,5 +1,13 @@
+const PLAYGROUND_URL = 'https://hax-playground.cryspen.com';
+
+// Fetches the commit hash for latest `main` of hax
+async function get_latest_hax_main() {
+    let commits = await (await fetch(PLAYGROUND_URL + '/git-refs')).text();
+    return commits.match(/(.*);refs\/remotes\/origin\/main;/).pop();
+}
+
 // Call into the API of the hax playground
-function call_playground(result_block, query, text) {
+async function call_playground(result_block, query, text) {
     let raw_query = async (API_URL, hax_version, query, files, on_line_received) => {
         let response = await fetch(`${API_URL}/query/${hax_version}/${query}`, {
             method: "POST",
@@ -24,14 +32,13 @@ function call_playground(result_block, query, text) {
                 on_line_received(line);
         }
     };
-    let hax_version = '5ca1c13023200dee0cca6237901a3b5a69ad345a';
-    let playground_url = 'https://hax-playground.cryspen.com';
     let ansi_up = new AnsiUp();
     let first = true;
     let logs = document.createElement('div');
     logs.style = 'font-size: 80%; background: #00000010; padding: 3px;';
+    let hax_version = await get_latest_hax_main();
     raw_query(
-        playground_url,
+        PLAYGROUND_URL,
         hax_version,
         query,
         [['src/lib.rs', text]],
@@ -75,7 +82,7 @@ function call_playground(result_block, query, text) {
                     result_block.innerHTML += '<div style="float: left; padding: 3px; padding-top: 8px; position: relative; top: 6px;"><span style="color: gray;">Status: </span><span style="color: green">✓ F* successfully typechecked!</span></div>';
                 }
                 hljs.highlightBlock(result);
-                result_block.innerHTML += `<br/><a style="float:right; font-family: 'Open Sans', sans-serif; font-size: 70%; cursor: pointer; color: gray; text-transform: uppercase; position: relative; top: -10px;" href='${playground_url}/#fstar/${hax_version}/${LZString.compressToEncodedURIComponent(text)}'>Open in hax playground ↗</a>`;
+                result_block.innerHTML += `<br/><a style="float:right; font-family: 'Open Sans', sans-serif; font-size: 70%; cursor: pointer; color: gray; text-transform: uppercase; position: relative; top: -10px;" href='${PLAYGROUND_URL}/#fstar/${hax_version}/${LZString.compressToEncodedURIComponent(text)}'>Open in hax playground ↗</a>`;
             }
         },
     );