Round 272: TLA+ ext, Alloy ext, Z3 ext, miniKanren ext, Datalog ext (20 commands)
ober
b77ee45a4c82e54a43d17cf6521c5786a5d7daa3
--- a/docs/jemacs-vs-emacs.md +++ b/docs/jemacs-vs-emacs.md @@ -4583,6 +4583,31 @@ No remaining Tier 1 gaps. All core editing, completion, and navigation features | ebib-import-file | :orange_circle: | Import file into Ebib | | ebib-push-citation | :orange_circle: | Push Ebib citation to buffer | +### Round 272 — TLA+ ext, Alloy ext, Z3 ext, miniKanren ext, Datalog ext + +| Command | Status | Description | +|---------|--------|-------------| +| tlaplus-check | :orange_circle: | Check TLA+ specification | +| tlaplus-run-model | :orange_circle: | Run TLA+ model checker | +| tlaplus-parse | :orange_circle: | Parse TLA+ specification | +| tlaplus-translate | :orange_circle: | Translate TLA+ to PlusCal | +| alloy-run | :orange_circle: | Run Alloy analysis | +| alloy-check | :orange_circle: | Check Alloy assertions | +| alloy-show | :orange_circle: | Show Alloy instance | +| alloy-evaluate | :orange_circle: | Evaluate Alloy expression | +| z3-check | :orange_circle: | Check Z3 satisfiability | +| z3-eval | :orange_circle: | Evaluate Z3 expression | +| z3-prove | :orange_circle: | Prove Z3 theorem | +| z3-model | :orange_circle: | Show Z3 model | +| minikanren-run | :orange_circle: | Run miniKanren query | +| minikanren-test | :orange_circle: | Run miniKanren tests | +| minikanren-eval | :orange_circle: | Evaluate miniKanren expression | +| minikanren-trace | :orange_circle: | Trace miniKanren execution | +| datalog-load | :orange_circle: | Load Datalog program | +| datalog-query | :orange_circle: | Query Datalog | +| datalog-run | :orange_circle: | Run Datalog program | +| datalog-compile | :orange_circle: | Compile Datalog program | + ### Round 271 — Lean ext, Agda ext, Idris ext, Isabelle ext, HOL ext | Command | Status | Description | --- a/src/jerboa-emacs/editor-extra-final.ss +++ b/src/jerboa-emacs/editor-extra-final.ss @@ -21525,4 +21525,48 @@ (def (cmd-hol-print-thm app) (let* ((echo (app-state-echo app))) - (echo-message! echo "HOL: printing theorem"))) \ No newline at end of file + (echo-message! echo "HOL: printing theorem"))) + +;;; Round 272 — Z3 ext, miniKanren ext, Datalog ext (batch 2) + +(def (cmd-z3-prove app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "Z3: proving theorem"))) + +(def (cmd-z3-model app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "Z3: showing model"))) + +(def (cmd-minikanren-run app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "miniKanren: running query"))) + +(def (cmd-minikanren-test app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "miniKanren: running tests"))) + +(def (cmd-minikanren-eval app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "miniKanren: evaluating expression"))) + +(def (cmd-minikanren-trace app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "miniKanren: tracing execution"))) + +(def (cmd-datalog-load app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "Datalog: loading program"))) + +(def (cmd-datalog-query app) + (let* ((echo (app-state-echo app))) + (echo-read-string echo "Query: " + (lambda (query) + (echo-message! echo (str "Datalog: querying " query)))))) + +(def (cmd-datalog-run app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "Datalog: running program"))) + +(def (cmd-datalog-compile app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "Datalog: compiling program"))) \ No newline at end of file --- a/src/jerboa-emacs/editor-extra-modes.ss +++ b/src/jerboa-emacs/editor-extra-modes.ss @@ -22146,3 +22146,47 @@ (let* ((echo (app-state-echo app))) (echo-message! echo "Idris: type-checking at point"))) +;;; Round 272 — TLA+ ext, Alloy ext, Z3 ext, miniKanren ext, Datalog ext (batch 1) + +(def (cmd-tlaplus-check app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "TLA+: checking specification"))) + +(def (cmd-tlaplus-run-model app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "TLA+: running model checker"))) + +(def (cmd-tlaplus-parse app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "TLA+: parsing specification"))) + +(def (cmd-tlaplus-translate app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "TLA+: translating to PlusCal"))) + +(def (cmd-alloy-run app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "Alloy: running analysis"))) + +(def (cmd-alloy-check app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "Alloy: checking assertions"))) + +(def (cmd-alloy-show app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "Alloy: showing instance"))) + +(def (cmd-alloy-evaluate app) + (let* ((echo (app-state-echo app))) + (echo-read-string echo "Expression: " + (lambda (expr) + (echo-message! echo (str "Alloy: evaluating " expr)))))) + +(def (cmd-z3-check app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "Z3: checking satisfiability"))) + +(def (cmd-z3-eval app) + (let* ((echo (app-state-echo app))) + (echo-message! echo "Z3: evaluating expression"))) + --- a/src/jerboa-emacs/editor-extra-regs2.ss +++ b/src/jerboa-emacs/editor-extra-regs2.ss @@ -7129,4 +7129,25 @@ (register-command! 'hol-load cmd-hol-load) (register-command! 'hol-type-of cmd-hol-type-of) (register-command! 'hol-print-thm cmd-hol-print-thm) + ;; Round 272 + (register-command! 'tlaplus-check cmd-tlaplus-check) + (register-command! 'tlaplus-run-model cmd-tlaplus-run-model) + (register-command! 'tlaplus-parse cmd-tlaplus-parse) + (register-command! 'tlaplus-translate cmd-tlaplus-translate) + (register-command! 'alloy-run cmd-alloy-run) + (register-command! 'alloy-check cmd-alloy-check) + (register-command! 'alloy-show cmd-alloy-show) + (register-command! 'alloy-evaluate cmd-alloy-evaluate) + (register-command! 'z3-check cmd-z3-check) + (register-command! 'z3-eval cmd-z3-eval) + (register-command! 'z3-prove cmd-z3-prove) + (register-command! 'z3-model cmd-z3-model) + (register-command! 'minikanren-run cmd-minikanren-run) + (register-command! 'minikanren-test cmd-minikanren-test) + (register-command! 'minikanren-eval cmd-minikanren-eval) + (register-command! 'minikanren-trace cmd-minikanren-trace) + (register-command! 'datalog-load cmd-datalog-load) + (register-command! 'datalog-query cmd-datalog-query) + (register-command! 'datalog-run cmd-datalog-run) + (register-command! 'datalog-compile cmd-datalog-compile) )